---
title: Incompleteness, Undecidability, and Church's Theorem
module: Arithmetization and the Incompleteness Theorems
moduleNumber: 7
lessonNumber: 2
order: 702
summary: >
  The fixed-point lemma manufactures a sentence that talks about its own Gödel
  number. Pointed at truth it gives Tarski's theorem — arithmetic truth is not
  arithmetically definable; pointed at provability it gives Gödel's first
  incompleteness theorem and the undecidability of the theory of the natural
  numbers, and, applied to validity, Church's theorem that first-order logic is
  undecidable. The set of theorems of a recursive theory is only recursively
  enumerable — the gap between provable and true.
topics: [Arithmetization and the Incompleteness Theorems]
sources:
  - book: Enderton
    ref: "Ch. 3 — Undecidability; §3.5 Incompleteness and Undecidability"
draft: false
---

The [arithmetization of syntax](/logic/incompleteness/arithmetization-of-syntax)
attached a Gödel number to every expression and made the syntactic relations
representable in $\Cn A_E$. Self-reference now becomes a theorem. Throughout,
the language is the language of $\fN$, so "theory" means a theory in that
language and $\Cn$ closes under its consequences. Write $\ulcorner \varphi
\urcorner$ for the numeral $S^{\#\varphi}0$ that names the Gödel number of
$\varphi$; a formula $\beta$ with one free variable, evaluated at $\ulcorner
\varphi\urcorner$, then makes an assertion about $\varphi$.[^open]

## The fixed-point lemma

One construction underlies the rest: for any property $\beta$ of Gödel
numbers there is a sentence that asserts $\beta$ holds of itself.

> **Lemma (Fixed point).** For any formula $\beta$ in which only $v_1$ occurs
> free, there is a sentence $\sigma$ such that
> $$
> A_E \;\vdash\; \big[\, \sigma \leftrightarrow \beta(\ulcorner \sigma \urcorner) \,\big].
> $$

The sentence $\sigma$ can be read as saying "$\beta$ is true of me." It says no
such thing on its own — it is a string that, under $\fN$, speaks of
numbers and their successors and products. Only because we have paired numbers
with expressions can $\sigma$ be understood as referring to a formula, in this
case itself.

> **Proof.** Let $\theta(v_1, v_2, v_3)$ functionally represent in $\Cn A_E$
> the substitution function whose value at $\langle \#\alpha, n\rangle$ is
> $\#\big(\alpha(S^{n}0)\big)$; this is representable by the substitution and
> numeral items of the
> [arithmetization catalog](/logic/incompleteness/arithmetization-of-syntax).
> Consider the formula
>
> $$
> \forall v_3\,\big[\, \theta(v_1, v_1, v_3) \to \beta(v_3) \,\big], \tag{1}
> $$
>
> which has only $v_1$ free. Let $q = \#(1)$ be its Gödel number, and let $\sigma$
> be the result of substituting the numeral $S^{q}0$ for $v_1$ in $(1)$,
>
> $$
> \sigma \;=\; \forall v_3\,\big[\, \theta(S^{q}0, S^{q}0, v_3) \to \beta(v_3) \,\big].
> $$
>
> Because $\theta$ functionally represents a function whose value at $\langle q,
> q\rangle$ is $\#\sigma$, the subtheory proves that $v_3$ ranges to exactly the
> right numeral,
>
> $$
> A_E \;\vdash\; \forall v_3\,\big[\, \theta(S^{q}0, S^{q}0, v_3) \leftrightarrow v_3 = S^{\#\sigma}0 \,\big]. \tag{2}
> $$
>
> Reading $\sigma$ at $v_3 = \ulcorner\sigma\urcorner$ and using $(2)$ gives $A_E;
> \sigma \vdash \beta(\ulcorner\sigma\urcorner)$, and $(2)$ also yields the
> converse $\beta(\ulcorner\sigma\urcorner) \to \sigma$. Together these are the
> biconditional. $\blacksquare$

$$
% caption: The diagonal substitution feeds a formula its own Gödel number, so
% $\sigma$ ends up provably equivalent to the assertion $\beta$ made about $\sigma$.
\begin{tikzpicture}[font=\small, >=stealth]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[draw, minimum width=30mm, minimum height=11mm, align=center] (sig) at (0,1.4)
    {the formula sigma};
  \node[draw=acc, thick, minimum width=42mm, minimum height=11mm, align=center] (beta) at (0,-1.4)
    {beta of the code of sigma};
  \draw[->, acc, thick] (sig.east) to[bend left=42] node[right=2mm, font=\footnotesize, align=center] {provably\\equivalent} (beta.east);
  \draw[->, black, thick] (beta.west) to[bend left=42] node[left=2mm, font=\footnotesize] {asserts} (sig.west);
\end{tikzpicture}
$$

## Undefinability of truth

Applied to the set of true sentences, the lemma refutes any formula proposed
to define truth. Let $\#\Th \fN$ be the set of Gödel numbers of
sentences true in $\fN$. This first application needs only the semantic
form $\models_{\fN} \sigma \leftrightarrow \beta(\ulcorner\sigma\urcorner)$
of the fixed point, not provability in $A_E$.

> **Theorem (Tarski's undefinability of truth, 1933).** The set
> $\#\Th \fN$ is not definable in $\fN$.

> **Proof.** Take any formula $\beta$ suspected of defining
> $\#\Th \fN$. Apply the fixed-point lemma to $\neg\,\beta$,
> producing $\sigma$ with $\models_{\fN} \sigma \leftrightarrow
> \neg\,\beta(\ulcorner\sigma\urcorner)$ — a sentence indirectly saying "I am
> false." Then
>
> $$
> \models_{\fN} \sigma \quad\Longleftrightarrow\quad \models_{\fN} \beta(\ulcorner\sigma\urcorner),
> $$
>
> so either $\sigma$ is true while its Gödel number lies outside the set $\beta$
> defines, or $\sigma$ is false while its number lies inside. Either way $\beta$
> fails to define $\#\Th \fN$. $\blacksquare$

Because every recursive set is definable in $\fN$ (recursive relations are
arithmetical), an undefinable set cannot be recursive.

> **Corollary (The theory of the naturals is not recursive).** $\#\Th \fN$ is not recursive.

The theory of the natural numbers is undecidable: no algorithm tests, of an
arbitrary arithmetic sentence, whether it is true.

> **Worked example (One construction, two conclusions).** The fixed point
> applied to $\neg\,\beta$ gives $\sigma$ with $\sigma \leftrightarrow
> \neg\,\beta(\ulcorner\sigma\urcorner)$, read "$\beta$ is false of me." What
> follows depends on what $\beta$ is asked to define.
> - **$\beta$ defines truth $\#\Th\fN$.** Then $\models_{\fN}\sigma \iff
>   \models_{\fN}\beta(\ulcorner\sigma\urcorner) \iff \#\sigma \in \#\Th\fN
>   \iff \models_{\fN}\sigma$, which forces $\models_{\fN}\sigma$ to disagree
>   with itself. No $\beta$ defines truth; truth is not arithmetical.
> - **$\beta$ defines provability $\#\Cn A$** for a recursive $A \subseteq
>   \Th\fN$ (available, since provability is r.e. hence arithmetical). No
>   contradiction results: $\sigma$ is simply true and $A$-unprovable.
>   Provability is definable, but does not coincide with truth.
>
> The construction is identical; only the definability of the target changes
> the verdict.

## Gödel's first incompleteness theorem

The undecidability of truth combines with the recursiveness bound (a complete
recursive theory has a recursive theorem set, item 21) to force incompleteness
on every reasonable axiomatization of arithmetic.

> **Theorem (Gödel's first incompleteness theorem, 1931).** If $A \subseteq
> \Th \fN$ and $\#A$ is recursive, then $\Cn A$ is not
> a complete theory.

> **Proof.** Since $A \subseteq \Th \fN$, we have $\Cn A
> \subseteq \Th \fN$. If $\Cn A$ were complete then its
> theorem set would be recursive by item 21; but $\Cn A$ complete forces
> $\Cn A = \Th \fN$, whose theorem set is not recursive
> by the non-recursiveness of true arithmetic. $\blacksquare$

No consistent recursive set of true axioms decides all of arithmetic; in
particular $\Cn A_E \neq \Th \fN$, and adding any
recursive set of further truths does not close the gap. The proof of Tarski's
theorem even exhibits the missing sentence. Fix a recursive $A \subseteq
\Th \fN$ and let $\beta$ define $\#\Cn A$ in
$\fN$ (available because $\#\Cn A$ is recursively enumerable,
hence arithmetical). The fixed point $\sigma$ against $\neg\,\beta$ indirectly
says "I am not a theorem of $A$," and it is true and unprovable:

$$
A \not\vdash \sigma \qquad\text{and}\qquad A \not\vdash \neg\,\sigma.
$$

This is nearer Gödel's original route, which did not detour through truth in
$\fN$.

> **Worked example (The Gödel sentence is true and unprovable).** Fix a
> recursive $A \subseteq \Th\fN$ and a formula $\beta$ defining $\#\Cn A$ in
> $\fN$; the fixed point against $\neg\,\beta$ gives $\sigma$ with
> $\models_{\fN} \sigma \leftrightarrow \neg\,\beta(\ulcorner\sigma\urcorner)$,
> read "I am not a theorem of $A$." Trace the three claims, keeping $\vdash$
> (provability from $A$) and $\models_{\fN}$ (truth in the standard model)
> distinct.
> - **$A \not\vdash \sigma$.** If $A \vdash \sigma$, then $\#\sigma \in \#\Cn A$,
>   so $\models_{\fN} \beta(\ulcorner\sigma\urcorner)$, so $\models_{\fN}
>   \neg\,\sigma$. But $A \subseteq \Th\fN$ makes $A \vdash \sigma$ give
>   $\models_{\fN}\sigma$ — a contradiction.
> - **$\sigma$ is true.** From $A \not\vdash \sigma$, $\#\sigma \notin \#\Cn A$,
>   so $\models_{\fN} \neg\,\beta(\ulcorner\sigma\urcorner)$, hence
>   $\models_{\fN} \sigma$.
> - **$A \not\vdash \neg\,\sigma$.** If $A \vdash \neg\,\sigma$, then
>   $\models_{\fN} \neg\,\sigma$, contradicting the truth of $\sigma$.
>
> So $\sigma$ is true in $\fN$ yet $A$ neither proves nor refutes it: exactly
> incompleteness.

$$
% caption: The Gödel sentence is true but sits outside the theorems; its negation
% is false, outside the truths entirely — so neither is provable and the theory is incomplete.
\begin{tikzpicture}[font=\small, >=stealth]
  \definecolor{acc}{HTML}{4A6FA5}
  \draw[black, thick] (0,0) ellipse (4.2 and 2.4);
  \node[font=\footnotesize, text=black, anchor=south] at (0,1.9) {true sentences};
  \draw[acc, thick, fill=acc!8] (-1.6,0) ellipse (2.1 and 1.5);
  \node[font=\footnotesize, text=acc] at (-1.6,0) {theorems of $A$};
  \fill[acc] (2.0,0.55) circle (2pt);
  \node[anchor=west, font=\footnotesize] at (2.2,0.55) {sigma};
  \fill[black] (0,-3.2) circle (2pt);
  \node[anchor=west, font=\footnotesize] at (0.2,-3.2) {not sigma};
  \node[font=\footnotesize, text=black, anchor=north] at (2.0,0.25) {true, unprovable};
  \node[font=\footnotesize, text=black, anchor=north] at (0.1,-3.45) {false};
\end{tikzpicture}
$$

## Strong undecidability and incompleteness from consistency

Truth in $\fN$ is more than the argument needs. The same fixed-point
move, run against a formula defining a recursive theory, shows that no consistent
extension of the subtheory can be decidable; the axioms need not be true.

First, adding finitely many axioms preserves recursiveness of the theorem set,
by the deduction theorem.

> **Lemma (Adding an axiom preserves recursiveness).** If $\#\Cn \Gamma$ is recursive, then
> $\#\Cn(\Gamma; \tau)$ is recursive, because $\alpha \in
> \Cn(\Gamma;\tau)$ iff $(\tau \to \alpha) \in \Cn \Gamma$.

> **Theorem (Strong undecidability of $\Cn A_E$).** Let $T$ be a
> theory such that $T \cup A_E$ is consistent. Then $T$ is not recursive.

> **Proof.** Let $T' = \Cn(T \cup A_E)$; since $A_E$ is finite, if $T$ were
> recursive then $T'$ would be too by the axiom-addition lemma. Suppose $T'$ is recursive, so it
> is represented in $\Cn A_E$ by some $\beta$. The fixed-point lemma gives
> $\sigma$ with $A_E \vdash [\sigma \leftrightarrow \neg\,\beta(\ulcorner\sigma
> \urcorner)]$, indirectly asserting "I am not in $T'$." Both memberships are
> untenable:
>
> $$
> \sigma \notin T'
> \;\Rightarrow\; A_E \vdash \neg\,\beta(\ulcorner\sigma\urcorner)
> \;\Rightarrow\; A_E \vdash \sigma
> \;\Rightarrow\; \sigma \in T',
> $$
> $$
> \sigma \in T'
> \;\Rightarrow\; A_E \vdash \beta(\ulcorner\sigma\urcorner)
> \;\Rightarrow\; A_E \vdash \neg\,\sigma
> \;\Rightarrow\; \neg\,\sigma \in T',
> $$
>
> the first contradicting itself and the second contradicting the consistency of
> $T'$. So $T'$, and hence $T$, is not recursive. $\blacksquare$

> **Corollary (Essential incompleteness).** If $\#\Gamma$ is recursive and $\Gamma \cup A_E$ is
> consistent, then $\Cn \Gamma$ is not complete.

This is Gödel's theorem again, with "true in $\fN$" weakened to "merely
consistent with $A_E$." Any recursively axiomatized theory that so much as agrees
with the finite subtheory is incomplete: the incompleteness is a fact about
axiomatizability, not about truth.

## Church's theorem

The smallest theory in the language is the set of valid sentences, $\Cn 
\emptyset$. It is consistent with $A_E$ (their closure is $\Cn A_E$), so
strong undecidability applies to it directly.

> **Theorem (Church, 1936).** The set of Gödel numbers of valid sentences in the
> language of $\fN$ is not recursive.

First-order validity is undecidable: no algorithm tests an arbitrary sentence for
logical truth. The result does not depend on the arithmetic vocabulary. It holds
for any language containing at least one two-place predicate symbol, because the
arithmetic can be interpreted there; on the other hand some minimum is needed —
in the language of pure equality, or with only $\forall$ and one-place predicate
symbols, validity is decidable.[^church]

| Property | Truth $\Th \fN$ | Provability $\Cn A_E$ | Validity $\Cn \emptyset$ |
| --- | --- | --- | --- |
| Definable in $\fN$? | no (Tarski) | yes | yes |
| Recursively enumerable? | no | yes | yes |
| Recursive (decidable)? | no | no | no |
| Complete theory? | yes | no | no |

## Recursive enumerability

The coded-deduction recursion places provability one quantifier away from
recursiveness.

> **Definition (Recursively enumerable).** An $m$-ary relation $R$ is recursively
> enumerable (r.e.) iff $R = \{\vec{a} : \exists b\, \langle \vec{a}, b\rangle \in
> Q\}$ for some recursive $Q$ — equivalently, $R$ is the domain of a recursive
> relation.

Existentially quantifying a defining formula shows every r.e. relation is
definable in $\fN$, and collapsing a block of existential quantifiers
into one (via sequence coding) shows the several characterizations agree.[^35e]
The r.e. relations are the formal counterpart of the effectively enumerable ones:
a relation is effectively enumerable iff it is the domain of a decidable
relation, and identifying decidable with recursive identifies the two notions
(Church's thesis, second form).

> **Theorem (Recursive iff both it and its complement are recursively enumerable).** A relation is recursive if and only if both it and its
> complement are recursively enumerable.

> **Proof.** A recursive relation and its complement are both recursive, hence
> r.e. Conversely, if $\vec{a} \in P \Leftrightarrow \exists b\,\langle \vec{a},
> b\rangle \in Q$ and $\vec{a} \notin P \Leftrightarrow \exists b\,\langle \vec{a},
> b\rangle \in R$ for recursive $Q, R$, then $f(\vec{a}) = $ the least $b$ landing
> in $Q$ or $R$ is recursive, and $\vec{a} \in P \Leftrightarrow \langle \vec{a},
> f(\vec{a})\rangle \in Q$. $\blacksquare$

Provability is the leading example of an r.e. set that need not be recursive.

> **Theorem (Enumerability of the consequences of a recursive axiom set).** If $\#A$ is recursive, then $\#\Cn A$ is recursively
> enumerable.

```algorithm
caption: $\textsc{Enumerate}(A)$ — listing the theorems of a recursive theory
for $d \gets 0, 1, 2, \dots$ do
  if $\textsc{IsDeduction}(d, A)$ then
    $a \gets (d)_{\lh\,d - 1}$   // the last line of the proof coded by $d$
    output $a$                            // a theorem; every theorem appears eventually
```

The procedure never halts and never decides non-theoremhood: if $a$ is not a
theorem, the search runs forever. This is the exact gap between provable and
true. With a recursive set of axioms the theorems are at best recursively
enumerable, whereas $\Th \fN$ is not even definable in
$\fN$. Expanding the language or adding axioms changes nothing: as long
as deductions are recursively recognizable, the theorems stay merely r.e. The
set of number-theoretic sentences provable in any standard axiomatic set theory
is r.e., includes $A_E$, and (barring inconsistency) is consistent — so that set
theory is itself nonrecursive and incomplete.

$$
% caption: Recursive sits inside recursively enumerable inside arithmetical
% (definable in $\fN$); the set of arithmetic truths lies outside all three.
\begin{tikzpicture}[font=\small, >=stealth]
  \definecolor{acc}{HTML}{4A6FA5}
  \draw[black, thick] (0,0) ellipse (4.6 and 2.8);
  \node[font=\footnotesize, text=black, anchor=south] at (0,2.85) {arithmetical};
  \draw[acc, thick] (-0.4,-0.1) ellipse (3.0 and 1.9);
  \node[font=\footnotesize, text=acc, anchor=south] at (-0.4,1.15) {recursively enumerable};
  \draw[black, thick, fill=acc!8] (-0.6,-0.25) ellipse (1.7 and 1.1);
  \node[font=\footnotesize] at (-0.6,-0.25) {recursive};
  \fill[black] (4.6,2.4) circle (2.2pt);
  \node[anchor=west, font=\footnotesize, align=left] at (4.8,2.4) {Th $\mathfrak{N}$};
\end{tikzpicture}
$$

## Weak representability

A recursive relation is represented outright: the theory settles each instance
positively or negatively. An r.e. relation cannot be, unless it is recursive, but
it can be represented halfway.

> **Definition (Weak representability).** A formula $\psi$ (free variables among
> $v_1, \dots, v_n$) weakly represents an $n$-ary relation $Q$ in a theory $T$
> iff for all $\vec{a}$,
> $$
> \vec{a} \in Q \;\iff\; \psi(\ulcorner a_1\urcorner, \dots, \ulcorner a_n\urcorner) \in T.
> $$

Membership is now signalled only by provability of the positive instance;
nonmembership produces no proof of the negation, merely the absence of a proof of
the instance. For an r.e. $Q$ with $a \in Q \Leftrightarrow \exists b\, \langle
a, b\rangle \in R$ and $\rho$ representing $R$, the formula $\exists v_2\,
\rho(v_1, v_2)$ weakly represents $Q$ in $\Cn A_E$; the nonmembership
direction uses that $A_E$ is $\omega$-consistent, so $A_E \vdash \neg\,
\rho(\ulcorner a\urcorner, S^{b}0)$ for every $b$ blocks $A_E \vdash \exists v_2\,
\rho(\ulcorner a\urcorner, v_2)$.[^omega]

> **Theorem (Weak representability equals recursive enumerability).** A relation is weakly representable in $\Cn A_E$ if
> and only if it is recursively enumerable.

Representable, definable, and weakly representable line up exactly with recursive,
arithmetical, and recursively enumerable.

| Notion in the theory | Class of relations |
| --- | --- |
| Representable in $\Cn A_E$ | recursive |
| Weakly representable in $\Cn A_E$ | recursively enumerable |
| Definable in $\fN$ | arithmetical |

## The arithmetical hierarchy

Definability in $\fN$ admits degrees, organized by counting alternations
of unbounded quantifiers over a recursive matrix. Let $\Sigma_1$ be the r.e.
relations (one existential quantifier away from recursive) and $\Pi_1$ their
complements. In general $Q \in \Sigma_k$ when it has the form $\{\vec{a} :
\exists b_1\, \forall b_2 \cdots \langle \vec{a}, \vec{b}\rangle \in R\}$ with $k$
alternating quantifiers led by $\exists$ over recursive $R$, and $Q \in \Pi_k$
when the leading quantifier is $\forall$. Writing $\Delta_k = \Sigma_k \cap
\Pi_k$, the base case $\Delta_1$ is the recursive relations, which is the
content of the complementary-enumerability theorem restated as $\Delta_1 = \Sigma_1 \cap \Pi_1$.

$$
% caption: The arithmetical hierarchy; $\Delta_1$ is the recursive relations, and
% each level sits inside both classes one step up, with all inclusions proper.
\begin{tikzpicture}[font=\small, >=stealth,
  n/.style={draw, minimum width=15mm, minimum height=8mm}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[n, draw=acc] (d1) at (0,0) {Delta 1};
  \node[n] (s1) at (-2.2,1.4) {Sigma 1};
  \node[n] (p1) at (2.2,1.4)  {Pi 1};
  \node[n] (d2) at (0,2.8) {Delta 2};
  \node[n] (s2) at (-2.2,4.2) {Sigma 2};
  \node[n] (p2) at (2.2,4.2)  {Pi 2};
  \draw[->, black] (d1) -- (s1);
  \draw[->, black] (d1) -- (p1);
  \draw[->, black] (s1) -- (d2);
  \draw[->, black] (p1) -- (d2);
  \draw[->, black] (d2) -- (s2);
  \draw[->, black] (d2) -- (p2);
  \node[font=\footnotesize, text=black, anchor=west] at (3.1,0.7) {recursive};
  \draw[->, black] (2.95,0.7) -- (d1.east);
\end{tikzpicture}
$$

> **Theorem (Arithmetical hierarchy characterization).**[^hierarchy] A relation is arithmetical (definable in $\fN$) if
> and only if it is in $\Sigma_k$ for some $k$, equivalently in $\Pi_l$ for some
> $l$.

Every arithmetical relation lands somewhere on the ladder: put its defining
formula in prenex form, whose quantifier-free matrix defines a recursive relation
(quantifier-free formulas are numeralwise determined by $A_E$), and read off the
level from the quantifier prefix. Bounded quantifiers can be pushed inward past
the counting, since $(\forall i < n)(\exists d)\, P \Leftrightarrow (\exists
d)(\forall i < n)\, P$ after collapsing, so they never raise a relation's level.
The hierarchy also lifts to theories: if $\#A$ is in $\Sigma_k$ for $k > 0$, then
$\#\Cn A$ is again in $\Sigma_k$, so provability from a
$\Sigma_k$ axiom set stays at level $k$.

> **Worked example (Locating a set in the hierarchy).** Let $B$ collect the
> Gödel numbers of formulas $\alpha$ for which, at some stage $n$, $A_E \vdash
> \alpha(S^n 0)$ while $A_E \vdash \neg\,\alpha(S^i 0)$ for every $i < n$.
> Membership unfolds as
> $$
> a \in B \iff [a \text{ codes a wff } \alpha] \wedge \exists n\, \exists d\,[d \text{ codes a deduction of } \alpha(S^n 0)]
> $$
> $$
> \wedge\ (\forall i < n)(\exists d_i)\,[d_i \text{ codes a deduction of } \neg\,\alpha(S^i 0)].
> $$
> The deduction predicates in brackets are recursive. Two unbounded existentials
> and one bounded universal remain. Push the bounded $\forall i < n$ past the
> existential,
> $$
> (\forall i < n)(\exists d_i)\, P \iff (\exists d)(\forall i < n)\, P',
> $$
> so it merges into the recursive matrix, and the leading existentials collapse
> to one by sequence coding. Hence $B \in \Sigma_1$: one existential quantifier
> above recursive.

Tarski's and Gödel's theorems divide cleanly. Tarski's says truth is not
arithmetical at all: $\#\Th \fN$ lies outside the whole
hierarchy. Gödel's says provability, though low in the hierarchy (it is
$\Sigma_1$), still does not coincide with truth. The [second incompleteness
theorem](/logic/incompleteness/second-incompleteness-theorem) sharpens the second
of these by turning the provability predicate on the consistency of the theory
itself.

[^open]: Enderton, §3.5 — the standing assumption that the language is that of $\fN$, and the reading of $\sigma$ as indirectly referring to itself through its Gödel number. The fixed point yields Corollary 35A (the theory of $\fN$ is not recursive), Lemma 35B (adding a finite set of axioms preserves recursiveness of the theorem set), Theorem 35C (strong undecidability of $\Cn A_E$), and Corollary 35D (essential incompleteness).
[^church]: Enderton, §3.5 and Corollary 37G — Church's theorem for the language of $\fN$, its extension to any language with a two-place predicate symbol, and the decidability of validity for the language of equality and for monadic predicate languages.
[^35e]: Enderton, §3.5, Theorems 35E–35H — the equivalent characterizations of recursive enumerability, the recursive-iff-both-r.e. theorem, and the second form of Church's thesis identifying effectively enumerable with recursively enumerable. Theorem 35I (the consequences of a recursive axiom set are recursively enumerable) is the r.e. side of provability.
[^hierarchy]: Enderton, §3.5, Theorem 35K — the arithmetical hierarchy $\Sigma_k/\Pi_k/\Delta_k$ over a recursive matrix, and the characterization of the arithmetical relations as those lying in some $\Sigma_k$ (equivalently some $\Pi_l$).
[^omega]: Enderton, §3.5 — weak representability, the definition, Theorem 35J, and the role of $\omega$-consistency in the nonmembership direction.