Gödel 完备性定理

哥德尔完备性定理
术语名称	哥德尔完备性定理
英语名称	Gödel's completeness theorem
别名	完全性定理

哥德尔完备性定理(Gödel's completeness theorem)是对一阶逻辑演算系统的完备性定理。即一阶谓词演算这一形式系统是完备的，所有普遍有效公式都是可证明的。

定理

一阶谓词演算中，所有逻辑有效的公式都是可证明的。

一般形式

对任意使用良序语言的一阶逻辑演算推理系统，其中任意理论 [math]\displaystyle{ T }[/math] 和公式 [math]\displaystyle{ s }[/math] ，若 [math]\displaystyle{ s }[/math] 是 [math]\displaystyle{ T }[/math] 的语义后承 [math]\displaystyle{ s }[/math] ，即 [math]\displaystyle{ T\vDash s }[/math] ，则 [math]\displaystyle{ s }[/math] 是 [math]\displaystyle{ T }[/math] 在推理系统中的语法后承，即 [math]\displaystyle{ T\vdash s }[/math] 。

模型存在定理

模型存在定理
术语名称	模型存在定理
英语名称	model existence theorem

对任意使用良序语言的一阶逻辑演算推理系统，若其中任意理论 [math]\displaystyle{ T }[/math] 其语法上有一致性，则其有一个模型。

证明论
结构化证明	推理系统 形式化公理系统 （形式化、公理化）	Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示
		Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
		Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算
	证明、演绎	演绎、可演绎、证明、可证明
	命题、定理	命题、元命题、公理/公理模式、定理、元定理
	推理规则性质描述	保存真实性、保存重言性
	推理系统性质描述	可靠性、完备性/完全性、一致性、独立性
	重要元定理	演绎定理、切消定理（切割消除定理）
		（某种推理系统的）可靠性定理、完备性定理
序数分析	证明论序数
构造性证明 程序化证明	Curry–Howard 对应
	证明复杂度
经典结论	Gödel 完备性定理、 Hilbert 纲领、 Gödel 不完备定理、相对一致性