格哈德·根岑 编辑
格哈德·根岑是德国数学家逻辑学家
1
相关
切消定理是确立相继式演算重要性的主要结果。它最初由格哈德·根岑在他的划时代论文《逻辑演绎研究》对分别形式化直觉逻辑和经典逻辑的系统LJ和LK做的证明。切削定理声称在相继式演算中,拥有利用了切规则的证明的任何判断,也拥有无切证明,就是说,不利用切规则的证明。
逻辑学家格哈德·根岑提议了逻辑连结词的意义可以用把它们介入到论述中的规则给出。例如,如果你相信“天是蓝的”并且还相信“草是绿的”,则你可以如下这样介入逻辑连接词“逻辑合取”: “天是蓝的 AND 草是绿的”。Gentzen 的想法是拥有这样的规则就是对你的词语,至少对特定词语的给出意义的东西。这个想法也关联于维特根斯坦的格言,在很多情况下我们可以说意义是使用。多数当代逻辑学家偏好认为介入规则和除去规则对于表达是同等重要的。在这种情况下,“与”被如下规则所特征化:
逻辑学家格哈德·根岑提议了逻辑连结词的意义可以用把它们介入到论述中的规则给出。例如,如果你相信“天是蓝的”并且还相信“草是绿的”,则你可以如下这样介入逻辑连接词“逻辑合取”: “天是蓝的 AND 草是绿的”。Gentzen 的想法是拥有这样的规则就是对你的词语,至少对特定词语的给出意义的东西。这个想法也关联于维特根斯坦的格言,在很多情况下我们可以说意义是使用。多数当代逻辑学家偏好认为介入规则和除去规则对于表达是同等重要的。在这种情况下,“与”被如下规则所特征化:
古德斯坦定理是数理逻辑中的一个关于自然数的叙述,是在 1944 年由鲁本·古德斯坦所证明。其主要是在说明“古德斯坦序列”最终会结束于 0 。柯比和柏丽斯 证明它在皮亚诺公理中是不可证明的。这是继哥德尔不完备定理构造的命题和 1943 年格哈德·根岑直接证明皮亚诺算术中 ε0-induction 不可被证明之后,第三个命题被证明在皮亚诺算术中不可证明。之后的例子是柏丽斯–哈灵顿定理。