Gödel's Incompleteness Theorems

Gödel's two incompleteness theorems (1931) are the central limitative results of mathematical logic. They say, roughly, that any formal system rich enough to express elementary arithmetic is unable to settle every question in its own language, and is unable to certify its own consistency. They mark the boundary between what can be captured by a fixed set of axioms and inference rules and what is true — and they do so constructively, by exhibiting concrete undecided sentences.

These results live downstream of first-order logic: the framework of effective axiomatization, provability ( $⊢$ ), and truth in a model ( $⊨$ ) is assumed throughout. They are best read alongside the contrasting completeness theorem, with which they are easily confused, and they underpin the independence phenomena seen in set theory.

Statement of the theorems

Fix a formal theory $T$ in the language of arithmetic (or any language interpreting arithmetic). Three hypotheses are essential:

$T$ is effectively axiomatized (recursively/computably enumerable): there is an algorithm that decides whether a given string is an axiom of $T$ . This is what makes " $T$ proves $φ$ " a mechanically checkable notion.
$T$ is consistent: it does not prove a contradiction. (For the exact form of the first theorem one needs $ω$ -consistency, later weakened to plain consistency by Rosser.)
$T$ interprets a sufficient fragment of arithmetic — it is strong enough to represent all computable functions. The standard weak benchmark is Robinson arithmetic $Q$ ; the usual working theory is Peano arithmetic $PA$ .

First Incompleteness Theorem. Any consistent, effectively axiomatized theory $T$ extending $Q$ is incomplete: there is a sentence $G_{T}$ in the language of $T$ such that $T ⊬ G_{T} and T ⊬ \neg G_{T} .$ Moreover $G_{T}$ can be chosen to be true in the standard model $N$ — it is a $Π_{1}$ arithmetical statement asserting its own unprovability.

Second Incompleteness Theorem. For such a $T$ (now at least as strong as $PA$ ), if $T$ is consistent then $T ⊬ Con (T),$ where $Con (T)$ is a natural arithmetical sentence expressing the consistency of $T$ . A theory strong enough to talk about its own proofs cannot prove its own consistency.

A useful slogan: truth outruns provability, and a system cannot lift itself by its own bootstraps.

Why "enough arithmetic"? The three hypotheses cannot be dropped

Each hypothesis is necessary, and dropping any one produces a complete theory, showing the theorem is sharp.

