Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

1 Zum grammatischen Rahmen

Theorem 1-5. Zur Identitat von Ausdrucksverkettungen (b)

Wenn k, k' ∈ N∖{0} und fur alle i < k: μ_i ∈ AUS und μi = ^rμ^μ*o^μ^μ,A_usL(_μ,)_-1^π, wobei {μ^μi₀, .,
μ^μ*AusL(μ,)-ι} ⊆ GAUS, und fur alle i < k': μ'_i ∈ AUS und μ'_i = ^rμ'^μ'ⁱ0^μ'^μ'*AusL(μ',)-1^π, wobei
{μ'^μ'ⁱo, ., μ'^μ'*AusL(μ',)-ι} ⊆ GAUS, und wenn 'μ .μ ∣ = >' .μ' ∣, dann:

(i)     ^rμo...μk√

^rμ^μ00 . μ^μθAUSL(μo)-1 . μ^μk^-10 . μ^μk^-1AUSL(μk-i)-1∣

^rμ'^μ00. μ'^μ0AUSL(μ'0)-1 . μ'^μk'^-10. μ'^μk'^1AUSL(μ⅛.ι)-1∣

^rμ'0∙ ∙ ∙ μ'k'-ι^l,

(ii)   AUSL(⅛...μk√) = ∑ 0 AUSI(U) = ∑ 0 AUSL(μjj) = AUSL(^rμ'0.μW) und

(iii) Fur alle i < k, k': Wenn AUSL(μ_j) = AUSL(μ'_j) fur alle j ≤ i, dann:

a)     ^rμc.μi∣

^rμ^μ00 . μ^μ0AUSL(μ0)-l . μ^μi0 . μ^μ,AUSL(μi)-1∣

^rμ'^{μ 0}0. μ'^{μ 0}AUSL(μ'0)-1. μ'^μ ’0. μ'^{μ i}AUSL(μ'i)-ι∣

'μ' .μ' ∣ und

b)     Fur alle j ≤ i: μ_j∙ = μ'_j∙.

Beweis: Seien k, k' ∈ N∖{0} und fur alle ’ < k: μi ∈ AUS und μ_i = ^rμ^μi₀... p,^ausl(^)-i' ,
wobei {μ^μi0, ., μ^μiAUSL(μ_i)-1} ⊆ GAUS, und fur alle i < k': μ'i ∈ AUS und μ'i =
^rμ'^μ⅛.μ'^μ'ⁱAUSiχμ∙√∣, wobei {μ'^μ'⅛, ., μ'^μ''AUSL(μ'i)-ι} ⊆ GAUS, und sei ^rμ0.μ_fc-Γ =
^rμ'₀. μ'_k'_-1∣. Dann gelten (i) und (ii) mit Theorem 1-4-(i) und -(ii).

Sei nun fur (iii) ’ < k, k' und sei AUSL(μ_j) = AUSL(μ'j) fur alle j ≤ ’. Zunachst gilt mit
Postulat 1-3: Es gibt m* ∈ N∖{0} und {μ*₀, ., μ*_m-1} ⊆ GAUS, so dass ^rμ₀.μ⅛_-Γ =
^rμ*₀. μ*_m-ι∣ und m = ∑n~=₀ AUSL(μ_n) und fur alle s < m: μ*_s = μ^μ0_s, falls s < AUSL(μ₀),
und μ*s = μ^μlr fur die eindeutig bestimmten l, r, fur die 0 < l < k, r < AUSL(μl) und s =
(∑_n ¹ ₀ AUSL(μ_n))+r, falls AUSL(μ₀) ≤ s, und es gibt m' ∈ N∖{0} und {μ'*₀, ., μ'*_m'_-ι}
⊆ GAUS, so dass ^rμ'₀. μ'_k∙.f = ^rμ'*₀. μ'*_m∙-ι∣ und m' = ∑n'Z¹₀ AUSL(μ'_n) und fur alle s
< m': μ'*s = μ'^μ'0s, falls s < AUSL(μ'0), und μ'*s = μ'^μ'l'r' fur die eindeutig bestimmten l', r',
fur die 0 < l' < k', r' < AUSL(μ'ι∙) und s = (∑n^J₀ AUSL(μ'_n))+r', falls AUSL(μ'0) ≤ s.

Dann ist mit (ii) m = m'. Sodann ist mit (i):

<<   <   10   11   12   13   14   15   16   >   >>