如何寻找命题演算中公式的证明？为何⊢α→α无法用于证明任意命题？

先把你提到的这套希尔伯特风格命题演算的三条核心公理摆清楚，方便后续讨论：

• 公理(Ak)：α → (β → α)
• 公理(AS)：(α → (β → γ)) → ((α → β ) → (α → γ))
• 公理(A¬)：(¬β → ¬α) → ((¬β → α) → β)

找证明的基本思路 #

在这个系统里构造证明，核心就是从三条公理出发，反复用分离规则（MP：如果已经证出⊢φ和⊢φ→ψ，就能推出⊢ψ）一步步凑出目标公式。分享几个实用小技巧：

1. 先攒一批"通用工具定理"——比如你提到的⊢α→α，还有像⊢¬α∨α、⊢α→¬¬α这类重言式定理，之后证明其他公式时直接用，不用每次都从公理从头推
2. 灵活用代入规则：把公理里的α、β、γ换成任意合法公式，就能得到公理的实例，比如把Ak里的β换成¬α，就能得到α → (¬α → α)
3. 处理带否定的公式时，重点抓公理(A¬)的归谬逻辑：如果能从¬β同时推出α和¬α，那就能证出β

为什么⊢α→α没法证明任意命题？ #

这个问题问到点子上了！⊢α→α确实是系统里的基础定理，但它只是个恒真的重言式，根本不具备"万能推导"的能力，原因主要有两个：

1. 系统的可靠性：这套命题演算系统是"可靠"的——所有能证出来的公式，都是在所有真值指派下都为真的重言式。要是⊢α→α能推出任意命题，那岂不是说所有命题都是重言式？但显然存在像α∧¬α这种矛盾式，或者α这种偶真式（真值随赋值变），它们不是重言式，自然不可能被推导出来。
2. 推导规则的局限性：分离规则MP是单向的，必须同时有⊢φ和⊢φ→ψ，才能得到⊢ψ。⊢α→α本身只是个"自己蕴含自己"的恒真式，它没法和其他公式配合，推导出和α无关的、或者非重言的命题。比如你想证⊢β，光靠⊢α→α根本没辙——没有规则允许你从一个关于α的定理直接跳转到关于β的结论，除非你有额外的前提支撑。

说白了，这套系统是**"保真"的**——它只能从真公理推导出真定理，不是什么阿猫阿狗都能推出来的。

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