Ein pragmatisierter Kalkul des naturlichen Schlieβens nebst Metatheorie

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^θ₀ = θ₁∣ und [θ₀, ξ, Δ] 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, ft_l) ∈ 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

<<   95   96   97   98   99   100   101   >>

More intriguing information