Formal System-相继式演算(Sequenz)

同样是用于解决不可实现问题(unerfüllbarkeit)，不同于Tabeau适用于纯手写和resolution的自动化。这个方法介于两者之间。他需要手动选择具体的操作方法，然后又电脑实现具体的方法。

另外这个方法是由Tebleau方法转变过来的，所以估计思路是差不多的。

定义

Sequenz是一对用下面方式表示的有限的公式(Formel)集：

Γ⇒Δ
\Gamma \Rightarrow \Delta

其中：

Γ\Gamma和Δ\Delta都可以是空集

已知D为一个谓词逻辑结构(//不该是指值域吗？？),β\beta为一个断言，那么就有：

valD,β(Γ⇒Δ)=valD,β(⋀Γ→⋁Δ)
val_{D,\beta}(\Gamma \Rightarrow \Delta)=val_{D,\beta}(\bigwedge\Gamma \rightarrow \bigvee \Delta)

上式同样适用于空集

(Es gelten die üblichen Vereinbarungen für leere Disjunktionen und Konjunktionen)

表达逻辑的相继公理和规则

axiom:Γ,F⇒F,Δnot−left:Γ⇒F,ΔΓ,¬F⇒Δnot−right:Γ,F⇒ΔΓ⇒¬F,Δimpl−left:Γ⇒F,Δ Γ,G⇒ΔΓ,F→G⇒Δimpl−right:Γ,F⇒G,ΔΓ⇒F→G,Δand−left:Γ,F,G⇒ΔΓ,F∧G⇒Δand−right:Γ⇒F,Δ Γ⇒G,ΔΓ⇒F∧G,Δor−left:Γ,F⇒Δ Γ,G⇒ΔΓ,F∨G⇒Δor−right:Γ⇒F,G,ΔΓ⇒F∨G,Δ
axiom: \frac{}{\Gamma,F\Rightarrow F,\Delta}\\
not-left:\frac{\Gamma\Rightarrow F,\Delta}{\Gamma,\lnot F\Rightarrow \Delta}\\
not-right:\frac{\Gamma,F\Rightarrow\Delta}{\Gamma\Rightarrow \lnot F,\Delta}\\
impl-left:\frac{\Gamma \Rightarrow F,\Delta\ \ \ \Gamma,G\Rightarrow \Delta}{\Gamma,F\rightarrow G\Rightarrow \Delta}\\
impl-right:\frac{\Gamma,F\Rightarrow G,\Delta}{\Gamma \Rightarrow F \rightarrow G,\Delta}\\
and-left:\frac{\Gamma,F,G\Rightarrow\Delta}{\Gamma,F\land G\Rightarrow \Delta}\\
and-right:\frac{\Gamma\Rightarrow F,\Delta\ \ \ \Gamma\Rightarrow G,\Delta}{\Gamma\Rightarrow F\land G,\Delta}\\
or-left:\frac{\Gamma,F\Rightarrow \Delta\ \ \ \Gamma,G\Rightarrow \Delta}{\Gamma,F\lor G\Rightarrow \Delta}\\
or-right:\frac{\Gamma\Rightarrow F,G,\Delta}{\Gamma\Rightarrow F\lor G,\Delta}

谓词逻辑的相继规则

all-left:

Γ,∀xF,{x/X}F⇒ΔΓ,∀xF⇒Δ
\frac{\Gamma,\forall x F,\{x/X\}F\Rightarrow \Delta}{\Gamma,\forall xF\Rightarrow \Delta}

其中X是一个新的变量

all-right:

Γ⇒{x/f(x⎯⎯)}F,ΔΓ⇒∀xF,Δ
\frac{\Gamma\Rightarrow\{x/f(\overline{x})\}F,\Delta}{\Gamma\Rightarrow \forall x F,\Delta}

其中：

f是新的函数符号

x⎯⎯=x1,...,xn\overline{x}=x_1,...,x_n表示∀xF\forall xF中的所有自由变量

ex-right:

Γ⇒∃xF,{x/X}F,ΔΓ⇒∃xF,Δ
\frac{\Gamma\Rightarrow \exists xF,\{x/X\}F,\Delta}{\Gamma\Rightarrow \exists xF,\Delta}

其中X为新的变量

ex-left:

Γ,{x/f(x⎯⎯)}F⇒ΔΓ,∃xF⇒Δ
\frac{\Gamma,\{x/f(\overline{x})\}F\Rightarrow \Delta}{\Gamma,\exists xF\Rightarrow \Delta}

其中：

f为新的函数符号

x⎯⎯=x1,...,xn\overline{x}=x_1,...,x_n为∃xF\exists xF中的所有的自由变量

//为什么会是这样，还有点晕

等式的相继规则和公理

identity−right:Γ⇒s≐s,Δsymmetry−right:Γ⇒s≐t,ΔΓ⇒t≐s,Δsymmetry−left:Γ,s≐t⇒ΔΓ,t≐s⇒Δeq−subst−right:Γ,s≐t⇒F(t),ΔΓ,s≐t⇒F(s),Δeq−subst−left:Γ,F(t),s≐t⇒ΔΓ,F(s),s≐t⇒Δ
identity-right:\frac{}{\Gamma\Rightarrow s\doteq s,\Delta}\\
symmetry-right:\frac{\Gamma\Rightarrow s\doteq t,\Delta}{\Gamma\Rightarrow t\doteq s,\Delta}\\
symmetry-left:\frac{\Gamma,s\doteq t\Rightarrow \Delta}{\Gamma,t\doteq s \Rightarrow \Delta}\\
eq-subst-right:\frac{\Gamma,s\doteq t\Rightarrow F(t),\Delta}{\Gamma,s\doteq t\Rightarrow F(s),\Delta}\\
eq-subst-left:\frac{\Gamma,F(t),s\doteq t\Rightarrow \Delta}{\Gamma,F(s),s\doteq t\Rightarrow \Delta}

相继式的推导树

推导树就是一个树结构，他的每个节点都用Sequence标志，其中：

1.加入节点n有且仅有一个子节点n’，且n和n’分别用“Γ⇒Δ\Gamma\Rightarrow \Delta”“Γ1⇒Δ1\Gamma_1\Rightarrow\Delta_1”标志，那么对应的就有下面的相继规则：

Γ1⇒Δ1Γ⇒Δ
\frac{\Gamma_1\Rightarrow \Delta_1}{\Gamma\Rightarrow\Delta}

2.如果节点n有且仅有两个子节点n1,n2n_1,n_2，他们分别标识为：Γ⇒Δ,Γ1⇒Δ1,Γ2⇒Δ2\Gamma\Rightarrow \Delta,\Gamma_1\Rightarrow\Delta_1,\Gamma_2\Rightarrow\Delta_2，那么对应的就有下面这个相继规则：

Γ1⇒Δ1 Γ2⇒Δ2Γ⇒Δ
\frac{\Gamma_1\Rightarrow\Delta_1\ \ \ \ \Gamma_2\Rightarrow\Delta_2}{\Gamma\Rightarrow\Delta}

3.存在一个替换σ\sigma，他可以使得对于每一个不存在子节点的节点n的标识A，σ(A)\sigma(A)为一个公理。

/*

Man beachte daß zunächst A≡p(s)⇒p(t)\equiv p(s)\Rightarrow p(t) kein Axiom zu sein braucht

ist σ\sigma aber ein Unifikator von s und t dann ist σ(A)\equivp(σ(S))⇒p(σ(t))\sigma(A)\equivp(\sigma(S))\Rightarrow p(\sigma(t))zu einem Axiom wird.

*/

两条定理

已知M⊆For∑,A∈For∑M \subseteq For_\sum,A\in For_\sum,那么就有：

M⊢sA⇒M⊨A
M\vdash_s A \Rightarrow M\models A

已知M⊆For∑,A∈For∑M \subseteq For_\sum,A\in For_\sum,那么就有：

M⊨A⇒M⊢sA
M\models A \Rightarrow M\vdash_s A