Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

Theorem 1-11. Eindeutige Lesbarkeit ohne Satze (b - Eindeutige Zerlegbarkeit)

Wenn μ ∈ TERM ∪ QUANTOR ∪ FORM, dann:

(i) μ ∈ ATERM oder

(ii) μ ∈ FTERM und es gibt n ∈ N∖{0}, φ ∈ FUNK und {θ₀, .., θ_n-∣} ⊆ TERM, so dass μ
= ^rφ(θ₀, .., θ,,-∣f^l und fur alle n' ∈ N∖{0}, φ' ∈ FUNK und {θ'₀, .., θ'_n'_-1} ⊆ TERM
mit μ = ^rφ'(θ'₀, ..., θ'n'-ʃ gilt: n = n' und φ = φ' und fur alle i < n: θ_i = θ'i, oder

(iii) μ ∈ QUANTOR und es gibt Π ∈ QUANT und ξ ∈ VAR, so dass μ = ^rΠξ^^l und fur
alle Π' ∈ QUANT und ξ' ∈ VAR mit μ = ^rΠ'ξⁿ gilt: Π = Π' und ξ = ξ', oder

(iv)   μ ∈ AFORM und es gibt n ∈ N∖{0}, Φ ∈ PRA und {θ₀, ., θn_-∣} ⊆ TERM, so dass μ

= ^rΦ(θ₀, ., θ,,-∣f^l und fur alle n' ∈ N∖{0}, Φ' ∈ PRA und {θ'₀, ., θ'_n'_-1} ⊆ TERM

mit μ = ^rΦ'(θ'₀, ., θ'_n'_-1)^^l gilt: n = n' und Φ = Φ' und fur alle i < n: θ_i = θ'i, oder

(v)   μ ∈ { ^r-Δ^π | Δ ∈ FORM} und es gibt Δ ∈ FORM, so dass μ = ^r-Δ^^η und fur alle Δ' ∈

FORM mit μ = ^r- Δ^π gilt: Δ = Δ', oder

(vi) μ ∈ {^r(Δ0 ψ Δι)^π | Δ0, Δι ∈ FORM und ψ ∈ JUNK∖{^r-^π}} und es gibt Δ_o, ʌɪ ∈
FORM und ψ ∈ JUNK∖{^r-^π}, so dass μ = ^r(Δ₀ ψ Δ₁)^^l und fur alle Δ'₀, Δ'₁ ∈ FORM
und ψ' ∈ JUNK∖{ ^r-^π } mit μ = ^r(Δ'₀ ψ' Δ'₁)^^l gilt: Δ₀ = Δ'₀ und Δ₁ = Δ'₁ und ψ = ψ',
oder

(vii) μ ∈ QFORM und es gibt Π ∈ QUANT, ξ ∈ VAR und Δ ∈ FORM, so dass μ = ^rΠξΔ^^l
und fur alle Π' ∈ QUANT, ξ' ∈ VAR und Δ' ∈ FORM mit μ = ^rΠ'ξ'Δ^r, gilt: Π = Π'
und ξ = ξ' und Δ = Δ'.

Beweis: Sei μ ∈ TERM ∪ QUANTOR ∪ FORM. Also μ ∈ ATERM ∪ FTERM ∪
QUANTOR ∪ AFORM ∪ {^r-Δ^π | Δ ∈ FORM} ∪ {^r(Δ0 ψ Δι)^π | Δ0, ʌɪ ∈ FORM und ψ
∈ JUNK∖{^r-^^l}} ∪ QFORM. Es werden diese sieben Falle unterschieden. Erstens: An-
genommen μ ∈ ATERM. Damit ist (i) trivial erfullt.

Zweitens: Sei μ ∈ FTERM. Dann gibt es nach Definition ∣-6 und Definition ∣-7 n ∈
N∖{0}, φ ∈ FUNK und {θ₀, ., θ_n-1} ⊆ TERM, so dass μ = ^rφ(θ₀, ., θ_n-1)^π. Seien nun
auch n ∈ N∖{0}, φ' ∈ FUNK und {θ'₀, ., θ'_n'_-1} ⊆ TERM, so dass μ = ^rφ'(θ'₀, ., θ'_n'_-1)^^l.
φ = φ' folgt mit Theorem 1-7-(iii). Mit Theorem 1-7-(i) folgt damit ^rθ₀, ., θ∙_-∣Γ =
^rθ'₀, ., θ'_n'_-1)^π. Dann lasst sich durch Induktion uber i zeigen, dass fur alle i ∈ N gilt:
Wenn i < n, dann i < n' und θi = θ'i. Gelte dazu die Behauptung fur alle k < i. Angenom-
men i < n. Angenommen i = 0. Dann gilt, dass 0 < n'. Auβerdem gilt, dass es {μ₀, .,
μAUSL(θ0)-1} ∪ {μ'0^, ∙∙∙^, μ'AUSL(θ'0)-1} ⊆ GAUS gibt^, so ^dass θ0 = ^l^μ0∙∙∙ μAUSL(θ0)-1^^{l and θ}'0 =
^rμo.μ'AUSL(θ'0)-ι^^l und somit mit Theorem 1-6 ^rμ0. μAUSL(θ0)-ι, ., θn-ι)^^l =
^rμ'o.μAUSL<θ'o)-b ., θ'_n'_-1)^π. Ware AUSL(θ₀) < AUSL(θ'₀). Dann ware mit Theorem
∣-5-(iii) fur alle l < AUSL(θ0) μl = μ'l und damit nach Postulat ∣-2-(i) θ0 =
^rμ₀. liλ∣-_s∣ ,θ ∙∣_-Γ = ^rμ'₀. li'a_us∣,∣∙θ ∣_-C. Damit ware dann aber mit Theorem 1-6

<<   <   21   22   23   24   25   26   27   >   >>