BHK释义
释义
释义精确的陈述一个给定的公式的证明是什么。这是通过这个公式的在结构上归纳规定的:
P∧ ∧ -->Q{\displaystyle P\wedge Q}的有序对有序对,这里的a是P的一个证明而b是Q的一个证明。
P∨ ∨ -->Q{\displaystyle P\vee Q}的证明是有序对,这里的a是0而b是P的证明,或者a是1而b是Q的证明。
P→ → -->Q{\displaystyle P\to Q}的证明是函数f: P→Q,它把P的证明变换成Q的证明。
∃ ∃ -->x∈ ∈ -->S:ϕ ϕ -->(x){\displaystyle \exists x\in S:\phi (x)}的证明是有序对,这里的a是S的一个元素,而b是φ(a)的一个证明。
∀ ∀ -->x∈ ∈ -->S:ϕ ϕ -->(x){\displaystyle \forall x\in S:\phi (x)}的证明是函数f: a→φ(a),它把S的一个元素a变换成φ(a)的证明。
¬ ¬ -->P{\displaystyle \neg P}的证明被定义为P→ → -->⊥ ⊥ -->{\displaystyle P\to \bot },它的证明是把P的证明变换成⊥ ⊥ -->{\displaystyle \bot }的证明的一个函数。
⊥ ⊥ -->{\displaystyle \bot }是荒谬。应当没有它的证明。
假定从上下文获知原始命题的释义。
例子
恒等函数是公式P→ → -->P{\displaystyle P\to P}的证明,不管P是什么。
无矛盾律¬ ¬ -->(P∧ ∧ -->¬ ¬ -->P){\displaystyle \neg (P\wedge \neg P)}被展开为(P∧ ∧ -->(P→ → -->⊥ ⊥ -->))→ → -->⊥ ⊥ -->{\displaystyle (P\wedge (P\to \bot ))\to \bot }:
(P∧ ∧ -->(P→ → -->⊥ ⊥ -->))→ → -->⊥ ⊥ -->{\displaystyle (P\wedge (P\to \bot ))\to \bot }的证明是函数f,它把(P∧ ∧ -->(P→ → -->⊥ ⊥ -->)){\displaystyle (P\wedge (P\to \bot ))}的证明变换成⊥ ⊥ -->{\displaystyle \bot }的证明。
(P∧ ∧ -->(P→ → -->⊥ ⊥ -->)){\displaystyle (P\wedge (P\to \bot ))}的证明是证明的有序对,这里的a是P的证明,而b是 P → → --> ⊥ ⊥ --> {\displaystyle P\to \bot } 的证明。
P→ → -->⊥ ⊥ -->{\displaystyle P\to \bot }的证明是把P的证明变换成⊥ ⊥ -->{\displaystyle \bot }的证明的函数。
把它们放置到一起,(P∧ ∧ -->(P→ → -->⊥ ⊥ -->))→ → -->⊥ ⊥ -->{\displaystyle (P\wedge (P\to \bot ))\to \bot }的证明是函数f,它把有序对变换成 ⊥ ⊥ --> {\displaystyle \bot } 的证明 -- 这里的a是P的证明,而b是把P的证明变换成 ⊥ ⊥ --> {\displaystyle \bot } 的证明的一个函数。函数 f ( ⟨ ⟨ --> a , b ⟩ ⟩ --> ) = b ( a ) {\displaystyle f(\langle a,b\rangle )=b(a)} 证明了无矛盾律,不管P是什么。
在另一方面,排中律P∨ ∨ -->(¬ ¬ -->P){\displaystyle P\vee (\neg P)}展开为P∨ ∨ -->(P→ → -->⊥ ⊥ -->){\displaystyle P\vee (P\to \bot )},而一般没有证明。
什么是荒谬?
逻辑系统不可能有形式否定算子,使得在没有P的证明的时候有正确的 非P的证明(参见哥德尔不完备定理)。BHK释义转而采纳 非P为意味着P导致荒谬,指示为⊥ ⊥ -->{\displaystyle \bot },所以¬P的证明是把P的证明变换成荒谬的证明的函数。
荒谬的标准例子可以在算术中找到。假定0=1,并进行数学归纳法:0=0通过等同公理得到;(归纳假设)如果0等于特定自然数n,则1将等于n+1 (皮亚诺公理:Sm = Sn当且仅当m = n),但是因为0=1,所以0也等于n+1;通过归纳,0等于任何数,所以任何两个自然数都是相等的。
所以,有从0=1的证明得到任何基本算数等式和进而任何复杂算术命题的一种方式。进一步的说,要得到这种结果,不是必须的涉及皮亚诺公理0不是任何自然数的后继。这使得0=1在Heyting算术(皮亚诺公理被重写0=Sn → 0=S0)适合充当⊥ ⊥ -->{\displaystyle \bot }。这种0=1的使用验证了爆炸原理。
什么是函数?
BHK释义依赖于制定把一个证明变换成另一个证明,或者把一个域的元素变换成一个证明的函数的观点。不同版本的数学构造主义在这一点上是有分歧的。
Kleene的可实现性理论把这种函数看成是可计算函数。它处理Heyting算术,这里的量化的域是自然数而原始命题有x=y的形式。x=y的证明简单是平凡的算法,如果x求值得到与y求值同样的数(它对于自然数总是可决定的),否则没有证明。可以通过归纳建造起更复杂的算法。
引用
Troelstra, A. "History of Constructivism in the Twentieth Century". 1991.[1]
Troelstra, A. "Constructivism and Proof Theory". 2003.[2]
参见
直觉逻辑
直觉类型论
免责声明:以上内容版权归原作者所有,如有侵犯您的原创版权请告知,我们将尽快删除相关内容。感谢每一位辛勤著写的作者,感谢每一位的分享。
- 有价值
- 一般般
- 没价值