Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

3.1 Der Kalkul 125

Handlungsanleitung 3-16. Identitatseinfuhrungsregel (IE)

Wenn man й ∈ SEQ geauBert hat und θ ∈ GTERM, dann darf man й zu й ∪ {(Dom(⅛), ^rAl-
so θ = θ∣)} fortsetzen.

Handlungsanleitung 3-17. Identitatsbeseitigungsregel (IB)

Wenn man й ∈ SEQ geauBert hat, ξ ∈ VAR, Δ ∈ FORM, wobei FV(Δ) ⊂ {ξ}, θ₀, θ₁ ∈
GTERM und {^rθ₀ = θ₁^^l, [θ₀, ξ, Δ]} ⊂ VER(⅛), dann darf man й zu й ∪ {(Dom(⅛), rAlso
[θ₁, ξ, Δ∣∣)} fortsetzen.

Zuletzt wird ein Verbot gesetzt, das den interdiktionalen Status des Reglements explizit
macht. Dazu werden fur die Fortsetzung von й zu й' alle 17 Regelantezedentia als uner-
fullt vorausgesetzt. Dieser Zustand ist dann hinreichend dafur, dass man й nicht zu й'
fortsetzen darf.

Handlungsanleitung 3-18. Interdiktionsklausel (IDK)

Wenn й ∉ SEQ oder wenn man й nicht geauBert hat oder wenn es keine B, Γ, Δ ∈ GFORM
und θo, θι ∈ GTERM und β ∈ PAR und ξ ∈ VAR und Δ' ∈ FORM, wobei FV(Δ') ⊂ {ξ}, und
i, j ∈ Dom(⅛) gibt, so dass

(i) й' = й и {(Dom« rSei Γ ∣)} oder

(ii)   A(&) = Δ, (i, ⅛) ∈ VANS(⅛), A(‰m(s>ι) = Γ, es kein l mit i < l ≤ Dom(⅛)-1 gibt,

so dass (l, й₁) ∈ VANS(⅛), und й' = й ∪ {(Dom(⅛), rAlso Δ → Γ)} oder

(iii)   {Δ, ^rΔ → Γ} ⊂ VER(⅛) und й' = й и {(Dom(⅛), rAlso Γ)} oder

(iv)   {Δ, Γ} ⊂ VER(⅛) und й' = й и {(Dom($), rAlso Δ ∧ Γ)} oder

(v)   {rΔ ∧ Γ¹, T ∧ .∖^l} ∩ VER(£) ≠ 0 und й' = й ∪ {(Dom(£), rAlso Γ¹)} oder

(vi) {rΔ → Γ∣, T → Δ∣} ⊂ VER(£) und й' = й ∪ {(Dom(£), rAlso Δ θ Γ¹)} oder

(vii) Δ ∈ VER($), { rΔ θ Γ∣, T θ Δ∣} ∩ VER($) ≠ 0 und й' = й ∪ {(Dom($), rAlso
Γ∣)} oder

(viii) {Δ, Γ} ∩ VER($) ≠ 0 und й' = й ∪ {(Dom($), rAlso Δ v Γ∣)} oder

(ix)   {rB v Δ∣, rB → Γ∣, rΔ → Γ¹} ⊂ VER(£)und й' = Й ∪ {(Dom(£), rAlso Γ∣)} oder

(x)   i ≤ j, A(⅛) = Δ, (i, йі) ∈ VANS(M A(⅛∙) = Γ und A‰m_w)-ι) =   Γ ∣ oder A(⅛∙) =

r—Γ∣ und A(‰_om(⅛)_-1) = Γ, (j, йу) ∈ VERS^), es kein l mit i < l ≤ Dom(Ei)-I gibt, so
dass (l, й₁) ∈ VANS^), und й' = й ∪ {(Dom^), rAlso — Δ∣)} oder

(xi)   r——γ∣ ∈ VER^) und й' = й ∪ {(Dom^), rAlso Γ∣)} oder

(xii) [β, ξ, Δ'] ∈ VER(M β ∉ TTFM({Δ'} и VAN(^) und й' = й ∪ {(Dom^), rAlso
ΛξΔ'∣)} oder

(xiii) rΛξΔ'∣ ∈ VER(Й) und й' = й U {(Dom^), rAlso [θo, ξ, Δ']∣)} oder

(xiv) [θo, ξ, Δ'] ∈ VERΦ) und й' = й U {(Dom^), rAlso VξΔ'∣)} oder

<<   99   100   101   102   103   104   105   >>

More intriguing information