256 6 Korrektheit und Vollstandigkeit des Redehandlungskalkuls
GTERMH, so dass a = [θ]A. Dann gilt nach Definition 6-2-(xv) rθ = θ^l ∈ X und damit
ergibt sich (a, a) ∈ IX(r=^l). Damit ist dann gemaβ Definition 5-2H (DX, IX) ein ModellH.
Sodann sieht man leicht ein, dass bχ eine BelegungH fur DX ist.
Sodann gilt fur alle φ ∈ FUNK: Wenn φ r-stellig ist und θ0, ..., θr-1 ∈ GTERMH, dann:
IX(φ)(([θo]A, ., [θr-ι]A)) = [ rφ(θo, ., θr-ι)π ]A. Seien dazu φ ∈ FUNK r-stellig und θo, .,
θr-1 ∈ GTERMH. Dann gilt mit Definition 6-2-(xv) rφ(θ0, ., θr-1) = φ(θ0, ., θr-1)^l ∈ X
und damit (([θo]A, ., [θr-1]A), [φ(θo, ., θr-1)]A) ∈ IX(φ) und damit IX(φ)(([θo]A, ., [θr-1]A))
= [rφ(θo, ., θr-1Γ]A.
Nun wird gezeigt, dass fur alle Φ ∈ PRA: Wenn Φ r-stellig ist und θ0, ., θr-1 ∈
GTERMH, dann: ([θ0]A, ., [θr-1]A) ∈ IX(Φ) gdw rΦ(θ0, ., θr-1)^l ∈ X. Seien dazu Φ ∈
PRA, Φ r-stellig und θo, ., θr-1 ∈ GTERMH. Gelte nun zunachst ([θo]A, ., [θr-1]A) ∈
IX(Φ). Dann gibt es θ'o, ., θ'r-1, so dass fur alle i < r: [θi]A = [θ'i]A und (θ'o, ., θ'r-1) ∈
rGTERMH und rΦ(θ'0, ., θ'r-1)^l ∈ X. Dann gilt mit b) fur alle i < r: rθ- = θ,f ∈ X. Mit
der oben gezeigten Symmetrie gilt dann fur alle i < r: rθ'i = θ,ɔ ∈ X. Sodann gilt rΦ(θ'0,
., θ'r-1)^l ∈ X und damit nach Definition 6-2-(xvii) auch rΦ(θ0, ., θr-1)^l ∈ X. Sei nun
umgekehrt rΦ(θ0, ., θr-1)^l ∈ X. Dann ergibt sich leicht, dass ([θ]0, ., [θ]r-1) ∈ IX (Φ).
Sodann ergibt sich mit Theorem 5-2H durch Induktion uber den Termaufbau fur alle θ ∈
GTERMH: TD(θ, DX, IX, bX) = [θ]A. Sei namlich α ∈ KONST ∪ KONSTNEU. Dann ist
TD(α, DX, IX, bX) = IX(α) = [α]A. Sei β ∈ PAR. Dann ist TD(β, DX, IX, bX) = bX(β) = [β]A.
Gelte die Behauptung nun fur θ0, ., θr-1 ∈ GTERMH und sei rφ(θ0, ., θr-1)^l ∈
FTERMH. Dann ist TDH(rφ(θo, ., θr-ι)π, DX, IX, bX) = IX (φ)((TD(θo, DX, IX, bX), .,
TDH(θr-ι, DX, IX, bX))) und damit mit I.V. TDH(rφ(θo, ., W, DX, IX, bX) = IX(φ)(([θo]A,
., [θr-ι] A)) = [rφ(θo, ., θr-ι)π] A.
Damit gilt dann fur alle Α ∈ AFORMH: DX, IX, bX ⅛ Α gdw Α ∈ X. Sei namlich Α ∈
AFORMH. Dann gibt es Φ ∈ PRA, Φ r-stellig, und θo, ., θr-1 ∈ GTERMH, so dass Α =
rΦ(θo, ., θ ) . Dann gilt:
Dx , IX, bX ⅛ a
gdw
Dx, Iχ, bχ ⅛ rΦ(θo, ., θr,ιΓ