哥德尔完全性定理是数理逻辑中重要的定理，在1929年由库尔特·哥德尔首先证明。它的最熟知的形式声称在一阶谓词演算中所有逻辑上有效的公式都是可以证明的。

上述词语“可证明的”意味着有着这个公式的形式演绎。这种形式演绎是步骤的有限列表，其中每个步骤要幺涉及公理要幺通过基本推理规则从前面的步骤获得。给定这样一种演绎，它的每个步骤的正确性可以在算法上检验（比如通过计算机或手工）。

如果一个公式在这个公式的语言的所有模型中都为真，它就被称为“逻辑上有效”的。为了形式的陈述哥德尔完全性定理，你必须定义这个上下文中词语“模型”的意义。这是模型论的基本定义。

Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. It makes a close link between model theory that deals with what is true in different models, and proof theory that studies what can be formally proven in particular formal systems.