Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

216   5 Modelltheorie

es mit Theorem 5-3 genau eine Erfullungsfunktion F fur D, I. Damit gilt dann mit
Definition 5-8 fur alle Γ ∈ GFORM: D, I, b к Γ gdw F(Γ, b) = 1 und D, I, b ≠ Γ gdw
F(Γ, b) = 0. Daraus ergibt sich die Behauptung dann mit Definition 5-7. ■

Theorem 5-5. Koinzidenzlemma

Wenn (D, I) und (D, I') Modelle und b, b' Belegungen fur D sind, dann:

(i) Fur alle θ ∈ GTERM: Wenn I ΓTA(θ) = I 'ΓTA(θ) und b ΓTT(θ) = b 'ΓTT(θ), dann TD(θ,
D, I, b) = TD(θ, D, I', b'), und

(ii) Fur alle Γ ∈ GFORM: Wenn I ΓTA(Γ) = I 'ΓTA(Γ) und b ΓTT(Γ) = b 'ΓTT(Γ), dann D,
I, b к Γ gdw D, I', b' к Γ.

Beweis: Zu (i): Seien (D, I) und (D, I') Modelle und b, b' Belegungen fur D. Der Beweis
wird durch Induktion uber den Termaufbau von θ ∈ TERM gefuhrt. Sei zunachst θ ∈
ATERM ∩ GTERM und gelte IΓTA(θ) = I'ΓTA(θ) und bΓTT(θ) = b'ΓTT(θ). Dann ist θ ∈
KONST ∪ PAR. Sei nun θ ∈ KONST. Dann gilt mit {θ} = TA(θ) ∩ KONST, I ΓTA(θ) =
I'ΓTA(θ) und Theorem 5-2-(i): TD(θ, D, I, b) = I(θ) = I'(θ) = TD(θ, D, I', b'). Sei nun θ
∈ PAR. Dann gilt mit {θ} = TT(θ) ∩ PAR, b ΓTT(θ) = b 'ΓTT(θ) und Theorem 5-2-(ii):
TD(θ, D, I, b) = b(θ) = b'(θ) = TD(θ, D, I', b').

Gelte die Behauptung nun fur θ₀, ., θ_r-ι ∈ TERM und sei φ ∈ FUNK, wobei φ r-
stellig, und sei ^rφ(θo, ., θr-ι)^π ∈ FTERM ∩ GTERM und gelte I ΓTA(^rφ(θo, ., θr-ι)^π) =
I TTA(^rφ(θo, ., θr-ι)^π) und b ΓTT(^rφ(θo, ., θr-ɪ)ɔ) = b TTT(^rφ(θo, ., θr-ι)^π). Dann gilt
mit FV(^rφ(θ₀, ., θ_r-ι)^^l) = U{FV(θi) | i < r} fur alle θ_i mit i < r ebenfalls: θ_i ∈ GTERM.
Sodann gilt mit U{TA(θi) | i < r} ⊆ TA(^rφ(θ₀, ., θ_r-ι)^^l) und U{TT(θ_i) | i < r} ⊆
TT(^rφ(θo, ., θr-ι)^π) fur alle i < r: I ΓTA(θi) = I 'ΓTA(θi) und b ΓTT(θi) = b 'ΓTT(θi). Mit
I.V. gilt somit fur alle i < r: TD(θi, D, I, b) = TD(θi, D, I', b'). Sodann gilt mit φ ∈
TA(^rφ(θ₀, ., θ_r-ι)^^l) ∩ FUNK nach Annahme auch I (φ) = I '(φ). Damit gilt:

TD(^rφ(θo, ., θr-ʃ, D, I, b)

I(φ)((TD(θo, D, I, b), ., TD(θr-ι, D, I, b)>)

I'(φ)((TD(θo, D, I', b'), ., TD(θr-ι, D, I, b')>)

TD(^rφ(θo, ., θr-ʃ, D, I', b').

<<   187   188   189   190   191   192   193   >>

More intriguing information