Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

106   2 Verfugbarkeit von Aussagen

Theorem 2-75. VANS-Inklusion impliziert VAN-Inklusion

Wenn й, й ∈ SEQ und VANS(⅛) ⊆ VANS(⅛'), dann VAN(^) ⊆ VAN(⅛').

Beweis: Seien й, й'е SEQ und sei VANS(#) ⊆ VANS(#'). Sei nun Γ ∈ VAN(#). Dann
gibt es ein i ∈ Dom(VANS(⅛)) und Γ = A(W). Dann ist (i, йі) ∈ VANS(#). Nach Vo-
raussetzung ist dann (і, й) ∈ VANS(W). Nun ist VANS(W) ⊆ й' und somit (і, йї) ∈ й'
und also йі = йї Somit ist Γ = А(йі) = A(W«). Also ist insgesamt і ∈ Dom(VANS(W))
und Γ = А(й'і). Also ist Γ ∈ VAN(W). ■

Theorem 2-76. VAN ist hochstens so groβ wie VANS

Fur alle й ∈ SEQ: |VAN(£)| ≤ |VANS(£)|.

Beweis: Sei й ∈ SEQ. Nach Definition 2-31 ist dann f : VAN(⅛) → VANS(⅛), f(Γ) =
(тт({і | і ∈ Dom(VANS(£)) und А(йі) = Γ}), Wmin({j ∣ і ∈ Dom(VANS(⅛)) und А(йі) = Γ})) eine In-
jektion von VAN(⅛) in VANS(⅛). ■

Theorem 2-77. VAN ist dann und nur dann leer, wenn auch VANS leer ist

Fur alle й ∈ SEQ: |VAN(£)| = 0 gdw |VANS(£)| = 0.

Beweis: Sei й ∈ SEQ. Sei |VAN(^)| ≠ 0. Dann ist mit Theorem 2-76 auch |VANS(^)| ≠
0. Sei nun |VANS(W| ≠ 0. Dann gibt es (і, W) ∈ VANS(⅛) und mit Definition 2-31 ist
dann A(W) ∈ VANW) und damit |VAN(^)| ≠ 0. Damit ist insgesamt |VAN(W)| ≠ 0 gdw
|VANS(W| ≠ 0, woraus sich unmittelbar die Behauptung ergibt. ■

Theorem 2-78. Bei non-redundantem VANS ist jede Annahme an genau einer Stelle als An-
nahme verfugbar

Wenn й ∈ SEQ und |VAN($)| = |VANS($)|, dann gilt fur alle Γ ∈ VAN(W): Es gibt genau
ein j ∈ Dom(VANSW)), so dass Γ = A(Wj).

Beweis: Sei й ∈ SEQ und |VANW)| = |VANSW)|. Dann gilt nach Theorem 2-70-(ii),
dass VANSW) ⊆ й und damit mit й ∈ SEQ und Definition 1-24 und Definition 1-23,
dass |VAN(#)| = |VANS(#)| = k fur ein k ∈ N. Sei nun Γ ∈ VAN(W). Dann ist k > 0. So-
dann gibt es nach Definition 2-31 ein j ∈ Dom(VANSW)), so dass Γ = A(Wj). Sei nun і
∈ Dom(VANS(W)) und Γ = A(W). Ware nun і ≠ j. Dann ist |VANS(W)\{(j, й^)}| = k-1
und andererseits ist f : VAN(W) → VANS(W)∖{(j', Wj)}, f(Β) = (min({l | l ∈
Dom(VANS(£)\{(j, Wj)}) und A(W) = Β}), Wmin({l | l ∈ Dom(VANS(⅛)∖{(j, й,)}) und А(йі) = Β})) eine

<<   81   82   83   84   85   86   87   >>

More intriguing information