基于希尔伯特系统公理证明⊢(P→¬P)→(¬¬P→¬P)的技术问询

我明白你在希尔伯特系统里反复尝试证明这个公式却卡壳的挫败感——希尔伯特系统的公理推导确实需要精准的变量替换和规则应用，尤其是要学会利用已证定理来简化步骤。下面我会一步步带你完成这个证明，先从最直观的演绎定理方法入手（因为它能大幅降低推导复杂度），再补充纯公理序列的版本供你参考。

先明确已知条件 #

首先把我们能用的公理和已证定理列出来，方便随时查阅：

• 公理1：$P \implies (Q \implies P)$（弱化规则：任何命题都能被另一个命题蕴涵）
• 公理2：$(P \implies (Q \implies R)) \implies ((P \implies Q) \implies (P \implies R))$（蕴涵分配规则）
• 公理3：$(\neg Q \implies \neg P) \implies (P \implies Q)$（逆否规则）
• 已证定理1：$P \implies \neg \neg P$（双重否定引入）
• 已证定理2：$\neg \neg P \implies P$（双重否定消去）
• 已证定理3：$(P \implies \neg P) \implies \neg P$（矛盾导出否定）

方法一：利用演绎定理简化证明 #

希尔伯特系统的演绎定理是个强大工具：如果从假设集合$\Gamma \cup {A}$能推出$B$，那么$\Gamma$能推出$A \implies B$。这里我们的$\Gamma$是空集，目标是证明$\vdash (P→¬P)→(¬¬P→¬P)$，所以只需证明${(P→¬P)} \vdash (¬¬P→¬P)$，再应用演绎定理即可。

具体推导步骤：

1. 假设前提：我们先假设$(P \implies \neg P)$成立
   $$P \implies \neg P \tag{假设}$$
2. 应用已证定理3：结合假设和定理3$(P \implies \neg P) \implies \neg P$，用分离规则（MP）（若$\vdash A$且$\vdash A→B$，则$\vdash B$），直接得到$\neg P$：
   $$\neg P \tag{MP: 1, 定理3}$$
3. 公理1实例：把公理1中的$P$替换为$\neg P$，$Q$替换为$\neg \neg P$，得到：
   $$\neg P \implies (\neg \neg P \implies \neg P) \tag{公理1实例}$$
4. 再次应用分离规则：结合步骤2的$\neg P$和步骤3的公式，得到目标结论：
   $$\neg \neg P \implies \neg P \tag{MP: 2, 3}$$

现在，我们从假设$(P→¬P)$推出了$(¬¬P→¬P)$，根据演绎定理，直接可得：
$$\vdash (P \implies \neg P) \implies (\neg \neg P \implies \neg P)$$

方法二：纯公理序列证明（无演绎定理） #

如果需要完全不依赖演绎定理，直接用公理和分离规则构造证明序列，我们可以把演绎定理的推导过程转化为公理组合，核心是利用蕴涵传递性（这个引理可以用公理1和公理2证明）：

先证明中间引理：蕴涵传递性 $\vdash (A→B)→((B→C)→(A→C))$ #

1. 公理1实例：$(B \implies C) \implies (A \implies (B \implies C))$
2. 公理2实例：$(A \implies (B \implies C)) \implies ((A \implies B) \implies (A \implies C))$
3. 结合步骤1和2，通过分离规则的传递性可推导出：
   $$(B \implies C) \implies ((A \implies B) \implies (A \implies C))$$
4. 替换变量调整前件顺序，最终得到：
   $$(A \implies B) \implies ((B \implies C) \implies (A \implies C))$$

正式证明目标公式 #

1. 已证定理3：$(P \implies \neg P) \implies \neg P$
2. 公理1实例：$\neg P \implies (\neg \neg P \implies \neg P)$
3. 应用蕴涵传递性引理（令$A=(P→¬P), B=\neg P, C=(¬¬P→¬P)$），得到：
   $$[(P \implies \neg P) \implies \neg P] \implies [(\neg P \implies (\neg \neg P \implies \neg P)) \implies ((P \implies \neg P) \implies (\neg \neg P \implies \neg P))]$$
4. 对步骤1和步骤3应用分离规则，得到：
   $$(\neg P \implies (\neg \neg P \implies \neg P)) \implies ((P \implies \neg P) \implies (\neg \neg P \implies \neg P))$$
5. 对步骤2和步骤4应用分离规则，最终得到目标公式：
   $$(P \implies \neg P) \implies (\neg \neg P \implies \neg P)$$

内容的提问来源于stack exchange，提问作者Yulia23576