Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

6.2 Vollstandigkeit des Redehandlungskalkuls 255

Sei nun D_X = GTERMH/A = {[θ]_A | θ ∈ GTERMH}. Sei sodann I_X eine Funktion mit
Dom(IX) = KONST ∪ KONSTNEU ∪ FUNK ∪ PRA, wobei fur alle α ∈ KONST ∪
KONSTNEU: IX(α) = [α]A und fur alle φ ∈ FUNK: Wenn φ r-stellig, dann IX(φ) =
{(<[θo]A, ., [θr-ι]A), [θ*]A) | (<θo, ., θr-ι>, θ*) ∈ ^rGTERMH × GTERMh und ^rφ(θo, .,
θ_r-ι) = θ*^^l ∈ X} und fur alle Φ ∈ PRA: Wenn Φ r-stellig, dann IX (Φ) = {<[θ₀] A, ...,
[θ_r-1]A) | <θ0, ∙∙∙, θ_r-ι) ∈ ^rGTERMH und ^rΦ(θ₀, ., θ_r-1)^^l ∈ X}. Sei zuletzt bX eine Funkti-
on mit Dom(b_X) = PAR und fur alle β ∈ PAR: b_X(β) = [β]_A.

Dann ist nach Definition 5-1_h IX eine InterpretationsfunktionH fur DX. Zunachst gilt fur
alle α ∈ KONST ∪ KONSTNEU: I_X(α) = [α]_A ∈ D_X. Sei nun φ ∈ FUNK r-stellig. Dann
ist IX(φ) = {(<[θo]_A, ., [θr-1]_A), [θ*]_A) | (<θo, ., θr-1), θ*) ∈ ^rGTERMH × GTERMH und
^rφ(θ₀, ., θ_r-1) = θ*^^l ∈ X}. Damit ist IX(φ) ⊆ ^rD_x × DX. Sei nun <a₀, ., a_r-1) ∈ ^rD_x.
Dann gibt es θo, ., θr-1 ∈ GTERMH, so dass fur alle i < r: ai = [θi]_A. Sodann gilt mit
Definition 6-2-(xv) ^rφ(θo, ., θr-ι) = φ(θo, ., θr-ι)^^l ∈ X und damit (<[θo] A, ., [θr-ι] A),
[φ(θo, ., θr-1)]_A) ∈ IX(φ) und also <ao, ., ar-1) ∈ Dom(IX(φ)). Seien nun (<ao, ., ar-1),
a*) ∈ I_X(φ) und (<ao, ., ar-1), a⁺) ∈ I_X(φ). Dann gibt es θo, ., θr-1 und θ*, so dass fur al-
le i < r: ai = [θi]_A und a* = [θ*]_A und (<θo, ., θr-1), θ*) ∈ ^rGTERMH × GTERMH und
^rφ(θ₀, ., θ_r-1) = θ*^^l ∈ X und es gibt θ'₀, ., θ'_r-1 und θ⁺, so dass fur alle i < r: a_i = [θ'_i]A
und a⁺ = [θ⁺]A und (<θ'o, ., θ'r-ι), θ⁺) ∈ ^rGTERMH × GTERMH und ^rφ(θ'o, ., θ'r-ι) = θ^+π
∈ X. Dann gilt fur alle i < r: [θi]_A = ai = [θ'i]_A. Damit gilt dann fur alle i < r: (θi, θ'i) ∈ A
und damit ^rθ_i = θ'Γ ∈ X. Damit gilt nach Definition 6-2-(xvi): ^rφ(θ₀, ., θ_r-1) = φ(θ'₀, .,
θ'r-ι)^π ∈ X und damit mit b): [ ^rφ(θo, ., θr-ι)^π ]A = [ ^rφ(θ'o, ., θ'r-ι)^π ]A. Mit ^rφ(θo, ., θr-ι)
= θ*^^l ∈ X und ^rφ(θ'₀, ., θ'_r-1) = θ⁺^^l ∈ X und b) gilt sodann auch [ ^rφ(θ₀, ., θ_r-1)^π ]A =
[θ*] A und [^rφ(θ'₀, ., θ'_r-1)^^l ] A = [θ⁺] A und damit insgesamt a * = [θ*] A = [θ⁺] A = a⁺. Also
ist I_X(φ) insgesamt eine r-stellige Funktion uber D_X. Ferner gilt fur alle Φ ∈ PRA: Wenn
Φ r-stellig ist, dann IX(Φ) ⊆ ^rDX. Zuletzt gilt IX(^r=^^l) = {<a, a) | a ∈ DX}. Sei namlich <a,
a') ∈ IX(^r=^^l). Dann gibt es θ, θ' ∈ GTERMH, so dass a = [θ]A und a' = [θ']A und ^rθ = θ^π
∈ X. Damit ergibt sich mit b): a = [θ]_A = [θ']_A = a'. Sei nun a ∈ D_X. Dann gibt es ein θ ∈

<<   225   226   227   228   229   230   231   >>

More intriguing information