哥德爾完備性定理是數理邏輯中重要的定理，在 1929年由庫爾特·哥德爾首先證明。它的最熟知的形式聲稱在一階謂詞演算中所有邏輯上有效的公式都是可以證明的。
上述詞語“可證明的”意味著有著這個公式的形式演繹。這種形式演繹是步驟的有限列表，其中每個步驟要麼涉及公理要麼透過基本推理規則從前面的步驟獲得。給定這樣一種演繹，它的每個步驟的正確性可以在演算法上檢驗(比如透過計算機或手工)。
一個公式被稱為“邏輯上有效”的，如果它在這個公式的語言的所有模型中都為真。為了形式的陳述哥德爾完備性定理，你必須定義這個上下文中詞語“模型”的意義。這是模型論的基本定義。
在另一個方向上，哥德爾完備性定理聲稱一階謂詞演算的推理規則是“完備的”，在不需要額外的推理規則來證明所有邏輯上有效的公式的意義上。完備性的逆命題是“可靠性”。一階謂詞演算的實情是可靠的，就是說，只有邏輯上有效的陳述可以在一階邏輯中證明，這是可靠性定理斷言的。
處理在不同的模型中什麼為真的數理邏輯分支叫做模型論。研究在特定形式系統中什麼為可以形式證明的分支叫做證明論。完備性定理建立了在這兩個分支之間的基本聯絡。給出了在語義和語法之間的連線。但完備性定理不應當被誤解為消除了在這兩個概念之間的區別；事實上另一個著名的結果哥德爾不完備定理，證實了對“在數學中什麼是形式證明可以完成的”有著固有的限制。不完備定理的名聲與另一種意義的“完備”有關，參見模型論。
更一般版本的哥德爾完備性定理成立。它生成對於任何一階理論 T 和在這個理論中的任何句子 S，有一個 S 的自 T 的形式演繹，當且僅當 S 被 T 的所有模型滿足。這個更一般的定理被隱含使用，例如，在一個句子被證實可以用群論的公理證明的時候，透過考慮一個任意的群並證實這個句子被這個群所滿足。完備性定理是一階邏輯的中心性質，不在所有邏輯中成立。比如二階邏輯就沒有完備性定理。
完備性定理等價於超濾子引理，它是弱形式的選擇公理，在不帶有選擇公理的 Zermelo–Fraenkel集合論中有著等價的可證明性
哥德爾完備性定理是數理邏輯中重要的定理，在 1929年由庫爾特·哥德爾首先證明。它的最熟知的形式聲稱在一階謂詞演算中所有邏輯上有效的公式都是可以證明的。
上述詞語“可證明的”意味著有著這個公式的形式演繹。這種形式演繹是步驟的有限列表，其中每個步驟要麼涉及公理要麼透過基本推理規則從前面的步驟獲得。給定這樣一種演繹，它的每個步驟的正確性可以在演算法上檢驗(比如透過計算機或手工)。
一個公式被稱為“邏輯上有效”的，如果它在這個公式的語言的所有模型中都為真。為了形式的陳述哥德爾完備性定理，你必須定義這個上下文中詞語“模型”的意義。這是模型論的基本定義。
在另一個方向上，哥德爾完備性定理聲稱一階謂詞演算的推理規則是“完備的”，在不需要額外的推理規則來證明所有邏輯上有效的公式的意義上。完備性的逆命題是“可靠性”。一階謂詞演算的實情是可靠的，就是說，只有邏輯上有效的陳述可以在一階邏輯中證明，這是可靠性定理斷言的。
處理在不同的模型中什麼為真的數理邏輯分支叫做模型論。研究在特定形式系統中什麼為可以形式證明的分支叫做證明論。完備性定理建立了在這兩個分支之間的基本聯絡。給出了在語義和語法之間的連線。但完備性定理不應當被誤解為消除了在這兩個概念之間的區別；事實上另一個著名的結果哥德爾不完備定理，證實了對“在數學中什麼是形式證明可以完成的”有著固有的限制。不完備定理的名聲與另一種意義的“完備”有關，參見模型論。
更一般版本的哥德爾完備性定理成立。它生成對於任何一階理論 T 和在這個理論中的任何句子 S，有一個 S 的自 T 的形式演繹，當且僅當 S 被 T 的所有模型滿足。這個更一般的定理被隱含使用，例如，在一個句子被證實可以用群論的公理證明的時候，透過考慮一個任意的群並證實這個句子被這個群所滿足。完備性定理是一階邏輯的中心性質，不在所有邏輯中成立。比如二階邏輯就沒有完備性定理。
完備性定理等價於超濾子引理，它是弱形式的選擇公理，在不帶有選擇公理的 Zermelo–Fraenkel集合論中有著等價的可證明性