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(Δ) ⊂ {ξ}, θ0, θ1 ∈
GTERM und {rθ0 = θ1^l, [θ0, ξ, Δ]} ⊂ VER(⅛), dann darf man й zu й ∪ {(Dom(⅛), rAlso
[θ1, ξ, Δ∣∣)} 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, й1) ∈ VANS(⅛), und й' = й ∪ {(Dom(⅛), rAlso Δ → Γ)} oder
(iii) {Δ, rΔ → Γ} ⊂ VER(⅛) und й' = й и {(Dom(⅛), rAlso Γ)} oder
(iv) {Δ, Γ} ⊂ VER(⅛) und й' = й и {(Dom($), rAlso Δ ∧ Γ)} oder
(v) {rΔ ∧ Γ1, T ∧ .∖l} ∩ VER(£) ≠ 0 und й' = й ∪ {(Dom(£), rAlso Γ1)} oder
(vi) {rΔ → Γ∣, T → Δ∣} ⊂ VER(£) und й' = й ∪ {(Dom(£), rAlso Δ θ Γ1)} oder
(vii) Δ ∈ VER($), { rΔ θ Γ∣, T θ Δ∣} ∩ VER($) ≠ 0 und й' = й ∪ {(Dom($), rAlso
Γ∣)} oder
(viii) {Δ, Γ} ∩ VER($) ≠ 0 und й' = й ∪ {(Dom($), rAlso Δ v Γ∣)} oder
(ix) {rB v Δ∣, rB → Γ∣, rΔ → Γ1} ⊂ VER(£)und й' = Й ∪ {(Dom(£), rAlso Γ∣)} oder
(x) i ≤ j, A(⅛) = Δ, (i, йі) ∈ VANS(M A(⅛∙) = Γ und A‰mw)-ι) = Γ ∣ oder A(⅛∙) =
r—Γ∣ und A(‰om(⅛)-1) = Γ, (j, йу) ∈ VERS^), es kein l mit i < l ≤ Dom(Ei)-I gibt, so
dass (l, й1) ∈ 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