哥德尔不完备定理

形式系统：完备性、一致性和有效公理化

不完备性定理适用于足够复杂，可以表示自然数算术的形式系统，而这种形式系统是自洽的，可以被公理化的。这些概念的详细含义会在后面给出。尤其是在一阶逻辑的语境中，形式系统也被称为"形式定理"。一般地，一个形式系统被定义为含有一组特定公理集合以及符号变换规则(或者是推导规则)的演绎工具。这样的一个形式系统的例子是一阶算术系统，在这个系统中，所有变量都代表为自然数。而在其他系统中，例如集合论，只有部分属于形式系统的表述才表示了自然数算术。不完备性理论是关于这些形式系统中的形式可证明性，而不是关于非形式意义上的"可证明性"。

形式系统可能具有的性质如下，完备性、一致性和有效公理化的存在性。不完备性定理则表明任何蕴含皮亚诺算术公理的形式系统不能同时具有这三个性质。

有效公理化

如果形式系统中的定理集是递归可列举的集合(Franzén 2004, p. 112)，那么该形式系统是"有效公理化的"(也被称为“生成定理的有效性”)。
这意味着，在原则上计算机程序能够列举出系统中所有的定理，而不列出任何非定理的陈述。皮亚诺公理和策梅洛-弗兰克尔集合论 (ZFC) 都是有效生成定理的例子。
现在被称为真算术的理论不仅有皮亚诺算术中关于整数的正确陈述，而且是自洽和完备的，并有足够的运算公理。但是它的定理集不是递归可列举的集合，因此也不满足不完备定理的假设。

含义

哥德尔巧妙地利用了命题的“真值为真”和“含义为真”的区别，从而构造出了含义为真而真值不可证的命题，又避免了悖论的陷阱。形式逻辑系统的命题本身是没有含义的。命题只有真值而没有含义。公理命题的真值为真。其它命题的真值为真当且仅当该命题可以被证明，为假当且仅当该命题的非可以被证明。当形式逻辑系统被实际应用时，系统中的符号都被映射到实际概念上，从而有了语义。这种映射叫做一个模型。有了模型，命题就有了含义（语义）。例如，在ZF公理化集合论中，系统中的对象（object）被影射到“集合”这一概念，∈被映射到“属于”这一概念就是模型的一个例子。而ZF公理化系统本身即使没有模型也可以成立。如果换一个模型，形式系统没变，只是它不再是集合论了。当然，ZF公理化系统是为了集合论量身打造的，很适合于集合论。如果换一个模型，很难找到可理解的语义。但这说明了“真值为真”和“含义为真”是有区别的。
在大多数情况下，命题的“真值为真”和“含义为真”是一致的。例如，设A为一命题,则命题A↔¬A的含义是“本命题A为假”，这时A的真值为真和含义为真是一致的，结果形成了否定循环而构成了悖论。而逻辑系统不能含有悖论，所以这样的A应该是构造不出来得。哥德尔定理证明的巧妙之处就在于将悖论的“为假”改为了“为不可证”使得真值为真和含义为真成为不一致（含义为真是不可证，而真值为真或假都是可证），因而产生了自我否定又避免了循环的效果，也就避免了悖论。
理解了这一点，就可以理解哥德尔定理不是说存在真值为真又不可证这种自相矛盾的悖论命题（实际上应该构造不出来），而是存在含义为真但不可证（即真值不可知）的命题。哥德尔定理也不只是说存在既不可证真，也不可证伪的命题，这样的命题有很多，哥德尔定理的重要之处在于它还说了该不可证的命题是含义为真的。
哥德尔定理是一阶逻辑的定理，故最终只能在这个框架内理解。在形式逻辑中，数学命题及其证明皆以一种符号语言描述，只要检查每一个证明的有效性，便可从一组公理开始无可辩驳地证明一条定理。理论上，这样的证明可以在计算机上检查，事实上这样的有效性检查程序也已经有了。
为了这个过程得以进行，需确定手头有什么样的公理。可以从一组有限的公理集开始，例如欧几里得几何。或者更一般地，由一个可以允许无穷的公理列表开始，只要能机械地判断给定的命题是否是一条公理就行。在计算机科学里面，这被称为公理的递归集。尽管无穷的公理列表听起来有些奇怪，实际上自然数的通常理论中(被称为皮亚诺公理)就是如此。
哥德尔的第一条不完备定理表明任何一个允许定义自然数的体系必定是不完备的：它包含了不能在此体系内以一阶谓词逻辑形式证明的命题，并且该命题的否命题也不能在该体系内以一阶谓词逻辑的形式证明。
存在不完备的体系这一事实本身并不使人感到特别惊讶。例如，在欧几里得几何中，如果把平行公设去掉，就得到一个不完备的体系。不完备的体系可能只意味着尚未找出所有必须的公理而已。
但哥德尔揭示的是在多数情况下，例如在数论或者实分析中，永远不能找出公理的完整集合。换句话说，每一次将一个命题作为公理加入，将总有另一个命题出现在所能形式证明的范围之外。
如果加入无穷条公理（例如，所有真命题）到公理列表中，确保所有命题都可证明为真或假，但得到的公理列表将不再是递归集。给出任意一条命题，将没有机械的方法判定它是否是系统的一条公理。如果给出一个证明，一般来说也无法检查它是否正确。
在计算机科学的语言中，哥德尔定理有另一种表述方式。在一阶逻辑中，定理是递归可枚举的：你可以编写一个可以枚举出其所有有效证明的程序。你可以问是否可以将结论加强为递归的：可以编写一个在有限时间内判定命题真假的程序吗？根据哥德尔定理，答案是一般来说不能。

不确定命题的例子

哥德尔和保罗·寇恩得出的一些结果结合起来给出了不确定命题（既不能证明也不能否证的命题）的一个实际例子：选择公理和连续统假设都是集合论的标准公理系统内的不确定命题。
在1973年，同调代数中的怀特海问题被证明是集合论中的不确定命题。
1977年，Paris和Harrington证明了组合论中的一个命题，拉姆赛理论的某个版本，在皮阿诺公理给出的算术公理系统中是不确定的，但可以在集合论的一个更大体系中证明为真。
在计算机科学中用到的Kruskal的树问题，也是在皮亚诺公理中不确定而在集合论中可证明的。
Goodstein定理是一个关于自然数的相对简单的命题，它在皮亚诺算术中是不确定的。
古格里·钱顿（Gregory Chaitin）在算法信息论中构造了一个不确定命题，即“Chaitin随机数Ω的第n个字节是否为0”这样的命题在ZFC内是不可判定的。
计算逻辑中的停机问题不可解，亦是哥德尔不完备定理的一种表现形式。

第二不完备定理的证明要点

令𝑝是如上构造的不确定命题，且假定系统的兼容性可以在系统内部证明。我们已经看到，如果系统是兼容的，则𝑝是不可自证的。这个证明过程可以在系统内部形式化，因此命题“𝑝是不可证明的”或者“~𝑃(𝑝)”可以在系统内证明。
但是最后一个命题就等价于𝑝自己（而且这种等价性可以在系统内部证明），从而𝑝就可以在系统内证明。这一矛盾说明系统是不兼容的。

与不确定性原理的关系

有学者指出不完备定理和不确定性原理有某种联系。