Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

^гЦю. μj-ιμ'^{μ 0}0. μ'^{μ 0}AUSL(μ'0)-1 ... μ'^{μ s}^¹0... μ'^{μ s-1}AUSL(μ's-1)-1μj+1 .. μk-ι^π

^rμo. μ_j∙-ι μ'o. μ'iμ'^μ '⁺¹o. μ'^{μ ,+1}AusL(μ⅛ι)-ι ■■■ μ'^{μ s-1}0 ■■■ μ'^{μ s}^¹AUSL(μ^,_s-ι)-ι μj+ι. μ⅛-ι^π.

Damit gilt dies dann auch fur i = s-1 und damit gilt dann

^rμo...μk√

^l"μ0∙.. μj-iμ'^μ 00. μ'^{μ 0}AUSL(μ'0)-1 ∙∙∙ μ'^{μ s-1}0∙∙∙ μ'^{μ s-}1AUSL(μ's-1)-1μj+1 ∙∙∙ Цк-Ґ

^rμo. μj-ι μ'o. μ's-ι μ₇+ι. μk-ι^π.

Damit gilt dann das Theorem. Gelte die Behauptung nun fur alle l < i. Sei nun i < s. Dann
ist i = 0 oder 0 < i. Sei i = 0. Wegen μ'0 = ^rμ'^μ00∙∙∙ μ'^μ0AUSL(μ'0)-1^^l ist dann nach Postulat
1-3:

^rμ0∙ ∙ ∙ μj-ιμ'^{μ 0}0. μ'^{μ 0}AUSL(μ'0)-1. μ'^{μ s-1}0∙ ∙ ∙ μ'^{μ s-1}AUSL(μ's-1)-1μj+1. μk-ι^π

^l"μ0 . μj-1 μ'0μ'^{μ 1}0. μ'^μ 1AUSL(μ'ι)-1 . μ'^μs-10 . μ'^μs-1AUSL(μ's-1)-1 μj+1... μ⅛-1^π.

Sei nun 0 < i. Dann gilt fur alle l < i, dass l < s und damit nach I.V.:

^rμ0. μj-1μ'^{μ 0}0. μ'^{μ 0}AUSL(μ⅛)-1. μ'^{μ s-1}0. μ'^{μ s-1}AUSL(μ's-1)-1μj+1. цм^п

^rμ0. μj-1μ'0. μ'ιμ'^{μ l+1}0. μ'^{μ l+1}AUSL(μ'ι+1)-1. μ'^{μ s-1}0. μ'^{μ s-1}AUSL(μ's-1)-1μj+1. μk-1^π.

Da nun mit 0 < i gilt, dass i-1 < i, gilt damit:

^rμ0. μj-1μ'^{μ 0}0. μ'^{μ 0}AUSL(μ'0)-1. μ'^{μ s-1}0. μ'^{μ s-1}AUSL(μ's-1)-1μj+1. μk-∣^π

^rμ0. μ₇-1 μ'0. μ'i-1 μ'^{μ i}0. μ'^{μ i}AUSL(μ',)-1. μ'^{μ s-1}0. μ'^{μ s}-¹AUSL(μ's-1)-1 μj+1. μ⅛-1^π.

Wegen μ'_i = ^rμ'^μ'ⁱ₀. μ'^μ'ⁱ_AUSL(_μ'_i)_-Γ gilt dann mit Postulat 1-3:

^rμ0. μj-1μ'^{μ 0}0. μ'^{μ 0}AUSL(μ⅛)-1. μ'^{μ s}'¹0. μ'^{μ s}'¹AUSL(μ's-1)-1μj+1. μk-1^π

^rμ0. μ₇∙-1 μ'0. μ'i-1 μ'^{μ i}0. μ'^{μ i}AUSL(μ',)-1. μ'^{μ s-1}0. μ'^{μ s}-¹AUSL(μ's-1)-1 μj+1. μ⅛-1^π

^rμ0. μ₇∙-1 μ'0. μ'iiμ'^{μ i+1}0. μ'^{μ i+1}AUSL(μ⅛1)-1. μ'^{μ s-1}0. μ'^{μ s}^¹AUSL(μ'_s-1)-1 μj+1. μ⅛-1^π.

Damit gilt die Behauptung fur alle i < s und das Theorem ergibt sich wie oben angeben. ■

<<   13   14   15   16   17   18   19   >>

More intriguing information