Gödel's incompleteness theorems

E71396

mathematical theorem metamathematical theorem result in mathematical logic

Gödel's incompleteness theorems are two fundamental results in mathematical logic showing that any sufficiently powerful, consistent formal system cannot prove all true statements about arithmetic, and cannot prove its own consistency.

Try in SPARQL Jump to: Surface forms Disambiguation Statements Elicitation Referenced by

All labels observed (9)

Label	Occurrences
Gödel's incompleteness theorems canonical	10
Gödel’s incompleteness theorems	8
Gödel incompleteness theorems	3
incompleteness theorems	3
Gödel's first incompleteness theorem	2
Gödel's second incompleteness theorem	2
Gödel’s Incompleteness Theorems	1
Gödel’s second incompleteness theorem	1
Kurt Gödel's incompleteness theorems paper	1

How this entity was disambiguated

This entity first appeared as the object of triple T568429 — resolving that mention is where its identity was fixed. The disambiguator weighed these candidate entities and picked the highlighted one (or “None”, minting a new entity). This is how homonymy is resolved: the same surface form can point to different entities.

NED1 Entity disambiguation (via context triple) gpt-5-mini-2025-08-07

Target entity: Gödel's incompleteness theorems
Context triple: [liar paradox, relatedTo, Gödel's incompleteness theorems]

A. Tarski's undefinability theorem
Tarski's undefinability theorem is a fundamental result in mathematical logic showing that, in sufficiently strong formal systems, the notion of truth for the language of the system cannot be defined within that same language.
B. Hilbert’s program
Hilbert’s program was an influential early-20th-century initiative in the foundations of mathematics that sought to formalize all of mathematics and prove its consistency using finitistic methods.
C. Remarks on the Foundations of Mathematics
Remarks on the Foundations of Mathematics is a posthumously published collection of Ludwig Wittgenstein’s later writings that critically examines the nature of mathematical truth, proof, and practice from a philosophical and language-centered perspective.
D. Church–Turing thesis
The Church–Turing thesis is a foundational principle in computability theory stating that any function that can be effectively computed by an algorithm can be computed by a Turing machine (or equivalently by other formal models of computation).
E. On Computable Numbers with an Application to the Entscheidungsproblem
"On Computable Numbers, with an Application to the Entscheidungsproblem" is Alan Turing’s landmark 1936 paper that introduced the Turing machine model and founded the formal study of computability and the limits of algorithmic decision procedures.
F. None of above. chosen
G. Unsure - the case is ambiguous/there is not enough information to decide.

NED2 Entity disambiguation (via description) gpt-5-mini-2025-08-07

Target entity: Gödel's incompleteness theorems
Target entity description: Gödel's incompleteness theorems are two fundamental results in mathematical logic showing that any sufficiently powerful, consistent formal system cannot prove all true statements about arithmetic, and cannot prove its own consistency.

A. Tarski's undefinability theorem
Tarski's undefinability theorem is a fundamental result in mathematical logic showing that, in sufficiently strong formal systems, the notion of truth for the language of the system cannot be defined within that same language.
B. Hilbert’s program
Hilbert’s program was an influential early-20th-century initiative in the foundations of mathematics that sought to formalize all of mathematics and prove its consistency using finitistic methods.
C. Remarks on the Foundations of Mathematics
Remarks on the Foundations of Mathematics is a posthumously published collection of Ludwig Wittgenstein’s later writings that critically examines the nature of mathematical truth, proof, and practice from a philosophical and language-centered perspective.
D. Church–Turing thesis
The Church–Turing thesis is a foundational principle in computability theory stating that any function that can be effectively computed by an algorithm can be computed by a Turing machine (or equivalently by other formal models of computation).
E. On Computable Numbers with an Application to the Entscheidungsproblem
"On Computable Numbers, with an Application to the Entscheidungsproblem" is Alan Turing’s landmark 1936 paper that introduced the Turing machine model and founded the formal study of computability and the limits of algorithmic decision procedures.
F. None of above. chosen

Statements (49)

Predicate	Object
instanceOf	mathematical theorem ⓘ metamathematical theorem ⓘ result in mathematical logic ⓘ
appliesTo	Peano arithmetic ⓘ Zermelo–Fraenkel set theory with Choice ⓘ linked to: Zermelo–Fraenkel set theory effectively axiomatized theories ⓘ formal axiomatic systems ⓘ recursively axiomatizable theories ⓘ sufficiently strong theories of arithmetic ⓘ
assumes	ω-consistency in Gödel's original proof of the first theorem ⓘ
author	Kurt Gödel ⓘ
concerns	provability in formal systems ⓘ truth in arithmetic ⓘ
field	foundations of mathematics ⓘ mathematical logic ⓘ metamathematics ⓘ proof theory ⓘ
firstTheoremStates	any consistent, effectively axiomatized theory capable of expressing elementary arithmetic is incomplete ⓘ
hasPart	Gödel's first incompleteness theorem ⓘ linked to: Gödel's incompleteness theorems Gödel's second incompleteness theorem ⓘ linked to: Gödel's incompleteness theorems
implies	a sufficiently strong consistent theory cannot prove its own consistency ⓘ existence of true but unprovable statements ⓘ limitations of Hilbert's program ⓘ no complete and consistent extension of Peano arithmetic is recursively axiomatizable ⓘ
influenced	philosophy of logic ⓘ philosophy of mathematics ⓘ proof theory ⓘ theory of computation ⓘ
laterGeneralizedBy	results using only simple consistency instead of ω-consistency ⓘ
namedAfter	Kurt Gödel ⓘ
originalLanguage	German ⓘ
publishedIn	Monatshefte für Mathematik ⓘ
relatedTo	Church–Turing thesis ⓘ Gödel numbering ⓘ Hilbert's program ⓘ linked to: Hilbert’s program Löb's theorem ⓘ Peano arithmetic ⓘ Tarski's undefinability theorem ⓘ
requires	ability to represent basic arithmetic ⓘ consistency of the formal system ⓘ effective axiomatization ⓘ
secondTheoremStates	no consistent, effectively axiomatized theory capable of expressing elementary arithmetic can prove its own consistency ⓘ
showsLimitationOf	axiomatic method for arithmetic ⓘ formalism in mathematics ⓘ
status	proven ⓘ
usesMethod	arithmetization of syntax ⓘ diagonalization ⓘ self-referential sentences ⓘ
yearProved	1931 ⓘ

How these facts were elicited

Referenced by (31)

Full triples — surface form annotated when it differs from this entity's canonical label.

liar paradox → relatedTo → Gödel's incompleteness theorems ⓘ

On Computable Numbers, with an Application to the Entscheidungsproblem → relatedTo → Gödel’s incompleteness theorems ⓘ

subject linked to: On Computable Numbers with an Application to the Entscheidungsproblem