Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

214   5 Modelltheorie

Theorem 5-2. Termdenotate fur Modelle und Belegungen

Wenn (D, I) ein Modell und b eine Belegung fur D ist, dann:

(i)   Wenn α ∈ KONST, dann TD(α, D, I, b) = I (α),

(ii) Wenn β ∈ PAR, dann TD(β, D, I, b) = b (β), und

(iii) Wenn φ ∈ FUNK, wobei φ r-stellig ist, und θ₀, ..., θ_r-1 ∈ GTERM, dann
TD(^rφ(θo, ..., θr,ɪ)ɔ, D, I, b) = I(φ)(<TD(θ0, D, I, b)), ..., TD(θr-ι, D, I,
b )>)∙

Beweis: Sei (D, I) ein Modell und b eine Belegung fur D. Dann gibt es mit Theorem 5-1
genau eine Termdenotationsfunktion F fur D, I, b. Dann gilt nach Definition 5-6 fur alle
θ ∈ GTERM: TD(θ, D, I, b) = F(θ). Daraus folgt dann mit Definition 5-5 die Behaup-
tung. ■

Definition 5-7. Erfullungsfunktionen fur Modelle

F ist eine Erfullungsfunktion fur D, I

gdw

(D, I) ist ein Modell, F ist eine Funktion auf GFORM × {b | b ist eine Belegung fur D},
Ran(F) = {0, 1} und fur alle Belegungen b fur D gilt:

(i) Wenn Φ ∈ PRA, wobei Φ r-stellig ist, und θ₀, ..., θ_r-1 ∈ GTERM dann:
F(^rΦ(θo, ..., θr-ɪ)ɔ, b) = ɪ gdw (TD(θo, D, I, b), ..., TD(θr-ι, D, I, b)> ∈ I(Φ),

(ii) Wenn Α ∈ GFORM, dann: F(^r-Α∖ b) = 1 gdw F(Α, b) = 0,

(iii)  Wenn Α, Β ∈ GFORM, dann F (^rΑ ∧ Β"¹, b) = 1 gdw F (Α, b) = 1 und F (Β, b) = 1,

(iv)  Wenn Α, Β ∈ GFORM, dann F (^rΑ ∨ Β"¹, b) = 1 gdw F (Α, b) = 1 oder F (Β, b) = 1,

(v)   Wenn Α, Β ∈ GFORM, dann F (^rΑ → Β^^l, b) = 1 gdw F (Α, b) = 0 oder F (Β, b) = 1,

(vi)  Wenn Α, Β ∈ GFORM, dann F (^rΑ θ Β^^l, b) = 1 gdw F (Α, b) = F (Β, b),

(vii) Wenn ξ ∈ VAR, Δ ∈ FORM und FV(Δ) ⊆ {ξ}, dann

F (^rΛξΔ^π, b) = 1

gdw

es gibt β ∈ PAR∖TT(Δ), so dass fur alle b', die in β Belegungsvarianten von b fur
D sind: F([β, ξ, Δ], b') = 1, und

(viii) Wenn ξ ∈ VAR, Δ ∈ FORM und FV(Δ) ⊆ {ξ}, dann

F (^lVξΔ^,) = 1

gdw

es gibt β ∈ PAR∖TT(Δ) und b', das in β eine Belegungsvariante von b fur D ist, so
dass F ([β, ξ, Δ], b') = 1.

<<   185   186   187   188   189   190   191   >>

More intriguing information