Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

4.1 Vorbereitungen 163

(v)   Dom(VERS(⅛*)) =

Dom(VERS(⅛)) и {Dom(^)} и {Dom(^)+1+l | l ∈ Dom(VERS(⅛'))},

(vi)  VER(⅛*) = VER(^) и {^rα = α¹} и VER(⅛') und

(vii) VAN(⅛*) = VAN(^) и {^rα = α¹} и VAN(⅛^,).

Beweis: Durch Induktion uber Dom(>Y) wird gezeigt, dass es unter den entsprechenden
Voraussetzungen immer ein ⅛* gibt, dass (i) bis (v) erfullt. (vi) und (vii) ergeben sich aus
den vorhergehenden Klauseln. Mit (i) bis (v) gilt namlich mit Definition 2-30:

Β ∈ VER(⅛*)

gdw

es gibt ein i ∈ Dom(VERS(⅛*)), so dass Β = A(⅛*_i)

gdw

es gibt ein i ∈ Dom(VERS(⅛)) и {Dom(⅛)} и {Dom(⅛)+1+l | l ∈ Dom(VERS(⅛'))}, so
dass Β = A(⅛*_i)

gdw

Β ∈ VER(^) и {^rα = α¹} и VER(⅛').

Sodann ergibt sich (vii) aus (i) bis (v) mit Definition 2-31 wie folgt:

Β ∈ VAN(⅛*)

gdw

es gibt ein i ∈ Dom(VANS(⅛*)), so dass Β = A(⅛*_i)

gdw

es gibt ein i ∈ Dom(VERS(⅛*)) ∩ Dom(ANS(⅛*)), so dass Β = A(⅛*_i)
gdw

es gibt ein i ∈ (Dom(VERS(⅛)) и {Dom(⅛)} и {Dom(⅛)+1+l | l ∈ Dom(VERS(⅛'))})
∩ Dom(ANS(⅛*)), so dass Β = A(⅛*_i)
gdw

es gibt ein i ∈ (Dom(VERS(⅛)) ∩ Dom(ANS(⅛*))) и ({Dom(⅛)} ∩ Dom(ANS(⅛*))) и
({Dom(^)+1+l | l ∈ Dom(VERS(⅛'))} ∩ Dom(ANS(⅛*))), so dass Β = A(^*≈)
gdw

es gibt ein i ∈ (Dom(VERS(⅛)) ∩ Dom(ANS(⅛))) и ({Dom(⅛)} ∩ Dom(ANS(⅛*))) и
({Dom(⅛)+1+l | l ∈ Dom(VERS(⅛'))} ∩ {Dom(⅛)+1+l | l ∈ Dom(ANS⅛'))}), so dass
Β = A(^*i)
gdw

es gibt ein i ∈ Dom(VANS(⅛)) и {Dom(⅛)} и ({Dom(⅛)+1+l | l ∈ Dom(VANS(⅛'))},
so dass Β = A(⅛*_i)
gdw

Β ∈ VAN(⅛) и {^rα = α¹} и VAN(⅛').

<<   136   137   138   139   140   141   142   >>

More intriguing information