Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

6.2 Vollstandigkeit des Redehandlungskalkuls 247

gdw

b ist eine Belegung fur D.

Zu (iii): Mit Definition 5-4H, (ii) und Definition 5-4 gilt:

b' ist in β eine BelegungsvarianteH von b fur D
gdw

b' und b sind BelegungenH fur D und β ∈ PAR und b'∖{(β, b'(β))} ⊆ b
gdw

b' und b sind Belegungen fur D und β ∈ PAR und b'∖{(β, b'(β))} ⊆ b
gdw

b' ist in β eine Belegungsvariante von b fur D.

■

Theorem 6-4. L_H-Modelle verhalten sich im Bezug auf geschlossene L-Terme, L-Aussagen und
L-Aussagenmengen genauso wie ihre Beschrankungen auf L

Wenn (D, I) ein ModellH und b eine BelegungH fur D ist, dann gilt fur alle θ ∈ GTERM, Γ ∈
GFORM und X ⊆ GFORM:

(i)   TDH(θ, D, I, b) = TD(θ, D, I f(KONST ∪ FUNK ∪ PRA), b),

(ii)  D, I, b ⅛ Γ gdw D, IЇ (KONST ∪ FUNK ∪ PRA), b к Γ, und

(iii)  D, I, b ⅛ X gdw D, IKKONST ∪ FUNK ∪ PRA), b к X.

Beweis: (i) und (ii) zeigt man analog zum Koinzidenzlemma (Theorem 5-5) durch Induk-
tion uber den Term- und Formelaufbau. Dabei wird zusatzlich auf Theorem 6-3 zuruck-
gegriffen. (iii) ergibt sich dann mit (ii) und Definition 5-9H bzw. Definition 5-9. ■

Theorem 6-5. Eine L-Aussagenmenge ist genau dann L_H-erfullbar, wenn sie L-erfullbar ist
Wenn X ⊆ GFORM, dann: X ist erfullbarH gdw X ist erfullbar.

Beweis: Sei X ⊆ GFORM. Sei nun X erfullbarH. Dann gibt es nach Definition 5-17H D,
I, b, so dass D, I, b kH X. Mit Theorem 6-4 gilt dann D, IKKONST ∪ FUNK ∪ PRA),
b к X und damit ist X erfullbar. Sei nun X erfullbar. Dann gibt es D, I, b, so dass D,
I, b^- к X. Nun gibt es ein a ∈ D. Sei nun I⁺ = I^- ∪ (KONSTNEU × {a}). Dann ist (D,
I⁺) ein ModellH und b^- eine BelegungH und IK(KONST ∪ FUNK ∪ PRA) = I. Mit
Theorem 6-4 ergibt sich dann D, I⁺, b^- kH X und damit ist X erfullbarH. ■

<<   217   218   219   220   221   222   223   >>

More intriguing information