基础语法指南
动手实践
我们已经知道怎么推出一些简单的结论：先写下前提，然后运用推理规则逐步推导出更多公式，直到得出结论。
现在，请尝试为以下问题编写证明，确保你掌握了核心要点！
练习 1
证明公式序列 p, p -> q, p -> (q -> r) ⊢ r 是有效的。
要证明这个，我们需要使用 蕴涵消除 规则。
p [premise]
p -> q [premise]
p -> (q -> r) [premise]
q [->E(1,2)]请尝试自己完成剩下的证明！
参考答案
p [premise]
p -> q [premise]
p -> (q -> r) [premise]
q [->E(1,2)]
q -> r [->E(1,3)]
r [->E(4,5)]子证明框
为了证明更复杂的命题，我们需要使用 子证明框 来引入假设。例如，要使用 蕴涵引入 规则证明 p -> q，你必须先假设 p，然后在这个假设框内推导出 q。
在 ndp 文件中，我们通过缩进来创建子证明框。例如：
p [premise]
-- 注意：缩进必须是 2 个空格！
-- 可以写注释哦 :)
p [ass] -- ass 表示假设
p [tick(2)]
p -> p [->I(2,3)]来看一个稍复杂点的例子：
示例 1
证明 (p ^ q) -> r ⊢ p -> (q -> r)
(p ^ q) -> r [premise]
p [ass]
q [ass]
p ^ q [^I(2,3)]
r [->E(1,4)]
q -> r [->I(3,5)]
p -> (q -> r) [->I(2,6)]相信你现在已经明白它是如何工作的了。为什么不试试证明其逆命题也成立呢？即：
练习 2
证明 p -> (q -> r) ⊢ (p ^ q) -> r
参考答案
p -> (q -> r) [premise]
p ^ q [ass]
p [^E(2)]
q [^E(2)]
q -> r [->E(1,3)]
r [->E(5,4)]
(p ^ q) -> r [->I(2,6)]更复杂的子证明框
大多数推理规则的工作方式与我们上面展示的类似，但 析取消除 规则是个例外。下面是一个使用该规则的例子：p -> r, q -> r, p ∨ q ⊢ r
p -> r [premise]
q -> r [premise]
p ∨ q [premise]
p [ass]
r [->E(1,4)]
-- 必须用 tick 分隔第一种情况
r [tick(5)]
-- 现在开始 q 的情况
q [ass]
r [->E(2,7)]
r [/E(3,4,6,7,8)]接下来做什么？
信不信由你，关于命题逻辑和一阶逻辑的证明，你需要了解的基本上就是这些了！
更多参考资料：