Ez a szócikk nem tünteti fel a független forrásokat, amelyeket felhasználtak a készítése során. Emiatt nem tudjuk közvetlenül ellenőrizni, hogy a szócikkben szereplő állítások helytállóak-e. Segíts megbízható forrásokat találni az állításokhoz! Lásd még: A Wikipédia nem az első közlés helye. (2023 augusztusából)

Gödel teljességi tétele a matematikai logika fontos tétele, azt mondja ki, hogy ha egy elsőrendű elméletben egy tetszőleges mondat minden modellben igaz, akkor bizonyítható is.

A tétel szerint, ha egy L elsőrendű nyelvben megadott T elméletnek (zárt formulák halmazának) van modellje, akkor konzisztens (ellentmondásmentes). Ez nyilvánvaló, hiszen a modellben minden T-ből levezethető állításnak igaznak kell lennie, márpedig a modellen nem teljesülhet egyszerre egy zárt formula és tagadása.

A teljességi tétel az igazság tétel megfordítása:

Ha egy L elsőrendű nyelvben megadott T elmélet konzisztens, akkor van modellje.

Ha egy L elsőrendű nyelvben T elmélet és ${\displaystyle \varphi }$ zárt formula, amire teljesül ${\displaystyle T\models \varphi }$, azaz igaz T minden modelljében, akkor ${\displaystyle T\vdash \varphi }$ is teljesül, azaz ${\displaystyle \varphi }$ levezethető T-ből.

Ez az állítás ekvivalens a teljességi tétel fenti alakjával. Ennek az állításnak egy interpretációja a szócikk elején levő állítás.

A fenti állítás szerint, ha például (csoportelméleti eszközökkel) belátjuk, hogy ha egy csoportban minden elem rendje 1 vagy 2, akkor a csoport kommutatív, akkor ez le is vezethető a csoportaxiómákból. Hasonlóan, ha belátjuk, hogy a halmazelmélet ZFC axiómarendszerének minden modelljében igaz egy állítás, akkor az az állítás bizonyítható ZFC-ből. Ez nem csak elképzelt lehetőség: a Baumgartner–Hajnal-tétel első bizonyítása úgy született, hogy a szerzők a Martin-axióma segítségével belátták, hogy az állítás igaz ZFC minden modelljében.

Az alábbiakban a Henkin-konstansos bizonyítás vázlatát adjuk. Először feltesszük, hogy a nyelv megszámlálható. Bővítsük ki a nyelvet megszámlálható sok új konstansjellel: ${\displaystyle c_{0},c_{1},\dots }$. Soroljuk fel a kibővített nyelv zárt formuláit, mint ${\displaystyle \varphi _{0},\varphi _{1},\dots }$. Soroljuk fel a kibővített nyelv kvantorral kezdődő formuláit is: ${\displaystyle (\exists x)\psi _{0}(x),\dots }$. Elkészítjük konzisztens elméletek növő ${\displaystyle T_{0}\subseteq T_{1}\subseteq T_{2}\subseteq \cdots }$ láncát a következőképpen: legyen ${\displaystyle T_{0}=T}$. Ha a konzisztens ${\displaystyle T_{2n}}$ adott, legyen ${\displaystyle T_{2n+1}=T_{2n}\cup \{\varphi _{n}\}}$ vagy ${\displaystyle T_{2n+1}=T_{2n}\cup \{\neg \varphi _{n}\}}$ aszerint, hogy az első konzisztens-e vagy sem. Ha a konzisztens ${\displaystyle T_{2n+1}}$ adott, legyen ${\displaystyle T_{2n+2}=T_{2n+1}\cup \{\exists x\psi _{n}(x)\to \psi _{n}(c_{i})\}}$ ahol ${\displaystyle c_{i}}$ egy olyan konstansjel, ami nem fordul el a ${\displaystyle \psi _{n}}$ formulában. ${\displaystyle T_{2n+2}}$ még mindig konzisztens. ${\displaystyle T^{*}=T_{0}\cup T_{1}\cup \cdots }$ mint konzisztens elméletek egyesítése, konzisztens és mivel minden zárt formulát vagy tagadását tartalmazza, teljes. Definiáljuk a ${\displaystyle \sim }$ relációt a konstansjeleken a következőképpen: ${\displaystyle c_{i}\sim c_{j}}$, ha ${\displaystyle [c_{i}=c_{j}]\in T^{*}}$. Ez ekvivalencia-reláció, jelölje ${\displaystyle c_{i}}$ ekvivalenciaosztályát ${\displaystyle [c_{i}]}$. Ekkor az ekvivalenciaosztályokra struktúrát építhetünk: ha R k-változós relációjel, ${\displaystyle R([c_{i_{1}}],\dots ,[c_{i_{k}}])}$, ha ${\displaystyle R(c_{i_{1}},\dots ,c_{i_{k}})\in T^{*}}$, hasonlóan a konstansjelekre és a függvényjelekre. Ekkor ez a struktúra modellje T-nek.

Ha a nyelv megszámlálhatónál nagyobb, hasonlóan járunk el, csak elméleteknek nem megszámlálható hosszú, hanem ${\displaystyle \kappa }$ hosszú növő láncát készítjük el, ahol ${\displaystyle \kappa }$ a nyelv számossága. Limesz lépésekben mindig a korábbi elméletek egyesítését kell venni. Ez még mindig konzisztens marad, mert minden bizonyítás véges lévén konzisztens elméletek növő transzfinit láncának egyesítése is konzisztens.

A fenti bizonyítás nemcsak modellt, de megszámlálható modellt ad (${\displaystyle |L|}$ számosságút, ha az L nyelv megszámlálhatónál nagyobb). Ezért a bizonyítás adja a Löwenheim–Skolem–Tarski-tételt is, továbbá Gödel kompaktsági tételét is.

A tétel használja a kiválasztási axiómát. Annak gyengébb változatával, az ultrafilterek létezéséről szóló állítással ekvivalens.

A tételt először Gödel igazolta doktori disszertációjában.