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 θ0, ..., θ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 θ0, ..., θ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Α ∧ Β"1, b) = 1 gdw F (Α, b) = 1 und F (Β, b) = 1,
(iv) Wenn Α, Β ∈ GFORM, dann F (rΑ ∨ Β"1, 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.