3.1 Der Kalkul 121
man r——Γ gewonnen, dann darf man Γ folgern (NB); hat man [β, ξ, Δ] gewonnen, wo-
bei β kein Teilterm von Δ oder von einer verfugbaren Annahme ist, dann darf man rΛξΔ^l
folgern (UE), hat man rΛξΔ^l gewonnen, dann darf man [θ, ξ, Δ] folgern (UB); hat man
[θ, ξ, Δ] gewonnen, dann darf man rVξΔ^l folgern (PE); hat man rVξΔ^l gewonnen, als
nachstes [β, ξ, Δ] angenommen, wobei β ein neuer Parameter und kein Teilterm von Δ ist,
und dann im Ausgang von der Annahme von [β, ξ, Δ] als letztes Γ gewonnen, wobei β
kein Teilterm von Γist, dann darf man Γfolgern und sich so von der Annahme von [β, ξ,
Δ] befreien (PB); man darf l^θ = θ∣ folgern (IE); hat man l^θ0 = θ1∣ und [θ0, ξ, Δ] gewon-
nen, dann darf man [θ1, ξ, Δ] folgern (IB); das ist alles, was man darf (IDK).
Es folgen nun die Regeln des Redehandlungskalkuls in ihrer verbindlichen Formulie-
rung:
Handlungsanleitung 3-1. Annahmeregel (AR)
Wenn man ft ∈ SEQ geauβert hat und Γ ∈ GFORM, dann darf man ft zu ft ∪ {(Dom(ft), rSei
Γ)} fortsetzen.
Handlungsanleitung 3-2. Subjunktoreinfuhrungsregel (SE)
Wenn man ft ∈ SEQ geauβert hat, Δ, Γ ∈ GFORM und i ∈ Dom(ft) und
(i) A(fti) = Δ und (i, fti) ∈ VANS(ft),
(11) A‰mw)-1) = Γ und
(iii) Es kein l mit i < l ≤ Dom(ft)-1 gibt, so dass (l, ftl) ∈ VANS(ft),
dann darf man ft zu ft ∪ {(Dom(ft), rʌlso Δ → Γl)} fortsetzen.
Man beachte, dass die Anwendung der Subjunktoreinfuhrungsregel SE-geschlossene Ab-
schnitte gemaβ Definition 2-23 erzeugt (vgl. Theorem 2-91). Setzt man ft mittels SE zu ft
∪ {(Dom(ft), rAlso Δ → Γ∣)} fort, so ist daher in ft ∪ {(Dom(ft), rAlso Δ → Γ∣)} keine
der bei der Auβerung von ft ab (einschlieβlich) dem i-ten Glied gefolgerten oder ange-
nommenen Aussagen verfugbar, es sei denn, die Aussage war in ft schon vor dem i-ten
Glied verfugbar (vgl. Definition 2-26). Davon ist naturlich die neuerdings verfugbare
Subjunktion rΔ → Γ ausgenommen, da sie die Aussage des neuen letzten Gliedes bildet
und damit in jedem Fall in der nun insgesamt geauβerten Sequenz verfugbar ist (vgl.
Theorem 2-82). Da die Aussage des letzten Gliedes einer Sequenz ft in ft immer bei
Dom(ft)-1 verfugbar ist, reicht es auch, in Klausel (ii) der Regel zu fordern, dass das
Sukzedens der zu folgernden Subjunktion die Aussage des letzten Gliedes von ft ist, ohne