哥德尔不完备定理
哥德尔不完备定理（）是数理逻辑中的两条定理，探讨了形式化公理系统中可证明性的局限性。这些结果由库尔特·哥德尔于1931年发表，在数理逻辑和数学哲学领域都具有重要意义。人们普遍认为，这些定理表明希尔伯特计划——即为所有数学寻找一套完备且一致的公理系统——是不可能实现的。 第一定理指出： 这是形式逻辑中的定理，容易被错误表述。有许多命题听起来很像是哥德尔不完备定理，但事实上并不是。具体实例见对哥德尔定理的误解。 把第一条定理的证明过程在系统…
标签：#证明论
共 17 篇文章
证明论
证明论是数理逻辑的一个分支，它将数学证明表达为形式化的数学客体，从而通过数学技术来简化对他们的分析。证明通常用归纳式地定义的数据结构来表达，例如链表，盒链表，或者树，它们根据逻辑系统的公理和推理规则构造。因此，证明论本质上是语法逻辑，和本质上是语义学的模型论形相反。和模型论，公理化集合论，以及递归论一起，证明论被称为数学基础的四大支柱之一。 证明论也可视为哲学逻辑的分支，其主要兴趣在于证明论语义学的思想，该思想依赖于结构证明论的技术型想…
缓成长阶层
在可计算性理论、计算复杂性理论和证明理论中，缓成长阶层是缓成长函数gα: N → N的序数索引族（其中N是自然数集合, {0, 1, ... }）。缓成长阶层的增长率与急成长阶层形成鲜明对比。 定义 令 μ 为一个大的可数序数，以便将基本序列分配给每个小于 μ 的极限序数。函数gα: N → N的缓成长阶层（对于α g_0(n) = 0 g_{\alpha+1}(n) = g_\alpha(n) + 1 对于极限序数α， g_\alph…
柯里-霍华德对应
寫作的：在Coq軟件中自然數加法交換性的證明。nat_ind 代表數學归纳，eq_ind 代替等於，f_equal 代表在等式兩邊取同樣的函數。 前面的定理參照顯示 m = m + 0和S（m + y）= m + S y。]] 柯里-霍華德对应（）是在计算机程序和数学证明之间的紧密联系；这种对应也叫做柯里-霍華德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和数学运算之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·柯里…
希尔伯特计划
希爾伯特計劃（）是由德國數學家大卫·希尔伯特在1920年代提出的一個數學計畫，旨在为数学基础危机提供解决方案。当时，早期澄清数学基础的尝试被发现存在悖论和不一致之处。作为解决方案，希尔伯特主张将所有现有理论建立在一个有限且的公理集之上，并证明这些公理具有一致性。他提出，像实分析这样的更复杂系统的一致性，可以通过更简单的系统来证明。最终，整个数学的一致性可以归结为基本算术的一致性。 1931年发表的哥德爾不完備定理指出，希爾伯特計劃在数学…
切消定理
切消定理（cut-elimination theorem (or Gentzen's Hauptsatz)）是确立相继式演算重要性的主要结果。它最初由格哈德·根岑在他的划时代论文《逻辑演绎研究》对分别形式化直觉逻辑和经典逻辑的系统LJ和LK做的证明。切削定理声称在相继式演算中，拥有利用了切规则的证明的任何判断，也拥有无切证明，就是说，不利用切规则的证明。 相继式是与多个句子有关的逻辑表达式，形式为"A, B, C, \ldots \vd…
希尔伯特演绎系统
在逻辑特别是数理逻辑中，希尔伯特风格演绎系统是归功于弗雷格和希尔伯特的一类形式演绎系统。这种演绎系统最经常为一阶逻辑而研究，但对其他逻辑也是有价值的。 所有演绎系统都在逻辑公理和推理规则之间作出取舍平衡。希尔伯特风格的演绎系统可以刻画为选择了大量的逻辑公理模式和少（Hilbert system）量的推理规则。最常研究的希尔伯特风格演绎系统只有一个推理规则即肯定前件和几个无限公理模式。 自然演绎系统做了相反的取舍，包括了很多演绎规则但有非…
自然演绎
在数理逻辑中，自然演绎是证明论中尝试提供象“自然”发生一样的逻辑推理形式模型的一种方式。這種方式對比於使用公理的公理系統。 动机 自然演绎来源自对共通于弗雷格、罗素和希尔伯特系统的判句公理化(希尔伯特演绎系统)的不满。这种公理化最著名使用是在罗素和怀特海的《数学原理》的数学论述中。在1926年由扬·武卡谢维奇在波兰发起的一系列研讨会提倡一种对逻辑的更加自然处理，斯坦尼斯瓦夫·亚希科夫斯基做了定义更自然的演绎的最早尝试，首先在1929年使…
相继式演算
在证明论和数理逻辑中，相继式演算（又译矢列演算、矢列式演算、序贯演算）是一阶逻辑（和作为它的特殊情况的命题逻辑）、模态逻辑等逻辑的一类。第一个相继式演算LK和LJ由格哈德·根岑（Gerhard Gentzen）在1934年/1935年引入，作为研究自然演绎的工具；它的名字得来自德语的“Logischer Kalkül”，意思是“逻辑演算”。相继式演算系统有时被称为Gentzen系统，但使用时应避免与同为Gentzen发明的证明演算自然演…
完备性
在数学及其相关领域中，一个对象具有完备性（），即它不需要添加任何其他元素，这个对象也可称为完备的或完全的。更精确地，可以从多个不同的角度来描述这个定义，同时可以引入完备化这个概念。但是在不同的领域中，“完备”也有不同的含义，特别是在某些领域中，“完备化”的过程并不称为“完备化”，另有其他的表述，请参考代数闭域、紧化或哥德尔不完备定理。 一个度量空间或一致空间被称为“完备的”，如果其中的任何柯西列都收敛，请参看完备空间。 在泛函分析中，一…
急成长阶层
在可计算性理论、计算复杂性理论和证明理论中，急成长阶层（也称为扩展Grzegorczyk阶层或Schwichtenberg-Wainer阶层） 是一类定义域和值域为自然数集，以序数作为索引的函数，即急成长函数fα: N → N构成的集合（其中N是自然数集 {0, 1, ...}，并且索引 α 的范围可达某个大的可数序数）。例如：Wainer阶层，或Löb–Wainer阶层是所有具有索引 α0 的急成长函数。 急成长阶层提供了一种根据增长…
结构规则
在证明论中，结构规则是不提及任何逻辑连结词的推理规则，它直接操作于判断或相继式。结构规则通常模仿逻辑的元理论性质。拒绝一个或多个结构规则的逻辑被归类为亚结构逻辑。 常见结构规则 弱化，这里的相继式的假设或结论可以扩展到额外的数目。在符号形式中弱化规则可以写为 :\frac{\Gamma \vdash \Sigma}{\Gamma, A \vdash \Sigma} 在十字转门的左侧，和 :\frac{\Gamma \vdash \Sig…
獨立性 (數理邏輯)
在數理邏輯上，獨立性指的是一個句子相對於其他句子的不可證明性。 若一個句子\sigma獨立於一個一階T，那就表示說\sigma在T中是不能證明也不能否證的，也就是說不能由T證明\sigma，也不能由T證明\sigma為偽。對於這樣的\sigma，有時會說\sigma在T中是不可判定的，而這裡的「不可判定」跟決定性問題中的「不可判定」是不同的。 若理論T中的每項公設都不能由T中的其他公設證明，則說T是獨立的，一個有著獨立公設集合的理論又稱…
相继式
在证明论中，相继式（sequent）是对在规定演绎的演算的时候经常用到的可证明性的形式陈述。 解释 相继式有如下形式 :\Gamma\vdash\Sigma 这里的Γ和Σ二者是逻辑公式的序列（就是说公式的数目和出现次序都是重要的）。符号\vdash通常被称为十字转门（turnstile）或T型符号（tee），并经常被读做"产生"或"证明"。它不是语言中的符号，而用来讨论证明的元语言中的符号。在相继式中，Γ叫做相继式的前件（anteced…
哥德尔完备性定理
哥德尔完备性定理是数理逻辑中重要的定理，在1929年由库尔特·哥德尔首先证明。它的最熟知的形式声称在一阶谓词演算中所有逻辑上有效的公式都是可以证明的。 上述词语“可证明的”意味着有着这个公式的形式演绎。这种形式演绎是步骤的有限列表，其中每个步骤要么涉及公理要么通过基本推理规则从前面的步骤获得。给定这样一种演绎，它的每个步骤的正确性可以在算法上检验（比如通过计算机或手工）。 如果一个公式在这个公式的语言的所有模型中都为真，它就被称为“逻辑…
BHK释义
在数理逻辑中，直覺主義邏輯的布勞威爾-海廷-柯爾莫哥洛夫释义（Brouwer–Heyting–Kolmogorov interpretation）或BHK释义是由魯伊茲·布勞威爾、阿蘭德·海廷和独立的由安德雷·柯爾莫哥洛夫提出的。它有时也叫做可实现性释义，因为有关于斯蒂芬·科尔·克莱尼的可实现性理论。 释义 释义精确的陈述一个给定的公式的证明是什么。这是通过这个公式的在结构上归纳规定的： P \wedge Q的证明是有序对，这裡的a是P…
可实现性
可实现性是可用来处理关于公式的信息而不是关于公式的证明的那部分证明论。自然数n被称为实现了自然数算术的语言中一个陈述。其他逻辑和数学陈述也是可实现的，假如提供了解释合式公式一种方法，而不用借助达成这些公式的证明。 起源 斯蒂芬·科尔·克莱尼在1945年介入了可实现性的概念，寄希望于它成为直觉逻辑推理的忠实典范，但这个设想最初由Rose反证了一个可实现的命题公式的例子，它在直觉演算中是不可证明的。可实现性似乎由于它的复杂度而难于公理化，但…