Drop effective axiomatizability. True arithmetic $Th (N)$ — the set of all sentences true in $N$ — is complete by definition. But it is not computably enumerable (this is essentially Tarski's theorem below), so it is not a formal system in the required sense.
Drop consistency. An inconsistent theory proves everything, hence is trivially complete. Incompleteness is interesting only for consistent theories.
Drop arithmetical strength. Several mathematically rich theories are complete and decidable because they cannot encode their own syntax: the theory of dense linear orders (DLO), Presburger arithmetic (the additive theory $(N, 0, 1, +, <)$ , with no multiplication), the theory of algebraically closed fields, and the first-order theory of real closed fields (Tarski). The presence of multiplication — which lets one express the divisibility and prime-counting relations needed to encode sequences — is exactly what tips arithmetic into incompleteness.

The machinery: arithmetization and three lemmas

Gödel's proof is a feat of self-reference made rigorous. Its parts have become standard tools.

Gödel numbering

Every symbol, formula, and finite proof is assigned a natural number — its Gödel number — by a fixed, computable, injective coding (e.g. via prime factorization $2^{a_{0}} 3^{a_{1}} 5^{a_{2}} \dots$ ). Syntactic operations (" $φ$ is an axiom", " $p$ is a proof of $φ$ ", "substitute a numeral into $φ$ ") become arithmetical relations on the codes. Write $┌ φ ┐$ for the numeral naming the code of $φ$ .

The numbering itself is purely syntactic and metatheoretic: the map $# : {expressions} \to N$ is defined in the metalanguage and depends only on the shape of a string, never on any interpretation or model. Two facts confirm its syntactic character. It is choice-independent — any computable injection with computable inverse and decidable syntactic predicates serves equally (prime powers, sequence codings, base- $128$ ASCII, …), so nothing depends on the scheme. And the basic syntactic predicates (" $x$ codes a formula", " $p$ codes a proof of $x$ ") are primitive recursive, so the metatheory doing the coding can be as weak as primitive recursive arithmetic (PRA) — no set theory, no semantics. This finitary character is exactly why the construction was admissible to Hilbert's finitists.

What makes self-reference non-circular is a number-vs-numeral distinction. For each expression there are two levels:

Object	What it is	Where it lives
$# φ \in N$	a natural number (the code)	metatheory
$┌ φ ┐ = S^{# φ} 0$	a numeral, a closed term naming that number	object language

The metalevel map lives in the metalanguage, but what appears inside a formula like $Prov_{T} (┌ φ ┐)$ is the numeral — an honest object-language term. The object theory never literally contains expressions; it contains numerals denoting their codes, together with arithmetical formulas defining the (recursive) syntactic relations on those codes. So $T$ "talks about its own syntax" only via the isomorphic copy $(metatheory’s syntax) ≅ (recursive relations on codes) \subseteq arithmetic \subseteq T$ . The one semantic-sounding claim — that $┌ φ ┐$ denotes $# φ$ in $N$ — is never needed for the proof, which manipulates numerals purely as closed terms.

Representability

Because $T$ interprets enough arithmetic, every computable function and decidable relation is representable in $T$ : there is a formula that $T$ proves to hold exactly on the true instances. In particular the proof predicate $Prf_{T} (p, x) \equiv “ p codes a T -proof of the formula coded by x ”$ is decidable, hence representable, and the provability predicate $Prov_{T} (x) \equiv \exists p Prf_{T} (p, x)$ expresses " $x$ is the code of a $T$ -theorem." Note $Prov_{T}$ is $Σ_{1}$ (a search for a proof), and not in general decidable.

The proof predicate up close

It is worth unpacking $Prf_{T}$ , since it carries the weight. It says: $p$ codes a finite sequence of formulas that is a correct $T$ -proof whose last line is the formula coded by $x$ .

The explicit formula and its decomposition. Long in symbols, but a bounded conjunction of decidable pieces.

"Correct proof" means every line is an axiom or follows from earlier lines by a rule:

$Prf_{T} (p, x) \equiv Seq (p) \land (p)_{lh (p) \dot{-} 1} = x \land \forall i < lh (p) [Ax_{T} ((p)_{i}) \lor \exists j, k < i MP ((p)_{j}, (p)_{k}, (p)_{i}) \lor \exists j < i Gen ((p)_{j}, (p)_{i})]$

with decidable subpredicates: $Seq (p)$ (" $p$ codes a sequence", $(p)_{i}$ its $i$ -th entry, $lh (p)$ its length), $Ax_{T} (y)$ (" $y$ codes a logical or nonlogical axiom of $T$ " — for $PA$ this must recognize instances of the induction schema), $MP (a, b, c)$ (" $b$ codes $a \to c$ "), and $Gen (a, c)$ (" $c$ codes $\forall v a$ "). Because $PA$ cannot quantify over finite sequences directly, the coding $(p)_{i}$ uses Gödel's β-function (or prime-power exponents) to pack a sequence into one number with a $Δ_{0}$ decoding.

Is it a long formula? In primitive symbols ( $0, S, +, \cdot, =, \neg, \to, \forall$ ) it is astronomically long — one must build sequence-coding, formulahood, substitution, and axiomhood from scratch. But as a logical object it is short and modular: a bounded conjunction of decidable pieces, normally written in a definitional extension (one defined symbol per primitive-recursive function, justified by representability + conservativity). The length is bookkeeping; the complexity is what matters.

That complexity is measured by the arithmetical hierarchy, which classifies formulas by their leading unbounded number-quantifiers (a bounded quantifier is one of the form $\forall x < t$ or $\exists x < t$ ):

$Δ_{0}$ (= $Σ_{0}$ = $Π_{0}$ ): all quantifiers bounded. Such formulas are decidable — their truth on given numerals can be checked mechanically, and $Q$ decides each closed instance.
$Σ_{1}$ : $\exists \overset{y}{ˉ} θ$ with $θ \in Δ_{0}$ — one block of unbounded existentials over a decidable matrix. These are exactly the recursively enumerable (semi-decidable) properties: search for a witness.
$Π_{1}$ : $\forall \overset{y}{ˉ} θ$ with $θ \in Δ_{0}$ — the co-r.e. properties. $Σ_{1}$ and $Π_{1}$ are dual: $φ$ is $Σ_{1}$ iff $\neg φ$ is $Π_{1}$ .

(The superscript in the fuller notation $Σ_{1}^{0}, Π_{1}^{0}$ records that the quantifiers range over numbers; the whole of this page stays at that level, so we drop the $0$ and write $Δ_{0}, Σ_{1}, Π_{1}$ .) With this vocabulary the three predicates line up cleanly:

Predicate	Form	Status
$Prf_{T} (p, x)$	$Δ_{0}$ (all quantifiers bounded by $p$ )	primitive recursive, decidable
$Prov_{T} (x) \equiv \exists p Prf_{T} (p, x)$	$Σ_{1}$	r.e., not decidable
$G_{T} \equiv \neg Prov_{T} (┌ G_{T} ┐)$	$Π_{1}$	the Gödel sentence

The engine is exactly this asymmetry: checking a candidate proof is mechanical ( $Δ_{0}$ ); searching for one adds a single unbounded $\exists p$ and jumps to $Σ_{1}$ . That one quantifier is the gap between proof-verification and provability. Two riders:

This is where "effectively axiomatized" is used. $Ax_{T}$ is primitive recursive only because $T$ 's axioms are decidable; drop that and $Prf_{T}$ is no longer $Δ_{0}$ and the derivability conditions break.
Intensionality (matters for the second theorem). Gödel II is sensitive to how $Prov_{T}$ is written, not merely its extension: a natural $Σ_{1}$ predicate satisfying the derivability conditions gives $T ⊬ Con (T)$ , but deviant extensionally-equivalent predicates (Rosser's, Feferman's) can make a $Con$ -style sentence provable.

The Diagonal (Fixed-Point) Lemma

For any formula $ψ (x)$ with one free variable there is a sentence $S$ with $T ⊢ S \leftrightarrow ψ (┌ S ┐) .$

The sentence $S$ "says of itself" that it has property $ψ$ . This is the rigorous engine behind the Liar-paradox intuition, but it produces a genuine sentence of arithmetic rather than a paradox.

Proof sketch. Self-reference is manufactured by a substitution function.

The key gadget: the diagonal function. Define a function on codes $d (n) = # (θ (\overline{n})) where n = # θ (x),$ which takes the code of a one-variable formula $θ (x)$ and returns the code of the sentence obtained by substituting $θ$ 's own numeral $\overline{n}$ back into it. Substitution-of-a-numeral is a primitive-recursive operation on codes, so $d$ is primitive recursive, hence representable in $T$ .

The construction (term version). Given $ψ (x)$ , build a formula saying " $ψ$ holds of the diagonalization of $x$ ." Working in a definitional extension where $d$ is available as a term, $θ (x) := ψ (d (x)), n_{0} := # θ, S := θ (\overline{n_{0}}) = ψ (d (\overline{n_{0}})) .$ By definition of $d$ , $d (n_{0}) = d (# θ) = # θ (\overline{n_{0}}) = # S, so T ⊢ d (\overline{n_{0}}) = ┌ S ┐ .$ Substituting equals into $S = ψ (d (\overline{n_{0}}))$ gives $T ⊢ S \leftrightarrow ψ (┌ S ┐)$ . $□$

The miracle in one line: $θ$ applies $ψ$ to "the diagonalization of $x$ "; plugging $θ$ 's own code in for $x$ makes that inner term compute the code of the very sentence $S$ being formed — self-reference is engineered, not assumed.

The honest version (for $Q$ , which lacks function terms). Use a representing formula $D (x, y)$ for $d$ (" $y = d (x)$ ") with provable uniqueness, and take $θ (x) := \forall y (D (x, y) \to ψ (y)), S := θ (\overline{n_{0}}) .$ Then $# S = d (n_{0})$ , so $T ⊢ D (\overline{n_{0}}, ┌ S ┐)$ and $T ⊢ \forall y (D (\overline{n_{0}}, y) \to y = ┌ S ┐)$ . The two directions are routine: ( $\to$ ) from $S$ , instantiate $y = ┌ S ┐$ via $D (\overline{n_{0}}, ┌ S ┐)$ to get $ψ (┌ S ┐)$ ; ( $\leftarrow$ ) from $ψ (┌ S ┐)$ , any $y$ with $D (\overline{n_{0}}, y)$ equals $┌ S ┐$ by uniqueness, so $ψ (y)$ , i.e. $S$ . The only ingredients are representability of one primitive-recursive function plus pure logic — no semantics.

A metatheorem: from provability to provable provability

The proofs below repeatedly take a step of the form " $T$ proves $φ$ , therefore $T$ proves that it proves $φ$ ." This is not a triviality — it is a genuine metatheorem, and it is worth isolating because the formula $Prov_{T} (┌ φ ┐)$ by itself is just a string. Four statements must be kept apart, two in each language:

Statement	Kind
$φ, Prov_{T} (┌ φ ┐)$	object-language formulas (mere sentences)
$T ⊢ φ$	metalanguage: "a derivation exists"
$T ⊢ Prov_{T} (┌ φ ┐)$	metalanguage: "that formula is a theorem"
$N ⊨ Prov_{T} (┌ φ ┐)$	metalanguage: "that formula is true in $N$ "

So "getting from $T ⊢ φ$ to $Prov_{T} (┌ φ ┐)$ " is ambiguous between reaching its truth and reaching its provability. The consistency-only proofs need the latter.

(D1) — provable $Σ_{1}$ -completeness. If $T ⊢ φ$ then $T ⊢ Prov_{T} (┌ φ ┐)$ .

This is the first Hilbert–Bernays–Löb derivability condition, a metatheorem about $T$ whose engine is:

Provable $Σ_{1}$ -completeness (core lemma). Every true $Σ_{1}$ sentence is provable already in $Q$ (hence in $T$ ).

Proof sketch. The core lemma, then D1 from it.

Why the core lemma holds. A true $Σ_{1}$ sentence is $\exists x θ (x)$ with $θ$ a $Δ_{0}$ (bounded) formula true of some numeral $\overset{n}{ˉ}$ . Bounded sentences are decided by $Q$ — numerals evaluate, and bounded quantifiers unfold into finite conjunctions/disjunctions $Q$ can check — so $Q ⊢ θ (\overset{n}{ˉ})$ , hence $Q ⊢ \exists x θ (x)$ .

Why D1 follows. If $T ⊢ φ$ , fix a concrete derivation with code $p_{0}$ . Then $Prf_{T} (\overset{p}{ˉ}_{0}, ┌ φ ┐)$ is a true $Δ_{0}$ sentence, so by the core lemma $T ⊢ Prf_{T} (\overset{p}{ˉ}_{0}, ┌ φ ┐)$ , and existential generalization gives $T ⊢ \exists p Prf_{T} (p, ┌ φ ┐)$ , i.e. $T ⊢ Prov_{T} (┌ φ ┐)$ . $□$

The weaker passage to mere truth — $T ⊢ φ \Rightarrow N ⊨ Prov_{T} (┌ φ ┐)$ — needs only that $Prov_{T}$ faithfully represents the real provability relation (a real proof's code witnesses the existential); it does not deliver the object-language theorem the consistency-only argument requires. Finally, the internalized form of D1 — $T$ proving the implication for itself, $T ⊢ Prov_{T} (┌ φ ┐) \to Prov_{T} (┌ Prov_{T} (┌ φ ┐) ┐)$ — is condition D3, which the second theorem needs.

Proof sketch of the first theorem

Apply the diagonal lemma to $ψ (x) \equiv \neg Prov_{T} (x)$ . This yields the Gödel sentence $T ⊢ G_{T} \leftrightarrow \neg Prov_{T} (┌ G_{T} ┐),$ a sentence asserting "I am not provable in $T$ ." Then:

$T ⊬ G_{T}$ . If $T ⊢ G_{T}$ , then by (D1) $T ⊢ Prov_{T} (┌ G_{T} ┐)$ ; but the fixed-point equivalence turns $T ⊢ G_{T}$ into $T ⊢ \neg Prov_{T} (┌ G_{T} ┐)$ , so $T$ proves a sentence and its negation — contradicting consistency. (Note D1 delivers the object-language theorem $T ⊢ Prov_{T} (┌ G_{T} ┐)$ , not just its truth, which is what makes the contradiction internal to $T$ .)
$T ⊬ \neg G_{T}$ . If $T ⊢ \neg G_{T}$ , then $T$ proves $Prov_{T} (┌ G_{T} ┐)$ , i.e. " $G_{T}$ is provable." Under $ω$ -consistency this cannot happen while $G_{T}$ is in fact unprovable. (Rosser's trick — using a cleverer "there is a proof of $G$ with no shorter proof of $\neg G$ " sentence — replaces $ω$ -consistency by plain consistency.)

Hence $G_{T}$ is undecided by $T$ . And since $G_{T}$ truly is unprovable, what it asserts is correct: $G_{T}$ is true in $N$ yet not a theorem. Incompleteness is not a gap in our cleverness; it is structural.

Proof idea of the second theorem

The argument above shows, informally, "if $T$ is consistent then $G_{T}$ is unprovable" — and that implication is itself elementary enough to be formalized inside $T$ . Formalized, it reads $T ⊢ Con (T) \to G_{T} .$ If $T$ could also prove $Con (T)$ , it would prove $G_{T}$ — which the first theorem forbids. Therefore $T ⊬ Con (T)$ .

What is $Con (T)$ ? The arithmetical sentence "no proof of a contradiction exists."

Consistency is internalized using the proof predicate. Pick any fixed refutable sentence — conventionally $0 = 1$ (i.e. $\overline{0} = \overline{1}$ ) — and define $Con (T) :\equiv \neg Prov_{T} (┌ 0 = 1 ┐) \equiv \forall p \neg Prf_{T} (p, ┌ 0 = 1 ┐),$ which reads "there is no $T$ -proof of $0 = 1$ ." Because $Prf_{T}$ is $Δ_{0}$ , this is a $Π_{1}$ sentence. Equivalent formulations (provably so, given the derivability conditions) include $\neg Prov_{T} (┌ ⊥ ┐)$ and "no sentence $φ$ has both $φ$ and $\neg φ$ provable," $\forall x \neg (Prov_{T} (x) \land Prov_{T} (\overset{\neg}{˙} x))$ .

Two cautions, both instances of intensionality:

$Con (T)$ depends on the chosen $Prov_{T}$ , hence on the axiom-recognizing predicate $Ax_{T}$ . A natural $Σ_{1}$ enumeration of the axioms gives the $Con (T)$ that the second theorem rules unprovable; deviant enumerations (Rosser-style, or Feferman's) yield consistency-style sentences $T$ can prove.
"Expressing consistency" is a claim about the standard model: $N ⊨ Con (T)$ iff $T$ really is consistent. Inside a nonstandard model, $\neg Con (T)$ can hold via a nonstandard "proof" of $0 = 1$ — which is exactly the model $T + \neg Con (T)$ produces.

The Hilbert–Bernays–Löb derivability conditions

Making "the first theorem is provable in $T$ " precise requires the Hilbert–Bernays–Löb derivability conditions on $Prov_{T}$ . Abbreviating the provability predicate by a box, $□ φ :\equiv Prov_{T} (┌ φ ┐) (“it is provable in T that φ ”),$ the three conditions read:

(D1) necessitation: $T ⊢ φ ⟹ T ⊢ □ φ$ ;
(D2) distribution: $T ⊢ □ (φ \to ψ) \to (□ φ \to □ ψ)$ ;
(D3) provable necessitation: $T ⊢ □ φ \to □□ φ$ .

These three are exactly the modal axioms of the provability logic GL (Gödel–Löb). Löb's theorem ( $T ⊢ □ φ \to φ$ only when $T ⊢ φ$ ) is the elegant generalization, and the second incompleteness theorem is its instance at $φ = ⊥$ .

The crux of the second theorem: $T ⊢ Con (T) \to G_{T}$ . Reduce to

(†)

, then a short box-calculus chain.

The crux of the second theorem is the single formalized implication $T ⊢ Con (T) \to G_{T}$ . Recall $Con (T) = \neg □ ⊥$ (with $□$ as defined above) and that the fixed point gives $T ⊢ G_{T} \leftrightarrow \neg □ G_{T}, equivalently T ⊢ \neg G_{T} \leftrightarrow □ G_{T} . (⋆)$ So proving $Con (T) \to G_{T}$ — i.e. $\neg □ ⊥ \to \neg □ G_{T}$ — is the contrapositive of the one fact that really needs the derivability conditions: $T ⊢ □ G_{T} \to □ ⊥. (†)$ In words: "if $G_{T}$ were provable then $T$ would be inconsistent" — the first theorem's own argument — is itself formalizable inside $T$ .

Derivation of $(†)$ . From $(⋆)$ , $T ⊢ □ G_{T} \to \neg G_{T}$ . Now reason with the derivability conditions D1–D3:

$T ⊢ □ G_{T} \to \neg G_{T}$ — from $(⋆)$ . Apply D1 then D2: $T ⊢ □□ G_{T} \to □ \neg G_{T}$ .
D3: $T ⊢ □ G_{T} \to □□ G_{T}$ . Chaining with (1): $T ⊢ □ G_{T} \to □ \neg G_{T}$ .
From the logical theorem $G_{T} \to (\neg G_{T} \to ⊥)$ , apply D1/D2 twice: $T ⊢ □ G_{T} \to (□ \neg G_{T} \to □ ⊥)$ .
Combine (2) and (3): $T ⊢ □ G_{T} \to □ ⊥$ , which is $(†)$ . $□$

Contraposing $(†)$ gives $T ⊢ \neg □ ⊥ \to \neg □ G_{T}$ , i.e. $T ⊢ Con (T) \to \neg □ G_{T}$ , and by $(⋆)$ that is $T ⊢ Con (T) \to G_{T}$ .

Finishing the theorem. The first theorem gives $T ⊬ G_{T}$ (assuming $T$ consistent). If $T$ also proved $Con (T)$ , then modus ponens on $T ⊢ Con (T) \to G_{T}$ would yield $T ⊢ G_{T}$ — a contradiction. Hence $T consistent ⟹ T ⊬ Con (T) .$ Two things are worth flagging. The proof needs only the first half of the first theorem ( $T ⊬ G_{T}$ ), so it goes through with plain consistency — no $ω$ -consistency or Rosser trick required. And it is exactly here that intensionality bites: step (1)'s reliance on a well-behaved $□$ is why a deviant provability predicate, though extensionally correct, can break $(†)$ and let a $Con$ -style sentence become provable.

Incompleteness is one node in a tight web of results, all powered by diagonalization.

Result	Statement	Diagonal target
Gödel I	$T$ consistent, effective, ⊇ $Q$ ⟹ incomplete	$\neg Prov_{T} (x)$
Gödel II	such $T$ ⟹ $T ⊬ Con (T)$	(formalized Gödel I)
Tarski's undefinability of truth	the set ${┌ φ ┐ : N ⊨ φ}$ is not arithmetically definable	a "truth" predicate $Tr (x)$
Church–Turing / undecidability	provability (and validity) in first-order logic is not decidable (the Entscheidungsproblem has no solution)	the halting problem
Rosser	consistency (not $ω$ -consistency) suffices for Gödel I	a refined provability predicate
Löb	$T ⊢ □ φ \to φ$ iff $T ⊢ φ$	$□ x \to φ$

Tarski's theorem is the semantic twin of Gödel's syntactic one: truth cannot be defined within the language; provability can, and that very definability is what makes the Gödel sentence possible.

"True but unprovable" — natural examples

Gödel's $G_{T}$ is artificial (it is built to be self-referential). A natural question is whether mathematically meaningful statements are independent of $PA$ . They are:

The Paris–Harrington theorem (1977): a strengthened finite Ramsey theorem is true (provable in ZFC) but unprovable in $PA$ — the first "natural" combinatorial independence.
Goodstein's theorem: every Goodstein sequence terminates — true, but unprovable in $PA$ (its proof needs transfinite induction up to $ε_{0}$ ).
The hydra game (Kirby–Paris): Hercules always wins, again independent of $PA$ .

For set theory the analogous independences — the Continuum Hypothesis and the Axiom of Choice — are independent of ZFC, established by Gödel's constructible universe $L$ and Cohen's forcing. These are incompleteness phenomena one level up.

Common misreadings

The theorems are famous and frequently distorted. A few guardrails:

They do not say "some truths are absolutely unprovable." $G_{T}$ is unprovable in $T$ ; the stronger theory $T + G_{T}$ (or $T + Con (T)$ ) proves it — and is in turn incomplete, with a new Gödel sentence. Incompleteness is relative to a fixed system, and provability is always relative to a theory.
They do not refute formalism wholesale, but they do refute Hilbert's program in its original form: there is no finitary consistency proof of analysis or set theory carried out within a weaker, "safe" fragment. (Gentzen's 1936 proof of $Con (PA)$ survives — at the cost of using $ε_{0}$ -induction, machinery not available inside $PA$ .)
They are not about vagueness, paradox, or human intuition. $G_{T}$ is a precise $Π_{1}$ arithmetical sentence; nothing inconsistent is asserted. The Liar analogy is heuristic — the diagonal lemma replaces "this sentence is false" (semantic, paradoxical) with "this sentence is unprovable" (syntactic, merely undecided).
They do not by themselves settle questions about minds and machines. The Lucas–Penrose argument — that incompleteness shows the mind is not a Turing machine — is contested; it assumes we can know our own consistency, exactly the move the second theorem blocks.

Summary

Question	Answer
What must $T$ be?	consistent, effectively axiomatized, interprets $Q$
First theorem	such $T$ is incomplete: an undecided, true $G_{T}$ exists
Second theorem	such $T$ (⊇ $PA$ ) cannot prove $Con (T)$
Key machinery	Gödel numbering, representability, diagonal lemma
What $G_{T}$ says	"I am not provable in $T$ "
Semantic twin	Tarski: truth is not definable in the language
Computational twin	Church–Turing: provability is undecidable
Escape routes (why sharp)	drop effectiveness, consistency, or multiplication ⟹ completeness returns
What it kills	Hilbert's program (finitary self-certification), not mathematics

Gödel's theorems do not show that mathematics is unreliable or that any particular problem is hopeless. They show something subtler and permanent: no single effectively given axiom system can be both complete and capable of certifying itself. Every consistent foundation strong enough to do arithmetic leaves true statements it cannot reach and a consistency it cannot vouch for — and the only way to settle them is to step up to a stronger system, which inherits the same predicament.

Keyboard shortcuts

youyuanwu