Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

10    1 Zum grammatischen Rahmen

μ⁺_s = μ^μl°_r° fur die eindeutig bestimmten l°, r°, fur die 0 < l° < i+1, r° < AUSL(μ_l°) und s =
(∑n → AUSL(μ_n))+r°,
und

μ'⁺s = μ'^μ'l'°r'° fur die eindeutig bestimmten l'°, r'°, fur die 0 < l'° < i+1, r'° < AUSL(μ'l'°)
und s = (∑n°=0 AUSL(μ'n))+r'°.

Mit l°, l'° < i+1 gilt dann l°, l'° ≤ i. Damit gilt nach Annahme AUSL(μl'°) = AUSL(μ'l'°)
und ∑...'° O AUSL(μn) = ∑n°= O AUSL(μ'n). Damit gilt 0 < l'° < i+1 und r'° < AUSL(μ_r)
und s = (∑n = O AUSL(μ_n))+r'°. Dann ist nach Theorem 1-3 l'° = l° und r'° = r°. Ware nun
i+1 ≤ l. Dann ware i ≤ l-1. Damit ware aber t = ∑n = _o AUSL(μ_n) ≤ ∑_n ¹ _o AUSL(μ_n) ≤ s.
Widerspruch! Also ist l < i+1. Damit ergibt sich dann l = l° und r = r°. Analog ergibt
sich, dass l' = l'° und r' = r'°, womit dann insgesamt gilt: l = l° = l'° = l' und r = r° = r'° =
r'. Damit ist dann μ*s = μ^μlr = μ⁺s und μ'*s = μ'^μ'lr = μ'⁺s. Wegen μ*s = μ'*s, ist damit μ⁺s =
μ'⁺s. Also gilt fur alle s < t = t', dass μ⁺s = μ'⁺s und damit nach Postulat 1-2-(i), dass
^rμ₀...μi^^l = ^rμ⁺₀...μ⁺_t-Γ = ^rμ'⁺₀...μ'VΓ = ^rμ'₀... μ'Γ. Sodann gilt mit Theorem 1-4-(i),
dass ^rμo∙..μi^^, = ^rμ^μ00∙∙∙ μ^μ0AUSL(μ0)-1∙∙∙ μ^μ,0∙∙∙ μ^μiAUSL<μi)-Γ und ^rμ'0...μ'i^¹ =
^rμ'^μ'⁰0. μ'^μ'⁰AUSL(μ'0)-1. μ'^μ'ⁱ0. μ'^μ'ⁱAUSL(μ',)-Γ. Damit gilt dann auch fur 0 < i, dass a) gilt.

Sei nun fur b) j ≤ i. Fur den Fall j = 0 wurde oben bereits gezeigt, dass dann μj = μ'j gilt.
Sei nun 0 < j ≤ i. Sei nun r < AUSL(μj) = AUSL(μ'j). Dann ist (∑^j_n = _o AUSL(μ_n))+r =
(∑n = _o AUSL(μ'_n))+r < t = t' ≤ m = m'. Dann gilt mit s = (∑^j_n =¹ _o AUSL(μ_n))+r, dass μ⁺_s =
μ^μjr und μ'⁺s = μ'^μ'jr. Da s < t = t' gilt dann, wie eben gezeigt, dass μ⁺s = μ'⁺s und damit auch
μ^μjr = μ'^μ'jr. Also gilt fur alle r < AUSL(μj) = AUSL(μ'j), dass μ^μjr = μ'^μ'jr. Damit gilt dann
mit Postulat 1-2-(i), dass μj∙ = ^rμ^μ⅛∙∙∙μ^μjAUSL(μ,)-Γ = ^rμ'^μ'⅛∙∙∙μ"‰SL<μ'j)-Γ = μ'j. Damit gilt
b) auch fur 0 < i. ■

Theorem 1-6. Zur Identitat von Ausdrucksverkettungen (c)

Wenn k, s ∈ N\{0} und {μ0, ., μk-1} ⊆ AUS und {μ'0, ., μ's-1} ⊆ AUS und j < k und μj =
^rμ'0. μ',-1^π, dann: ^rμ0. μ_fc√ = ^rμc. μj-1μ'0 . μ's-1 μj+1.. μt√.

Beweis: Seien k, s ∈ N\{0} und {μ0, ., μk-1} ⊆ AUS und {μ'0, ., μ's-1} ⊆ AUS und j <
k und μ_j∙ = ^rμ'₀. μ'_s-ι^^l. Dann gibt es mit {μ'₀, ., μ'_s-ι} ⊆ AUS und Theorem 1-2 fur alle i
< s {μ'^μ'ⁱ0, ., μ'^μ'ⁱAUSL(μ'i)-1} ⊆ GAUS, so dass μ'i = ^rμ'^μ'ⁱ0∙∙∙μ'^μ'ⁱAUSL(μ',)-Γ. Mit Theorem
1-4-(i) ist μj = ^rμ'0.μ's-1^π = ^rμ'^μ'⁰0.μ'^μ'⁰AUSL(μ'0)-1.μ'^μ'^s-¹0.μ'^μ'^s-¹AUSL(μs.₁)-1^π. Mit Postulat
1-3 gilt ^rμ0∙∙∙μk-1^^l = ^rμ0∙∙∙μj-1μ'^μ00∙∙∙μ'^μ0AUSL(μ'0)-1∙∙∙μ'^μs^¹0...μ'^μs'¹AUSL(μ'_s-1)-1μj+1.μk-1^¹.
Durch Induktion uber i wird zunachst gezeigt, dass fur alle i < s gilt:

<<   <   12   13   14   15   16   17   18   >   >>