Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

(viii) Wenn ^rΠξΔ^^l ∈ QFORM, dann sei <i_o, ..., i_s-1> so, dass s = ∣{j ∣ j < k und θj ≠ ξ}∣ und
fur alle l < s gilt il ∈ {j | j < k und θj ≠ ξ} und fur alle k < l < s gilt ik < il, und es sei

[<θ'o, ., θ'k-₁>, <θo, ., θk-₁>, ^r∏ξΔ^π] = ^r∏ξ[<θ⅛, ., θ∙is-ι>, ‰ ., θi_s-₁>, ΔΓ, falls
∣{j ∣ j < k und θj ≠ ξ}∣ ≠ 0, [<θ'o, ., θ'k-ι>, <θ0, ., θk-ι>, '∣∣ξΔ' I = '∏ξΔ' sonst,

(ix) Wenn ^rΞΔ^π ∈ SATZ, dann

[<θ'o, ., θ'k-ι>, <θo, ., θk-ι>, ^rΞΔ^π] = ^rΞ[<θ'o, ., θ'k-ι>, <θo, ., θk-ι>, ΔΓ, und

(x) Wenn £ ∈ SEQ, dann [<θ'o, ., θ'k-ι>, <θo, ., θk-ι>, Я]

= {(j, [<θ'o, ., θ'k-ι>, <θo, ., θk-ι>, j ∣ j ∈ Dom(S)}.

In Klausel (viii) wird die Substitution in Quantorformeln reguliert. Falls Glieder der Sub-
stituendumfolge nicht mit der durch den betreffenden Quantor gebundene Variable iden-
tisch sind, dann soll die Substitution innerhalb der quantifizierten Formel fur und nur fur
diese Glieder der Substituendumfolge durchgefuhrt werden. Dementsprechend mussen in
diesem Fall die erwunschten Substituendumglieder und die ihnen korrespondierenden
Substituensglieder herausgegriffen werden. Dies geschieht durch die (jeweils eindeutig
bestimmte) Zahlenfolge <io, ., is-1>, die gerade die Indizes herausgreift, deren Werte in
der Substituendumfolge verschieden von der gebundenen Variable sind. Durch Komposi-
tion der ursprunglichen Substituendum- resp. Substituensfolgen mit <io, ., is-1> entstehen
dann gerade die neue Substituendum- resp. Substituensfolgen, die die gewunschten Ei-
genschaften haben. Sind dagegen alle Glieder der Substituendumfolge mit der gebunde-
nen Variable identisch, dann soil das Substitutionsergebnis mit dem Substitutionsort -
also der betreffenden Quantorformel - identisch sein.

Nun sind einige Theoreme zu etablieren, die fur die Metatheorie des Redehandlungs-
kalkuls - insbesondere ab Kap. 4 - benotigt werden. Es empfiehlt sich fur den ungeduldi-
geren Leser, diese Theoreme zunachst zu Uberspringen und dann im Bedarfsfall hierher
zuruckzukehren. Zunachst folgt ein Theorem, das Induktionsbeweise uber den Formel-
grad vereinfacht. Es wird mittels Induktion uber den Formelaufbau bewiesen.

Theorem 1-13. Formelgraderhaltung bei Substitution

Wenn θ ∈ GTERM, θ' ∈ ATERM und Δ ∈ FORM, dann FGRAD(Δ) = FGRAD([θ, θ', Δ]).

Beweis: Seien θ ∈ GTERM, θ' ∈ ATERM und Δ ∈ FORM. Der Beweis wird mittels In-
duktion uber den Formelaufbau von Δ gefuhrt. Sei Δ = ^rΦ(θ_o, ., θ∙_-∣Γ ∈ AFORM.
Dann ist nach Definition 1-12 FGRAD(Δ) = o. Dabei gilt [θ, θ', Δ] = [θ, θ', ^rΦ(θ_o, .,
θn-ι)^π ] = ^rΦ([θ, θ', θo], ., [θ, θ', θn-ι])^π ∈ AFORM. Also auch FGRAD([θ, θ', Δ]) = o.

<<   29   30   31   32   33   34   35   >>

More intriguing information