---
title: The Second Incompleteness Theorem
module: Arithmetization and the Incompleteness Theorems
moduleNumber: 7
lessonNumber: 3
order: 703
summary: >
  Consistency of a recursively axiomatized theory is itself an arithmetic
  sentence, built from a provability predicate. When the theory is strong enough
  to formalize its own reflection and modus ponens — the Hilbert–Bernays–Löb
  derivability conditions — it cannot prove that sentence unless it is
  inconsistent. Löb's theorem is the companion result, and set theory is the
  case that closes Hilbert's program.
topics: [Arithmetization and the Incompleteness Theorems]
sources:
  - book: Enderton
    ref: "Ch. 3 — Undecidability; §3.7 Second Incompleteness Theorem"
draft: false
---

The [first incompleteness theorem](/logic/incompleteness/incompleteness-and-undecidability)
produced a true sentence a consistent recursive theory cannot prove. The second
one turns the same argument on the theory's own consistency: a sufficiently strong
recursively axiomatized theory cannot prove that it is consistent, unless it is
not. The consistency statement is an ordinary arithmetic sentence, and the proof
is the argument of the first theorem carried out inside the theory. Throughout,
$T$ is a recursively axiomatizable theory given by a recursive axiom set $A$
(that is, $\#A$ is recursive), and $\ulcorner\sigma\urcorner = S^{\#\sigma}0$
names a Gödel number.[^open]

## The provability predicate

From [item 20](/logic/incompleteness/arithmetization-of-syntax) of the
arithmetization, a sentence $\sigma$ is a theorem of $T$ iff some number codes a
deduction of it,

$$
\sigma \in T \;\iff\; \exists d\,\big[\, d \text{ codes a deduction from } A \text{ ending in } \sigma \,\big].
$$

The bracketed binary relation between $\#\sigma$ and $d$ is recursive; choose a
formula $\pi(v_1, v_2)$ that numeralwise represents it in $A_E$. Existentially
quantifying the proof gives a formula that expresses provability.

> **Definition (Provability predicate).** For a recursively axiomatizable $T$
> with recursive axioms $A$,
> $$
> \Prb_T\,\sigma \;=\; \exists v_2\, \pi(\ulcorner\sigma\urcorner, v_2).
> $$

The construction uses the recursiveness of $A$, so the subscript is really the
axiom set. The predicate reflects the theory's own proofs back into arithmetic.

> **Lemma (Reflection).** Let $T$ be recursively axiomatizable as above.
> **(a)** If $T \vdash \sigma$ then $A_E \vdash \Prb_T\,\sigma$.
> **(b)** If in addition $A_E \subseteq T$, then $T$ has the reflection
> property $T \vdash \sigma \Rightarrow T \vdash \Prb_T\,\sigma$.

> **Proof.** If $T \vdash \sigma$, let $d$ be the number of a deduction of $\sigma$
> from $A$. Then $A_E \vdash \pi(\ulcorner\sigma\urcorner, S^{d}0)$ because $\pi$
> represents the deduction relation, and existential generalization gives $A_E
> \vdash \Prb_T\,\sigma$. Part (b) follows since $A_E \subseteq T$.
> $\blacksquare$

Reflection is one-directional. Whenever the theory proves $\sigma$, it proves
that it proves $\sigma$, but it does not prove the conditional $\sigma \to
\Prb_T\,\sigma$. If $\sigma$ is true yet unprovable from $A_E$, then
$\sigma \to \Prb_{A_E}\,\sigma$ is actually false in $\fN$.

> **Worked example (Reflection is a rule, not an implication).** Reflection
> licenses $T \vdash \sigma \Rightarrow T \vdash \Prb_T\,\sigma$, which is a rule
> about proofs, not the object-level implication $\sigma \to \Prb_T\,\sigma$.
> Take $\sigma$ a Gödel sentence for $A_E$: true in $\fN$ but $A_E$-unprovable.
> In $\fN$ the antecedent $\sigma$ holds, while the consequent $\Prb_{A_E}\,
> \sigma = \exists v_2\, \pi(\ulcorner\sigma\urcorner, v_2)$ fails, since no
> number codes a proof of $\sigma$. A true antecedent and a false consequent
> make
> $$
> \models_{\fN} \neg\,(\sigma \to \Prb_{A_E}\,\sigma),
> $$
> so $A_E \not\vdash (\sigma \to \Prb_{A_E}\,\sigma)$. The rule holds only once
> an actual proof discharges the premise; as an internal implication it is not
> merely unprovable but outright false.

## The Gödel sentence, formalized

Apply the fixed-point lemma to $\neg\,\Prb_T$ to obtain a sentence
asserting its own unprovability,

$$
A_E \;\vdash\; \big(\, \sigma \leftrightarrow \neg\,\Prb_T\,\sigma \,\big).
$$

Half of the first incompleteness theorem is now a two-line consequence of
reflection.

> **Lemma (Unprovability of the Gödel sentence).** Let $T$ be recursively axiomatizable with $A_E \subseteq T$
> and $\sigma$ as above. If $T$ is consistent, then $T \not\vdash \sigma$.

> **Proof.** If $T \vdash \sigma$ then $T \vdash \Prb_T\,\sigma$ by
> reflection, while the choice of $\sigma$ gives $T \vdash \neg\,\sigma$; so $T$ is
> inconsistent. $\blacksquare$

The proof of the unprovability of the Gödel sentence is short and uses only reflection. A short proof about $T$
might be reproducible inside $T$, if $T$ can formalize the steps

$$
\Prb_T\,\sigma \;\to\; \Prb_T\,\Prb_T\,\sigma
\;\to\; \Prb_T(\neg\,\sigma)
\;\to\; \Prb_T(0 = S0).
$$

Carrying this out yields $T \vdash \Cons\,T$ only when $T$ is
inconsistent.

## The derivability conditions

What the internalization needs is that $T$ prove the reflection and modus-ponens
facts about its own provability predicate, not merely obey them in the
metatheory.

> **Definition (Sufficiently strong).** A recursively axiomatizable theory $T$ is
> sufficiently strong iff it satisfies the three derivability conditions:
> - $A_E \subseteq T$ — which gives reflection by the reflection lemma, $T \vdash \sigma
>   \Rightarrow T \vdash \Prb_T\,\sigma$;
> - $T \vdash \big(\Prb_T\,\sigma \to \Prb_T\,\Prb_T\,
>   \sigma\big)$ — reflection formalized inside $T$;
> - $T \vdash \big(\Prb_T(\rho \to \sigma) \to (\Prb_T\,\rho \to
>   \Prb_T\,\sigma)\big)$ — modus ponens formalized inside $T$.

Consistency itself is expressible. Take $0 = S0$ as a fixed sentence refutable
from $A_E$, and define

$$
\Cons\,T \;=\; \neg\,\Prb_T(0 = S0),
$$

read as "$T$ does not prove $0 = S0$," that is, "$T$ is consistent."

$$
% caption: Consistency is coded as the arithmetic assertion that no number codes
% a proof of the fixed refutable sentence $0 = S0$.
\begin{tikzpicture}[font=\small, >=stealth]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[draw=acc, thick, minimum width=30mm, minimum height=11mm] (con) at (0,0) {Con T};
  \node[draw, minimum width=56mm, minimum height=11mm, align=center] (rhs) at (6.6,0)
    {no number $d$ codes a proof\\of $0 = S0$};
  \draw[->, acc, thick] (con.east) -- (rhs.west) node[midway, above, font=\footnotesize] {abbreviates};
\end{tikzpicture}
$$

$$
% caption: The three derivability conditions the provability predicate must
% satisfy for the internalized argument to run.
\begin{tikzpicture}[font=\small, >=stealth,
  c/.style={draw, minimum width=74mm, minimum height=10mm, align=left, anchor=west}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[c] (c1) at (0,1.6)  {1.\ \ contains the subtheory $A_E$};
  \node[c] (c2) at (0,0.0)  {2.\ \ Prb sigma proves Prb Prb sigma};
  \node[c, draw=acc] (c3) at (0,-1.6) {3.\ \ modus ponens holds under Prb};
\end{tikzpicture}
$$

## The second incompleteness theorem

Formalizing the unprovability of the Gödel sentence inside a sufficiently strong theory gives the key
conditional: consistency would imply the Gödel sentence is unprovable.

> **Lemma (Formalized unprovability).** If $T$ is sufficiently strong and $A_E \vdash
> (\sigma \leftrightarrow \neg\,\Prb_T\,\sigma)$, then $T \vdash
> (\Cons\,T \to \neg\,\Prb_T\,\sigma)$.

> **Proof.** The choice of $\sigma$ gives $T \vdash \big(\sigma \to (\Prb_T
> \,\sigma \to 0 = S0)\big)$. Applying reflection and then formalized modus ponens,
>
> $$
> T \vdash \big(\Prb_T\,\sigma \to \Prb_T(\Prb_T\,\sigma \to 0 = S0)\big),
> $$
>
> and a second use of formalized modus ponens yields $T \vdash \big(\Prb_T
> \,\sigma \to (\Prb_T\,\Prb_T\,\sigma \to \neg\,\Cons\,
> T)\big)$. Combined with condition 2, $\Prb_T\,\sigma \to \Prb_T\,
> \Prb_T\,\sigma$, sentential logic delivers $\Prb_T\,\sigma \to
> \neg\,\Cons\,T$, which is the contrapositive of the claim.
> $\blacksquare$

> **Worked example (The internalized argument, line by line).** Each
> derivability condition enters at one step. With $\Cons\,T = \neg\,\Prb_T(0 =
> S0)$ and $\sigma$ the Gödel sentence,
> $$
> \begin{aligned}
> &T \vdash \sigma \to (\Prb_T\,\sigma \to 0 = S0) && \text{choice of } \sigma \\
> &T \vdash \Prb_T\,\sigma \to \Prb_T(\Prb_T\,\sigma \to 0 = S0) && \text{reflection, then condition 3} \\
> &T \vdash \Prb_T\,\sigma \to (\Prb_T\,\Prb_T\,\sigma \to \neg\,\Cons\,T) && \text{condition 3 again} \\
> &T \vdash \Prb_T\,\sigma \to \neg\,\Cons\,T && \text{condition 2, sentential logic}
> \end{aligned}
> $$
> The first line unwinds $\sigma$; reflection lifts it under $\Prb_T$; condition
> 3 (formalized modus ponens) discharges the two nested provability boxes; and
> condition 2 (formalized reflection) supplies $\Prb_T\,\sigma \to \Prb_T\,
> \Prb_T\,\sigma$ so the last box drops. Contraposing the final line gives $T
> \vdash (\Cons\,T \to \neg\,\Prb_T\,\sigma)$.

> **Theorem (Gödel's second incompleteness theorem, 1931).** If $T$ is a
> sufficiently strong recursively axiomatizable theory, then $T \vdash
> \Cons\,T$ if and only if $T$ is inconsistent.

> **Proof.** If $T \vdash \Cons\,T$, then by the formalized lemma $T \vdash
> \neg\,\Prb_T\,\sigma$, and the choice of $\sigma$ gives $T \vdash
> \sigma$. By the unformalized unprovability lemma, $T$ is inconsistent. $\blacksquare$

$$
% caption: Assuming Prb sigma, condition 2 gives Prb Prb sigma while the choice of
% sigma gives Prb of not-Prb sigma; formalized modus ponens collides them into a proof
% of 0 = S0, so Con T (which forbids that proof) is itself unprovable.
\begin{tikzpicture}[font=\small, >=stealth,
  b/.style={draw, minimum width=34mm, minimum height=9mm}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[b] (a) at (0,3.0)  {Prb sigma};
  \node[b] (l) at (-2.9,1.2) {Prb Prb sigma};
  \node[b] (r) at (2.9,1.2)  {Prb of not-Prb sigma};
  \node[b] (m) at (0,-0.6) {Prb of 0 = S0};
  \node[draw=acc, thick, minimum width=44mm, minimum height=10mm, align=center] (out) at (0,-2.6)
    {Con T is not provable};
  \draw[->, acc, thick] (a) -- (l);
  \draw[->, acc, thick] (a) -- (r);
  \node[font=\footnotesize, anchor=east] at (-1.7,2.35) {condition 2};
  \node[font=\footnotesize, anchor=west] at (1.7,2.35) {choice of sigma};
  \draw[->, acc, thick] (l) -- (m);
  \draw[->, acc, thick] (r) -- (m);
  \node[font=\footnotesize, anchor=west] at (1.7,0.0) {formalized modus ponens};
  \draw[->, black, thick] (m) -- (out);
\end{tikzpicture}
$$

An inconsistent theory proves everything, including its own (false) consistency
statement; the theorem says this is the only way a sufficiently strong theory can
prove its consistency.

## Löb's theorem

The same formalized argument, with the fixed refutable sentence $0 = S0$ replaced
by an arbitrary $\tau$, gives a companion result. Build $\sigma$ to say "if I am
provable, then $\tau$."

> **Lemma (Löb's derivability lemma).** If $A_E \vdash (\sigma \leftrightarrow (\Prb_T\,\sigma
> \to \tau))$ and $T \vdash \sigma$, then $T \vdash \tau$.

Its formalization runs exactly as the formalized unprovability lemma: from $T \vdash (\sigma
\to (\Prb_T\,\sigma \to \tau))$, reflection and two applications of
formalized modus ponens give $T \vdash (\Prb_T\,\sigma \to \Prb_T
\,\tau)$.

> **Theorem (Löb, 1955).** If $T$ is sufficiently strong and $T \vdash
> (\Prb_T\,\tau \to \tau)$, then $T \vdash \tau$.

> **Proof.** Construct $\sigma$ saying "if I am provable then $\tau$." From the
> formalized lemma $T \vdash (\Prb_T\,\sigma \to \Prb_T\,\tau)$, and
> the hypothesis $T \vdash (\Prb_T\,\tau \to \tau)$ then gives $T \vdash
> (\Prb_T\,\sigma \to \tau)$, which is $\sigma$; so $T \vdash \sigma$, and
> by Löb's derivability lemma, $T \vdash \tau$. $\blacksquare$

Since $T \vdash \tau$ trivially yields $T \vdash (\Prb_T\,\tau \to
\tau)$, Löb's theorem is the equivalence $T \vdash (\Prb_T\,\tau \to
\tau) \Leftrightarrow T \vdash \tau$: a theory proves "if I prove $\tau$ then
$\tau$" only when it already proves $\tau$. Taking $\tau$ to be $0 = S0$ recovers
the second incompleteness theorem, since $\Cons\,T = \neg\,\Prb_T
(0 = S0)$ is exactly $\Prb_T(0 = S0) \to 0 = S0$ up to sentential logic.

> **Worked example (The Henkin sentence is provable).** Where the Gödel
> sentence asserts its own unprovability, the Henkin sentence asserts its own
> provability. Let $T$ be sufficiently strong and let $\eta$ be a fixed point of
> $\Prb_T$,
> $$
> A_E \vdash \big(\eta \leftrightarrow \Prb_T\,\eta\big).
> $$
> The right-to-left half is $T \vdash (\Prb_T\,\eta \to \eta)$, which is exactly
> Löb's hypothesis at $\tau = \eta$. Löb's theorem then delivers
> $$
> T \vdash \eta.
> $$
> "I am provable" is provable — and, being a theorem, true. The self-reference
> that makes the Gödel sentence undecidable makes the Henkin sentence a theorem;
> the direction of the internal claim flips the verdict.

## Which theories are sufficiently strong

The finite subtheory $A_E$ is not sufficiently strong; conditions 2 and 3 require
proving general facts about provability, which needs induction. Two theories that
do satisfy all three are worth naming.

- **Peano arithmetic (PA).** The axioms of $A_E$ together with every induction
  axiom, the universal closure of $\big(\varphi(0) \wedge \forall x(\varphi(x)
  \to \varphi(Sx))\big) \to \forall x\,\varphi(x)$ for each formula $\varphi$.
  Induction is what lets one prove commutativity of addition, and formalized
  reflection and modus ponens, inside the theory.
- **Set theory (ST).** The number-theoretic sentences provable in an axiomatic
  set theory such as Zermelo–Fraenkel, via the standard interpretation of
  arithmetic in sets.

PA is consistent because it is true in $\fN$; the second theorem then
says PA cannot prove $\Cons(\text{PA})$. We know PA is consistent by an
argument carried out in informal mathematics, or in set theory — so set theory
has higher consistency strength, proving $\Cons(\text{PA})$ where PA
cannot. But the grounds for believing set theory consistent are thinner: there
is no evident "standard model of set theory" to point to, the way $\fN$
underwrites PA.

$$
% caption: Consistency strength climbs; each theory proves the consistency of
% the one below, and by the second theorem none proves its own.
\begin{tikzpicture}[font=\small, >=stealth,
  t/.style={draw, minimum width=32mm, minimum height=10mm}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[t] (ae) at (0,0)   {subtheory $A_E$};
  \node[t] (pa) at (0,1.7) {PA};
  \node[t, draw=acc] (st) at (0,3.4) {set theory};
  \draw[->, acc, thick] (pa.west) to[bend left=55] node[left, font=\footnotesize] {proves Con of} (ae.west);
  \draw[->, acc, thick] (st.east) to[bend right=55] node[right, font=\footnotesize] {proves Con of} (pa.east);
  \node[font=\footnotesize, text=black, align=center] at (0,4.4) {none proves its own Con};
\end{tikzpicture}
$$

## Set theory and Hilbert's program

Set theory gets a separate incompleteness argument because it yields the
undecidability results for its own language. Arithmetic embeds in set theory: take
$0 = \emptyset$ and $n + 1 = n \cup \{n\}$, so each number is the set of smaller
numbers, and let $\omega$ be the collection of these number-sets. Translating the
symbols of $A_E$ into set-theoretic formulas — $\pi_\forall$ from "$v_1 \in
\omega$," $\pi_0$ from "$v_1 = \emptyset$," $\pi_S$ from "$v_2 = v_1 \cup
\{v_1\}$," and $\pi_+, \pi_\cdot, \pi_E$ from the recursion equations — gives an
interpretation $\pi$ of $\Cn A_E$ into ST. Verifying it makes seventeen
demands on ST, each an everyday fact about $\omega$ (that $\emptyset$ is unique
and lies in $\omega$, that addition is well defined by recursion on $\omega$, and
so on), so a finite $\Delta \subseteq \mathrm{ST}$ already interprets
$\Cn A_E$.[^interp]

> **Theorem (Strong undecidability of set theory).** If $T$ is a theory in
> the language of set theory with $T \cup \Delta$ consistent, then $T$ is not
> recursive.

The proof transfers nonrecursiveness backward along the interpretation. The
preimage $\pi^{-1}[\Theta]$ of $\Theta = \Cn(T \cup \Delta)$ is a
consistent number-theoretic theory containing $A_E$, hence nonrecursive by strong
undecidability of $\Cn A_E$; and the translation $\sigma \mapsto
\#(\sigma^\pi)$ is recursive, so $\Theta$ cannot be recursive without making its
preimage recursive.[^37e] Two consequences follow.

- **Incompleteness of set theory.** If set theory is consistent, it is not
  complete: its axioms are recursive, so completeness would make it recursive.
- **Church's theorem, minimal vocabulary.** In the language with equality and
  one two-place predicate symbol, the set of valid sentences is not recursive.
  This is Church's theorem at its sharpest lower bound on the vocabulary.

The whole development can itself be carried out inside ST, since essentially all
of mathematics can. Then the informal implication "if ST is consistent, then
$\sigma^\pi$ is not a theorem of ST" becomes a deduction within ST of a formal
sentence $\big(\Cons(\mathrm{ST}) \to \sigma^\pi\big)$, where
$\sigma^\pi$ is itself the set-theoretic sentence asserting its own
unprovability.

> **Theorem (Gödel's second incompleteness theorem for set theory).** The
> sentence $\Cons(\mathrm{ST})$ is not a theorem of ST, unless ST is
> inconsistent.

> **Proof.** With $\big(\Cons(\mathrm{ST}) \to \sigma^\pi\big)$ a theorem
> of ST, a proof of $\Cons(\mathrm{ST})$ would give a proof of $\sigma^\pi$;
> but $\sigma^\pi \in \mathrm{ST}$ forces ST inconsistent. $\blacksquare$

This closes Hilbert's program in its original form. Before Gödel, one could hope
to prove $\Cons(\mathrm{ST})$ from assumptions weaker than the axioms of
set theory — ideally assumptions already known to be consistent, securing the
foundations from below. The second theorem shows $\Cons(\mathrm{ST})$ is
not provable in any subtheory of ST, so no such self-certification exists. A
consistent, recursively axiomatized, sufficiently strong theory can neither
decide every sentence in its language nor prove its own consistency. What remains
is to add axioms, judged by whether they both strengthen the theory and match our
informal understanding of the objects they describe.

[^open]: Enderton, §3.7 — the setup: a recursively axiomatizable theory with recursive axiom set, the provability predicate returning to item 20 of §3.4, and the numeral notation for Gödel numbers. Lemma 37A (reflection), Lemma 37B (unprovability of the Gödel sentence), and Lemma 37C (Löb's derivability lemma) are the provability-predicate facts driving the second theorem.
[^interp]: Enderton, §3.7 — the interpretation $\pi$ of $\Cn A_E$ into set theory via $0 = \emptyset$, $n+1 = n \cup \{n\}$, and $\omega$, and the seventeen demands verifying it is an interpretation.
[^37e]: Enderton, §3.7, Theorem 37D and Lemma 37E — the strong undecidability of set theory and the recursive dependence of $\#(\sigma^\pi)$ on $\sigma$ that transfers nonrecursiveness along the interpretation, with Corollaries 37F and 37G.