Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

6.1 Korrektheit des Redehandlungskalkuls 243

(KBF, AEF): Sei M ∈ KBF(MTDom(M)-1). Nach Definition 3-5 gibt es dann Δ ∈
GFORM, so dass ^rΔ ∧ K(M)^^l ∈ VER(MTDom(M)-1) oder ^rK(⅛) ∧ Δ ∈
VER(MTDom(M)-1). Wegen ^rΔ ∧ K(M)^^l ∈ VER(MTDom(M)-1) oder ∣K(M) ∧ ∆^^l ∈
VER(MTDom(M)-1) gibt es j ∈ Dom(M)-1, so dass ^rΔ ∧ K(M)^^l oder ∣K(M) ∧ ∆^^l in
MTDom(M)-1 bei j verfugbar ist. Dann ist K(MTj+1) = ∣∆ ∧ K(M)^^l oder K(MTj+1) =
∣K(M) ∧ ∆^^l. Dann gilt VAN(MTj+1) = ^rΔ ∧ K(M)^^l oder VAN(MTj+1) = ^rK(Λ) ∧ ∆^^l.
Mit Theorem 3-29-(iv) gilt dann VAN(MTj+1) ⊂ VAN(MTDom(M)-1) = VAN(M) und
damit mit Theorem 5-13 auch VAN(M) = ∣∆ ∧ K(M)^^l oder VAN(M) = ^rK(M) ∧ Δ^η.
Theorem 5-18 ergibt in beiden Fallen VAN(M) = K(M). Analog zeigt man fur AEF mit
Theorem 5-22, dass VAN(M) = K(M).

(ABF): Sei M ∈ ABF(MΓDom(M)-1). Nach Definition 3-9 gibt es dann Β, Δ ∈ GFORM
so dass ∣B V ∆^^l, ∣B → K(M)^^l, r∆ → K(M)^^l ∈ VER(MΓDom(M)-1). Dann gibt es j, k, l ∈
Dom(M)-1, so dass ^rB v ∆^^l in MΓDom(M)-1 bei j und ^rB → K(M)^^l in MΓDom(M)-1 bei k
und ∣∆ → K(M)^^l in MΓDom(M)-1 bei l verfugbar ist. Dann ist K(MTj+1) = ∣B v ∆^^l und
K(MΓk+1) = ∣B → K(M)^^l und K(Mtl+1) = ∣∆ → K(M)^^l. Dann gilt VAN(MTj+1) = ∣B v
∆^^l und VAN(MΓk+1) = ∣B → K(M)^^l und VAN(MTl+1) = ∣∆ → K(M)^^l. Mit Theorem
3-29-(iv) gilt sodann VAN(MΓj+1) ⊆ VAN(MΓDom(M)-1) und VAN(MΓk+1) ⊂
VAN(MΓDom(M)-1) und VAN(MTl+1) ⊆ VΛ∖(Mi□om(M)-1) und damit VAN(MTj+1) ⊆
VAN(M) und VAN(MΓk+1) ⊂ VAN(M) und VAN(MTl+1) ⊆ VAN(M). Damit gilt mit
Theorem 5-13 auch VAN(M) = ∣B v ∆^^l und VAN(M) = ∣B → K(M)^^l und VAN(M) =
∣∆ → K(M)^^l. Theorem 5-23 ergibt VAN(M) = K(M).

(NBF, UBF, PEF): Sei M ∈ NBF(MΓDom(M)-1). Nach Definition 3-11 ist dann
r—i—ιK(M)^^l ∈ VER(MΓDom(M)-1). Sodann gibt es j ∈ Dom(M)-1, so dass ∣- K(M)^^l in
MTDom(M)-1 bei j verfugbar ist. Dann ist K(MTj+1) = ∣--K(M)^^l. Dann gilt
VAN(MTj+1) = Г-—K(M)^π. Mit Theorem 3-29-(iv) gilt sodann VAN(MTj+1) ⊆
VAN(MTDom(M)-1) = VAN(M) und daher mit Theorem 5-13 auch VAN(M) =
Г-—K(M)^π. Theorem 5-26 ergibt VAN(M) = K(M). Analog zeigt man fur UBF mit
Theorem 5-28 und fur PEF mit Theorem 5-29, dass dann auch jeweils VAN(M) = K(M).

(UEF): Sei M ∈ UEF(MTDom(M)-1). Nach Definition 3-12 gibt es dann β ∈ PAR, ξ ∈
VAR und ∆ ∈ FORM, wobei FV(∆) ⊂ {ξ}, so dass [β, ξ, ∆] ∈ VER(MTDom(M)-1) und β
∉ TTFM({∆} и VAN(MTDom(M)-1)) und K(M) = ∣Λξ∆^π. Dann gibt es j ∈ Dom(M)-1,
so dass [β, ξ, ∆] in MTDom(M)-1 bei j verfugbar ist. Dann ist K(MTj+1) = [β, ξ, ∆]. Dann
gilt VAN(MTj+1) = [β, ξ, ∆]. Mit Theorem 3-29-(iv) gilt sodann VAN(MTj+1) ⊆

<<   213   214   215   216   217   218   219   >>

More intriguing information