为什么逻辑学的排中律不是任何条件下都可使用的? 第1页

实际上，无论你是接纳还是不接纳排中律，你从任意递归形式系统之内朝“外面”看，总有无限多的命题是不能认定是真还是假，只能落入真值空隙之中；即所谓的不完备定理。

排中律更接近于给予了真命题和假命题之间的对称性，以及承认了反证法的可行性^[1]。“只要想，中间情况都是可以没有的”我觉得更加适宜作为一种“良好的愿望”。

而且，这些落入真值空隙的命题还不是简单的只是因为形式系统的无能才没有真值；他们有一些命题的真值本来就是可以自由任取的，比如连续统假设，或者更通俗一点的“实数集是不是勒贝格可测的”。

当然，还可以提出更为直接的正面辩护：你想要一个可以求值的分析学吗？

迎接直觉主义的遗产，剔除排中律，直接在系统内承认真值空隙的存在，就可以实现一个可以求值的分析学。

还有一类称之为反经典公理：存在一个形式系统T，一个公理S，排中律LEM使得

T一致，T+S一致，T+LEM一致，T+S+LEM不一致

S就是反经典公理，T+S就是排中律的反模型。“MLTT^[2]+UA^[3]”“Agda + injective type constructors”“Coq + impredicative Set”“HA^[4] + 所有 函数都是可计算的”“IZF + 所有实函数都是一致连续的”都是这样的反模型。

为反模型辩护比直觉主义的模型困难很多。但我们可以作这样的思考：

• 否命题可以证明一切。
• 反证法提供了一种“证明无关”性(Proof irrelevance)：我们可以将所有的“最终证实为真”的证明，无论是直接构造出来的，还是用反证法得到的，都视为一样的。
• 如果我们承认了某种公理，具有分辨证明之间不同性的力量（这在算法的比较中很常见）
• 那么加上反证法带来的证明无关性，便可以证明一切，也就是不一致。

参考

1. ^ 反证法是【从“一个命题P是假的”出发得到矛盾，便得到了命题P的证明】，并不承诺命题都能且只能被两种真值填满（二值原理）。
2. ^ Martin-Lof type theory
3. ^ 单价公理, Univalence Axiom
4. ^ 海廷算术, Heyting Arithmetic, 皮亚诺算术的直觉主义版