Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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 θ₀, ..., θ_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φ(θ₀, ., θ_r-1) = φ(θ₀, ., θ_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-₁Γ]A.

Nun wird gezeigt, dass fur alle Φ ∈ PRA: Wenn Φ r-stellig ist und θ₀, ., θ_r-1 ∈
GTERMH, dann: ([θ₀]A, ., [θ_r-1]A) ∈ IX(Φ) gdw ^rΦ(θ₀, ., θ_r-1)^^l ∈ X. Seien dazu Φ ∈
PRA, Φ r-stellig und θo, ., θr-1 ∈ GTERMH. Gelte nun zunachst ([θo]_A, ., [θr-1]_A) ∈
I_X(Φ). Dann gibt es θ'o, ., θ'r-1, so dass fur alle i < r: [θi]_A = [θ'i]_A und (θ'o, ., θ'r-1) ∈
^rGTERMH und ^rΦ(θ'₀, ., θ'_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Φ(θ'₀,
., θ'_r-1)^^l ∈ X und damit nach Definition 6-2-(xvii) auch ^rΦ(θ₀, ., θ_r-1)^^l ∈ X. Sei nun
umgekehrt ^rΦ(θ₀, ., θ_r-1)^^l ∈ X. Dann ergibt sich leicht, dass ([θ]₀, ., [θ]_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 θ₀, ., θ_r-1 ∈ GTERMH und sei ^rφ(θ₀, ., θ_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^{, b}X ⅛ ^a

gdw

Dx, Iχ, bχ ⅛ ^rΦ(θo, ., θr,ιΓ

<<   226   227   228   229   230   231   232   >>

More intriguing information