Mathematical-Logic5

Before：Raytracing ing!Build my first ppm file!I ❤️ Computer Graphics!

Mathematical Logic 5 Left Proof of Substitution Lemma 替换引理 & Sequent Calculus (I)  序列演算

Left Proof of Substitution Lemma 替换引理

对于项的替换引理证明还是比较直观容易的：

但对于公式来说，需要对公式进行归纳，这就有一定的难度了（特别是对∃的证明），外加由于此博客的Markdown渲染器并未配好(upd:配好了，也是终于能用Tex了)，就偷个懒直接了lecture-notes的图了🤡

Sequent Calculus Basic Defintion

把证明当作数学对象来研究，这里的Sequent Calculus就是一种我们建立起来的证明系统。从已有的antecedent得到新的succedent。
$
Γ ⊢ Δ
$
Γ 是前提集合，Δ是结论集合而Sequent Calculus要做的就是，设计一个演算系统，通过一系列规则从已知的序列推导出新的序列。

Sequent Rule 序列规则的形式

$
\frac{Γ_1 φ_1…Γ_n φ_n}{Γ’ φ}
$

Derivability 可推导性

如果可以从 Γ 推出 $\phi$ ，则记作
$
⊢ \Gamma \phi
$
这称为可推导

如果存在有限个公式
$
\phi_1 \phi_2 … \phi_n \in \Phi
$
使得
$
⊢ \phi_1 \phi_2 … \phi_n \phi
$
则称作公式$\phi$可从公式集$\Phi$中形式化证明或推导，记作
$
\Phi ⊢ \phi
$

Correctness 正确性

A sequent $\Gamma$ $\phi$ is correct if
$
{\psi | \psi \in \Gamma} ⊢ \phi
$
即我们需要序列$\Gamma$中的所有公式都满足$\phi$，才能得到$\Gamma$ ⊢ $\phi$
引入的规则必须保证只产生正确的序列

Structure Rules 结构规则

Antecedent 前提规则

$
\frac{Γ ⊢ φ}{Γ’ ⊢ φ} \quad Γ ⊆ Γ’
$
如果某个结论可以从一组前提中推导出来，那么它也可以从更大的前提集合中推导出来。我们可以在推导过程中增加前提

Assumption

$
\frac{}{\Gamma \vdash \varphi} \quad \text{如果 } \varphi \in \Gamma
$
如果某个公式已经是前提集合的一部分，那么它可以直接作为结论。换句话说，假设规则允许我们直接从前提集合中"提取"已知的公式作为结论，而无需进一步的推导。

Connective Rules 连接词规则

Case Analysis 案例分析规则

我觉得就是分类讨论（遍历所有情况）
$
\frac{\Gamma, \psi \vdash \varphi \quad \Gamma, \neg \psi \vdash \varphi}{\Gamma \vdash \varphi}
$
如果从前提集合和某个假设 𝜓可以推导出结论 𝜑，并且从前提集合和 ¬𝜓也可以推导出𝜑，那么可以直接从前提集合推导出𝜑

Contradiction 矛盾规则

我觉得就是反证的思想推出矛盾
$
\frac{\Gamma, \neg \varphi \vdash \psi \quad \Gamma, \neg \varphi \vdash \neg \psi}{\Gamma \vdash \varphi}
$
如果从前提集合和 ¬𝜑可以推导出 𝜓和 ¬𝜓，那么可以直接从前提集合推导出 𝜑。

v-introduction in antecedent 析取引入规则(前提版)

$
\frac{\Gamma, \varphi \vdash \chi \quad \Gamma, \psi \vdash \chi}{\Gamma, \varphi \vee \psi \vdash \chi}
$
如果无论 𝜑为真还是 𝜓为真，𝜒都成立，那么从 𝜑∨𝜓（即 𝜑或𝜓中至少有一个为真）也可以推导出 𝜒。

v-introduction in succedent 析取引入规则(结论版)

$
\frac{\Gamma \vdash \varphi}{\Gamma \vdash \varphi \vee \psi} \quad \text{or} \quad \frac{\Gamma \vdash \psi}{\Gamma \vdash \varphi \vee \psi}
$
如果𝜑为真，则𝜑∨𝜓也为真；如果𝜓为真，则𝜑∨𝜓也为真；因此只要𝜑和𝜓中的一个为真，𝜑∨𝜓就为真

Derived Rules 派生规则（可通过结构规则、连接词规则证明）

排中律 Law of Excluded Middle

$
\vdash \varphi \vee \neg \varphi
$
对于任何命题 𝜑，$ \varphi \vee \neg \varphi$ 总是为真。也就是说，任何命题要么为真，要么为假，不存在中间状态

修改的矛盾规则 Modified Contradiction

$
\frac{\Gamma \vdash \psi \quad \Gamma \vdash \neg \psi}{\Gamma \vdash \varphi}
$
如果从前提集合 $\Gamma $ 可以推导出 $ \psi $，并且从前提集合 $ \Gamma $ 也可以推导出 $ \neg \psi $，那么可以直接从 $ \Gamma $ 推导出 $ \varphi $。

链式推理 Chain Deduction

$
\frac{\Gamma \vdash \varphi \quad \Gamma, \varphi \vdash \psi}{\Gamma \vdash \psi}
$
通过中间步骤 $ \varphi $，可以将前提集合 $ \Gamma $ 与结论 $ \psi $ 连接起来，形成一个推理链。

Quantifier Rules 量词规则

∃-introduction in succedent(结论版)

$
\frac{\Gamma \vdash \varphi(t/x)}{\Gamma \vdash \exists x \varphi}
$
如果存在一个具体的项 t ，使得 $ \varphi(t/x) $ 成立，那么可以推导出存在量词 $ \exists x \varphi $。

∃-introduction in antecedent(前提版)

$
\frac{\Gamma, \varphi(y/x) \vdash \psi}{\Gamma, \exists x \varphi \vdash \psi} \quad \text{如果 } y \notin \text{free}(\Gamma \cup {\exists x \varphi, \psi})
$
通过引入一个新的变量 y ，可以将存在量词 $ \exists x \varphi $ 引入前提中，从而推导出 $ \psi $。
变量y选取的重要性（如果变量选取不当，可能会导致逻辑错误）
y 必须是一个新变量，不能在其他地方自由出现

Equality Rules 等式规则

Equality 等式的基本规则

$
t \equiv t
$
等式的基本规则表明任何项 𝑡 都等于它自身。

Substitution 替换规则

$
\frac{\Gamma \vdash t \equiv t’ \quad \Gamma \vdash \varphi(t/x)}{\Gamma \vdash \varphi(t’/x)}
$
如果两个项 t 和 t’ 相等，那么在任何公式中，可以用 t’ 替换 t ，而不改变公式的真值。

Soundness 可靠性定理

$
\text{如果 } \Phi \vdash \varphi, \text{ 则 } \Phi \models \varphi.
$
如果从前提集合 $ \Phi $ 可以形式化推导出 $ \varphi $，那么 $ \varphi $ 在语义上也成立。也就是说，形式化推导的结果在语义上是正确的。