Logic and Computability - Cambridge III notes

Logic and Computability
Daniel Naylor

1Non-classical Logic
1.1Intuitionistic Logic
1.2The simply typed

λ

-calculus
1.3The Curry-Howard Correspondence
1.4Semantics for IPC
1.5Negative translations
2Computability
2.1Recursive functions and

λ

-computability
2.2Decidability in Logic
Index

1 Non-classical Logic

There are no non-experienced truths – L.E.J. Brouwer

1.1 Intuitionistic Logic

Idea: a proof of $φ \to ψ$ is a “procedure” that comments a proof of $φ$ into a proof of $ψ$ .

In particular, $\neg \neg φ$ is not always the same as $φ$ .

Fact: The law of excluded middle ( $φ \lor \neg φ$ ) is not generally intuitionistically valid.

Moreover, the Axiom of Choice is incompatible with intuitionistic set theory.

We take choice to mean that any family of inhabited sets admits a choice function.

Theorem 1.1.1 (Diaconescu). The law of excluded middle can be intuitionistically deduced from the Axiom of Choice.

Proof. Let $φ$ be a proposition. By the Axiom of Separation, the following are sets (i.e. we can construct a proof that they are sets):

A : = {x \in {0, 1} : φ \lor (x = 0)} B : = {x \in {0, 1} : φ \lor (x = 1)} .

As $0 \in A$ and $1 \in B$ , we have that ${A, B}$ is a family of inhabited sets, thus admits a choice function $f : {A, B} \to A \cup B$ by the Axiom of Choice. This satisfies $f (A) \in A$ and $f (B) \in B$ by definition.

Thus we have

(f (A) = 0 \lor φ) \land (f (B) = 1 \lor φ)

and $f (A), f (B) \in {0, 1}$ . Now $f (A) \in {0, 1}$ means that $(f (A) = 0) \lor (f (A) = 1)$ and similarly for $f (B)$ .

We can have the following:

(1) We have a proof of $f (A) = 1$ , so $φ \lor (1 = 0)$ has a proof, so we must have a proof of $φ$ .
(2) We have a proof of $f (B) = 0$ , which similarly gives a proof of $φ$ .
(3) We have $f (A) = 0$ and $f (B) = 1$ , in which case we can prove $\neg φ$ : given a proof of $ϕ$ , we can prove that $A = B$ (by Extensionality), in which case $0 = f (A) = f (B) = 1$ , a contradiction.

So we can always specify a proof of $φ$ or a proof of $φ$ or a proof of $\neg φ$ . □

Why bother?

Intuitionistic maths is more general: we assume less.
Several notions that are conflated in classical maths are genuinely different constructively.
Intuitionistic proofs have a computable content that may be absent in classical proofs.
Intuitionistic logic is the internal logic of an arbitrary topos.

Let’s try to formalise the BHK interpretation of logic.

We will inductively define a provability relation by enforcing rules that implement the BHK interpretation.

We will use the notation $Γ ⊢ φ$ to mean that $φ$ is a consequence of the formulae in the set $Γ$ .

Rules for Intuitionistic Propositional Calculus (IPC)

( $\land$ -I) $\frac{Γ ⊢ A, Γ ⊢ B}{Γ ⊢ A \land B}$
( $\lor$ -I) $\frac{Γ ⊢ A}{Γ ⊢ A \lor B}$ , $\frac{Γ ⊢ B}{Γ ⊢ A \lor B}$
( $\land$ -E) $\frac{Γ ⊢ A \land B}{Γ ⊢ A}$ and $\frac{Γ ⊢ A \land B}{Γ ⊢ B}$
( $\lor$ -E) $\frac{Γ, A ⊢ C Γ, B ⊢ C Γ ⊢ A \lor B}{Γ ⊢ C}$
( $\to$ -I) $\frac{Γ, A ⊢ B}{Γ ⊢ A \to B}$
( $\to$ -E) $\frac{Γ ⊢ A \to B, Γ ⊢ A}{Γ ⊢ B}$
( $⊥$ -E) $\frac{Γ ⊢ ⊥}{Γ ⊢ A}$ for any $A$
(Ax) $\frac{}{Γ, A ⊢ A}$ for any $A$
(Weak) $\frac{Γ ⊢ B}{Γ, A ⊢ B}$
(Contr) $\frac{Γ, A, A ⊢ B}{Γ, A ⊢ B}$

We obtain classical propositional logic (CPC) by adding either:

$\frac{}{Γ ⊢ A \lor \neg A}$
$\frac{Γ, \neg A ⊢ ⊥}{Γ ⊢ A}$ (reductio ad absurdum)

\frac{\begin{matrix} [A] \\ ⋮ \\ X \end{matrix} \begin{matrix} [B] \\ ⋮ \\ Y \end{matrix}}{C} (A, B)

we mean ‘if we can prove $X$ assuming $A$ and we can prove $Y$ assuming $B$ , then we can infer $C$ by “discharging / closing” the open assumptions $A$ and $B$ ’.

In particular, the ( $\to$ -I)-rule can be written as

\frac{\begin{matrix} Γ, [A] \\ ⋮ \\ B \end{matrix}}{Γ ⊢ A \to B} (A) .

We obtain intiuitionistic first-order logic (IQC) by adding rules for quantification:

( $\exists$ -I) $\frac{Γ ⊢ φ [x : = t]}{Γ ⊢ \exists x . φ (x)}$ , where $t$ is a term.
( $\exists$ -E) $\frac{Γ ⊢ \exists x . φ Γ, φ ⊢ ψ}{Γ ⊢ ψ}$ , if $x$ is not free in $Γ, ψ$ .
( $\forall$ -I) $\frac{Γ ⊢ φ}{Γ ⊢ \forall x . φ}$ if $x$ is not free in $Γ$ .
( $\forall$ -E) $\frac{Γ ⊢ \forall x . φ (x)}{Γ ⊢ φ [x : = t]}$ , where $t$ is a term.

Example 1.1.2. Let’s give a natural deduction proof of $A \land B \to B \land A$ .

\frac{\frac{\frac{[A \land B]}{A} \frac{[A \land B]}{B}}{B \land A}}{A \land B \to B \land A} (A \land B) .

Example 1.1.3. Let’s prove the Hilbert-style axioms $φ \to (ψ \to φ)$ and $(φ \to (ψ \to χ)) \to ((φ \to p s i) \to (φ \to χ))$ .

\frac{\frac{[φ] [ψ]}{ψ \to φ} (ψ)}{φ \to (ψ \to φ)} (φ)

$[φ \to (ψ \to χ)] [φ \to ψ] [φ]$	(toE)

$ψ \to χ ψ$	(toE)

$χ$	(toI,ψ)

$φ \to χ$	(toI, φ→ψ)

$(φ \to ψ) \to (φ \to χ)$	(toI, (φ→(ψ→χ)))

$(φ \to (ψ \to χ)) \to ((φ \to ψ) \to (φ \to χ))$

If $Γ$ is a set of propositions in the language and $φ$ is a proposition, we write $Γ ⊢_{IPC} φ$ , $Γ ⊢_{IQC} φ$ , $Γ ⊢_{CPC} φ$ , $Γ ⊢_{CQC} φ$ , if there is a proof of $φ$ from $Γ$ in the respective logic.

Lemma 1.1.4. Assuming that:

$Γ ⊢_{IPC} φ$
$ψ$ a proposition

Then

Γ, ψ ⊢_{IPC} φ

. Moreover, if

p

is a primitive proposition and

ψ

is any proposition, then

Γ [p : = ψ] ⊢_{IPC} φ [p : = ψ] .

Proof. Induction over the size of proofs. □

1.2 The simply typed $λ$ -calculus

For now we assume given a set $Π$ of simple types generated by a grammar

Π : = U | Π \to Π,

where $U$ is a countable set of type variables, as well as an infinite set $V$ of variables.

Definition 1.2.1 (Simply typed lambda-term). The set $Λ_{Π}$ of simply typed $λ$ -terms is defined by the grammar

Λ_{Π} : = \underset{variables}{\underset{⏟}{V}} | \underset{λ -abstraction}{\underset{⏟}{λ V : Π . Λ_{Π}}} | \underset{λ -application}{\underset{⏟}{Λ_{Π} Λ_{Π}}} .

A context is a set of pairs ${x_{1} : τ_{1}, \dots, x_{n} : τ_{n}}$ where the $x_{i}$ are (distinct) variables and each $τ_{i} \in Π$ . We write $C$ for the set of all possible contexts. Given a context $Γ \in C$ , we also write $Γ, x : τ$ for the context $Γ \cup {x : τ}$ (if $x$ does not appear in $Γ$ ).

The domain of $Γ$ is the set of variables that occur in it, and the range $| Γ |$ is the set of types that it manifests.

Definition 1.2.2 (Typability relation). We define the typability relation $⊩ \subseteq C \times Λ_{Π} \times Π$ via:

(1)
For every context $Γ$ , and variable $x$ not occurring in $Γ$ , and type $τ$ , we have $Γ, x : τ ⊩ x : τ$ .
(2)
Let $Γ$ be a context, $x$ a variable not occurring in $Γ$ , and let $σ, τ \in Π$ be types, and $M$ be a $λ$ -term. If $Γ, x : σ ⊩ M : τ$ , then $Γ ⊩ (λ x : σ . M) : (σ \to τ)$ .
(3)
Let $Γ$ be a context, $σ, τ \in Π$ be types, and $M, N \in Λ_{Π}$ be terms. If $Γ ⊩ M : (σ \to τ)$ and $Γ ⊩ N : σ$ , then $Γ ⊩ (M N) : τ$ .

Notation. We will refer to the $λ$ -calculus of $Λ_{Π}$ with this typability relation as $λ (\to)$ .

A variable $x$ occurring in a $λ$ -abstraction $λ \underset{̲}{x} : σ . M$ is bound, and it is free otherwise. We say that terms $M$ and $N$ are $α$ -equivalent if they differ only in the names of the bound variables.

If $M$ and $N$ are $λ$ -terms and $x$ is a variable, then we define the substitution of $N$ for $x$ in $M$ by:

$x [x : = N] = N$ ;
$y [x : = N] = y$ if $x \neq y$ ;
$(P Q) [x : = N] = P [x : = N] Q [x : = N]$ for $λ$ -terms $P, Q$ ;
$(λ y : σ . P) [x : = N] = λ y : σ . (P [x : = N])$ , where $x \neq y$ and $y$ is not free in $N$ .

Definition 1.2.3 (beta-reduction). The $β$ -reduction relation is the smallest relation $\to_{β}$ on $Λ_{Π}$ closed under the following rules:

$(λ x : σ . P) Q \to_{β} P [x : = Q]$ ,
if $P \to_{β} P^{'}$ , then for all variables $x$ and types $σ \in Π$ , we have $λ x : σ . P \to_{β} λ x : σ . P^{'}$ ,
$P \to_{β} P^{'}$ and $z$ as a $λ$ -term, then $P Z \to_{β} P^{'} Z$ and $Z P \to_{β} Z P^{'}$ .

We also define $β$ -equivalence $\equiv_{β}$ as the smallest equivalence relation containing $\to_{β}$ .

Example 1.2.4 (Informal). We have $(λ x : ℤ . (λ y : τ . x)) Z \to_{β} (λ y : τ . Z)$ .

When we reduce $(λ x : σ . P) Q$ , the term being reduced is called a $β$ -redex, and the result is its $β$ -contraction.

Lemma 1.2.5 (Free variables lemma). Assuming that:

$Γ ⊩ M : σ$

Then

(1) If $Γ \subseteq Γ^{'}$ , then $Γ^{'} ⊩ M : σ$ .
(2) The free variables of $M$ occur in $Γ$ .
(3) There is a context $Γ^{*} \subseteq Γ$ comprising exactly the free variables in $M$ , with $Γ^{*} ⊩ M : σ$ .

Proof. Exercise. □

Lemma 1.2.6 (Generation Lemma).

(1)
For every variable $x$ , context $Γ$ , and type $σ$ , if $Γ ⊩ x : σ$ , then $x : σ \in Γ$ ;
(2)
If $Γ ⊩ (M N) : σ$ , then there is a type $τ$ such that $Γ ⊩ M : τ \to σ$ and $Γ ⊩ N : τ$ ;
(3)
If $Γ ⊩ (λ x . M) : σ$ , then there are types $τ$ and $ρ$ such that $Γ, x : τ ⊩ M : ρ$ and $σ = (τ \to ρ)$ .

Lemma 1.2.7 (Substitution Lemma).

(1)
If $Γ ⊩ M : σ$ and $α$ is a type variable, then $Γ [α : = τ] ⊩ M : σ [α : = τ]$ ;
(2)
If $Γ, x : τ ⊩ M : σ$ and $Γ ⊩ N : τ$ , then $Γ ⊩ M [x : = N] : σ$ .

Proposition 1.2.8 (Subject reduction). Assuming that:

$Γ ⊩ M : σ$
$M \to_{β} N$

Then

Γ ⊩ N : σ

Proof. By induction on the derivation of $M \to_{β} N$ , using Lemma 1.2.6 and Lemma 1.2.7. □

Notation. We will write $M ↠_{β} N$ if $M$ reduces to $N$ after (potentially multiple) $β$ -reductions.

Theorem 1.2.9 (Church-Rosser for lambda(->)). Assuming that:

$Γ ⊩ M : σ$
$M ↠_{β} N_{1}$
$M ↠_{β} N_{2}$

Then there is a

λ

-term

L

such that

N_{1} ↠_{β} L

N_{2} ↠_{β} L

, and

Γ ⊩ L : σ

Pictorially:

Definition ( $b e t a$ -normal form). A $λ$ -term $M$ is in $β$ -normal form if there is no term $N$ such that $M \to_{β} N$ .

Corollary 1.2.10 (Uniqueness of normal form). If a simply typed $λ$ -term admits a $β$ -normal form, then it is unique.

Proposition 1.2.11 (Uniqueness of types).

(1)
If $Γ ⊩ M : σ$ and $Γ ⊩ M : τ$ , then $σ = τ$ .
(2)
If $Γ ⊩ M : σ$ , $Γ ⊩ N : τ$ , and $M \equiv_{β} N$ , then $σ = τ$ .

Proof.

(1) Induction.
(2) By the hypothesis and Church-Rosser for lambda(->), there is a term $L$ which both $M$ and $N$ reduce to. By Lemma 1.2.7, we have $Γ ⊩ L : σ$ and $Γ ⊩ L : τ$ , so $σ = τ$ by (1). □

Example 1.2.12. There is no way to assign a type to $λ x : x . x$ . If $x$ is of type $τ$ , then in order to apply $x$ to $x$ , it has to be of type $τ \to σ$ for some $σ$ . But $τ \neq τ \to σ$ .

Definition 1.2.13 (Height). The height function is the recursively defined map $h : Π \to ℕ$ that maps a type variable to $0$ , and a function type $σ \to τ$ to $1 + \max (h (σ), h (τ))$ .

We extend the height function from types to $β$ -redexes by taking the height of its $λ$ -abstraction.

Not.: ${(λ x : σ . P^{τ})}^{σ \to τ} R^{σ}$ .

Theorem 1.2.14 (Weak normalisation for lambda(->)). Assuming that:

$Γ ⊩ M : σ$

Then there is a finite reduction path

M : = M_{0} \to_{β} M_{1} \to_{β} M_{2} \to_{β} \dots \to_{β} M_{n}

, where

M_{n}

is in

β

-normal form.

Proof (“Taming the Hydra”). The idea is to apply induction on the complexity of $M$ . Define a function $m : Λ_{Π} \to ℕ \times ℕ$ by

m (M) = {\begin{matrix} (0, 0) & if M is in β -normal form \\ (h (M), r e d e x (M)) & otherwise \end{matrix},

where $h (M)$ is the greatest height of a redex in $M$ , and $r e d e x (M)$ is the number of redexes in $M$ of that height.

We will use induction over $ω \times ω$ to show that if $M$ is typable, then it admits a reduction to $β$ -normal form.

Problem: reductions can copy redexes or create new ones.

Strategy: always reduce the right most redex of maximum height.

We will argue that by following this strategy, any new redexes we generate have to be lower than the height of the redex we picked to reduce.

If $Γ ⊩ M : σ$ and $M$ is already in $β$ -normal form, then claim is trivially true. If $M$ is not in $β$ -normal form, let $Δ$ be the rightmost redex of maximal height $h$ .

By reducing $Δ$ , we may introduce copies of existing redexes, or create new ones. Creation of new redexes of $Δ$ has to happen in one of the following ways:

(1) If $Δ$ is of the form $(λ x : (ρ \to μ) \dots x P^{ρ} \dots) {(λ y : ρ . Q^{μ})}^{P \to μ}$ , then it reduces to $\dots {(λ y : ρ . Q^{μ})}^{ρ \to μ} P^{μ} \dots$ , in which case there is a new redex of height $h (ρ \to μ) < h$ .
(2) We have $Δ = (λ x : τ . (λ y : ρ . R^{μ})) P^{τ}$ occurring in $M$ in the scenario $Δ^{ρ \to μ} Q^{ρ}$ . Say $Δ$ reduces to $λ y : ρ . R_{1}^{μ}$ . Then we create a new redex of height $h (ρ \to μ) < h (τ \to (ρ \to μ)) = h$ .
(3) The last possibility is that $Δ = (λ x : (ρ \to μ) . x) (λ y : ρ . P^{μ})$ , and that it occurs in $M$ as $Δ^{ρ \to μ} Q^{ρ}$ . Reduction then gives the redex ${(λ y : ρ . P^{μ})}^{ρ \to μ} Q^{ρ}$ of height $h (ρ \to μ) < h$ .

Now $Δ$ itself is gone (lowering the count by $1$ ), and we just showed that any newly created redexes have height $< h$ .

If we have $Δ = (λ x : τ . P^{ρ}) Q^{τ}$ and $P$ contains multiple free occurrences of $x$ , then all the redexes in $Q$ are multiplied when performing $β$ -reduction.

However, our choice of $Δ$ ensures that the height of any such redex in $Q$ has height $< h$ , as they occur to the right of $Δ$ in $M$ . It is this always the case that $m (M^{'}) < m (M)$ (in the lexicographic order), so by the induction hypothesis, $M^{'}$ can be reduced to $β$ -normal form (and thus so can $M$ ). □

Theorem 1.2.15 (Strong Normalisation for lambda(->)). Assuming that:

$Γ ⊩ M : σ$

Then there is no infinite reduction sequence

M \to_{β} M_{1} \to_{β} \dots

Proof. See Example Sheet 1. □

1.3 The Curry-Howard Correspondence

Propositions-as-types: idea is to think of $φ$ as the “type of its proofs”.

The properties of the ST $λ$ C match the rules of IPC rather precisely.

First we will show a correspondence between $λ (\to)$ and the implication fragment IPC $(\to)$ of IPC that includes only the $\to$ connective, the axiom scheme, and the $(\to - I)$ and $(\to - E)$ rules. We will later extend this to the whole of IPC by introducing more complex types to $λ (\to)$ .

Start with IPC $(\to)$ and build a ST $λ$ C out of it whose set of type variables $U$ is precisely the set of primitive propositions of the logic.

Clearly, the set $Π$ of types then matches the set of propositions in the logic.

Comment: $λ x : σ . (M x) \to_{η} M$ if $x$ is not free in $M$ .

Proposition 1.3.1 (Curry-Howard for IPC(->)). Assuming that:

$Γ$ is a context for $λ (\to)$
$φ$ a proposition

Then

(1) If $Γ ⊩ M : φ$ , then $| Γ | = {τ \in Π : (x : τ) \in Γ for some x} ⊢_{IPC(\to)} φ$
(2) If $| Γ | ⊢_{IPC(\to)} φ$ , then there is a simply typed $λ$ -term $M \in λ (\to)$ such that ${(x_{ψ} : ψ) | ψ \in Γ} ⊩ M : φ$ .

Proof.

(1) We induct over the derivation of $Γ ⊩ M : φ$ .
If $x$ is a variable not occurring in $Γ^{'}$ and the derivation is of the form $Γ^{'}, x : φ ⊩ x : φ$ , then we’re supposed to prove that $| Γ^{'}, x : φ | ⊢ φ$ . But that follows from $φ ⊢ φ$ as $| Γ^{'}, x : φ | = | Γ^{'} | \cup {φ}$ .

If the derivation has $M$ of the form $λ x : σ . N$ and $φ = σ \to τ$ , then we must have $Γ, x : σ ⊩ N : τ$ . By the induction hypothesis, we have that $| Γ, x : σ | ⊢ τ$ , i.e. $| Γ |, σ ⊢ τ$ . But then $| Γ | ⊢ σ \to τ$ by ( $\to$ -I).

If the derivation has the form $Γ ⊩ (P Q) : φ$ , then we must have $Γ ⊩ P : (σ \to φ)$ and $Γ ⊩ Q : σ$ . By the induction hypothesis, we have that $| Γ | ⊢ σ \to φ$ and $| Γ | ⊢ σ$ , so $| Γ | ⊢ φ$ by ( $\to$ -E).

(2) Again, we induct over the derivation of

Γ ⊢ φ

. Write

Δ = {(x_{ψ} : ψ) | ψ \in Γ}

. Then we only have a few ways to construct a proof at a given stage. Say the derivation is of the form

Γ, φ ⊢ φ

. If

φ \in Γ

, then clearly

Δ ⊩ x_{φ} : φ

, and if

φ \notin Γ

then

Δ, x_{φ} : φ ⊩ x_{φ} : φ

Suppose the derivation is at a stage of the form

\frac{Γ ⊢ φ \to ψ Γ ⊢ φ}{Γ ⊢ ψ} .

Then by the induction hypothesis, there are $λ$ -terms $M$ and $N$ such that $Δ ⊩ M : (φ \to ψ)$ and $Δ ⊩ N : φ$ , from which $Δ ⊩ (M N) : φ$ .

Finally, if the stage is given by

\frac{Γ, φ ⊢ ψ}{Γ ⊢ φ \to ψ},

then we have two sub-cases:

If $φ \in Γ$ , then the induction hypothesis gives $Δ ⊩ M : ψ$ for some term $M$ . By weakening, we have $Δ, x : φ ⊩ M : ψ$ , where $x$ does not occur in $Δ$ . But then $Δ ⊩ (λ x : φ . M) : (φ \to ψ)$ as needed.
If $φ \notin Γ$ , then the induction hypothesis gives $Δ, x_{φ} : φ ⊩ M : ψ$ for some $M$ , thus $Δ ⊩ (λ x_{φ} : φ . M) : (φ \to ψ)$ as needed. □

Example 1.3.2. Let $φ, ψ$ be primitive propositions. The $λ$ -term

λ f : (φ \to ψ) \to φ . λ : φ \to ψ . \overset{ψ}{\overset{︷}{g (\underset{φ}{\underset{⏟}{f g}})}}

has type $((φ \to ψ) \to φ) \to ((φ \to ψ) \to ψ)$ , and therefore encodes a proof of that proposition in IPC( $\to$ ).

$g : φ \to ψ$ , $f : (φ \to ψ) \to φ$ .

$g : [φ \to ψ] f : [(φ \to ψ) \to φ]$	(toE)

$f g : φ g : [φ \to ψ]$	(toE)

$g (f g) : ψ$	(toI, φ→ψ)

$λ g . g (f g) : (φ \to ψ) \to ψ$	(toI, (φ→ψ) →φ)

$λ f . λ g . g (f g) : ((φ \to ψ) \to φ) \to ((φ \to ψ) \to ψ)$

Definition 1.3.3 (Full STlambdaC). The types of the full simply typed $λ$ -calculus are generated by the following grammar:

Π : = U | Π \to Π | Π \times Π | Π + Π | 0 | 1,

where $U$ is a set of type variables (usually countable).

Its terms are given by $Λ_{Π}$ given by:

Λ_{Π} : = V | λ V : Π . Λ_{Π} | Λ_{Π} Λ_{Π} | Π_{1} (Λ_{Π}) | Π_{2} (Λ_{Π}) | ι_{1} (Λ_{Π}) | ι_{2} (Λ_{Π}) | case (Λ_{Π}; V . Λ_{Π}; V . Λ_{Π}) | * |!_{Π} Λ_{Π},

where $V$ is an infinite set of variables, and $*$ is a constant.

We have new typing rules:

$\frac{Γ ⊩ M : ψ \times φ}{Γ ⊩ π_{1} (M) : ψ}$
$\frac{Γ ⊩ M : ψ \times φ}{Γ ⊩ π_{2} (M) : φ}$
$\frac{Γ ⊩ M : ψ}{Γ ⊩ ι_{1} (M) : ψ + φ}$
$\frac{Γ ⊩ N : φ}{Γ ⊩ ι_{2} (N) : ψ + φ}$
$\frac{Γ ⊩ M : ψ Γ ⊩ N : φ}{Γ ⊩ ⟨ M, N ⟩ : φ \times ψ}$
$\frac{Γ ⊩ L : ψ + φ Γ, x : ψ ⊩ M : ρ Γ, y : φ ⊩ N : ρ}{Γ ⊩ case (L; x^{ψ} . M; x^{φ} . N)}$
$\frac{}{Γ ⊩ * : 1}$
$\frac{Γ ⊩ M : 0}{Γ ⊩!_{φ} M : φ}$ for each $φ \in Π$

They come with new reduction rules:

Projections: $π_{1} ⟨ M, N ⟩ \to_{β} M$ and $π_{2} ⟨ M, N ⟩ \to_{β} N$
Pairs: $⟨ π_{1} M, π_{2} M ⟩ \to_{η} M$
Definition by cases: $case (ι_{1} (M); x K; y . L) \to_{β} K [x : = M]$ and $case (ι_{2} (M); x . K; y . L) \to_{β} L [y : = M]$
Unit: If $Γ ⊩ M : 1$ , then $M \to_{η} *$

When setting up Curry-Howard with these new types, we let:

$0 ↭ ⊥$
$\times ↭ \land$
$+ ↭ \lor$
$\to ↭ \to$

Example 1.3.4. Consider the following proof of $(φ \land χ) \to (ψ \to φ)$ :

$\frac{[φ \land χ]}{φ} [ψ]$	()

$ψ \to φ$	()

$(φ \land χ) \to (ψ \to φ)$

We decorate this proof by turning the assumptions into variables and following the Curry-Howard correspondence:

$\frac{[φ \land χ] : p}{φ : π_{1} (p)} [ψ] : b$	()

$ψ \to φ : λ b : ψ . π_{1} (p)$	()

$(φ \land χ) \to (ψ \to φ)$

ST $λ$ C	IPC

(primitive) types	(primitive) propositions
variable	hypothesis
ST $λ$ -term	proof
type constructor	logical connective
term inhabitation	provability
term reduction	proof normalisation

1.4 Semantics for IPC

Definition 1.4.1 (Lattice). A lattice is a set $L$ equipped with binary commutative and associative operations $\land$ and $\lor$ that satisfy the absorption laws:

a \lor (a \land b) = a; a \land (a \lor b) = a,

for all $a, b \in L$ .

A lattice is:

Distributive if $a \land (b \lor c) = (a \land b) \lor (a \land c)$ for all $a, b, c \in L$ .
Bounded if there are elements $⊥, ⊤ \in L$ such that $a \lor ⊥ = a$ and $a \land ⊤ = a$ .
Complemented if it is bounded and for every $a \in L$ there is $a^{*} \in L$ such that $a \land a^{*} = ⊥$ and $a \lor a^{*} = ⊤$ .

A Boolean algebra is a complemented distributive lattice.

Note that $\land$ and $\lor$ are idempotent in any lattice. Moreover, we can define an ordering on $L$ by setting $a \leq b$ if $a \land b = a$ .

Example 1.4.2.

(1) For every set $I$ , the power set $P (I)$ with $\land : = \cap$ and $\lor : = \cup$ is the prototypical Boolean algebra. More generally, the clopen subsets of a topological space form a Boolean algebra. Interestingly: every Boolean algebra corresponds to a Boolean algebra constructed in this way.
(2) The set of finite and cofinite subsets of $ℤ$ is a Boolean algebra.
(3) The set of Zariski-closed subsets of the affine variety $ℂ^{n}$ is a distributive lattice but not a Boolean algebra.

Proposition 1.4.3. Assuming that:

$L$ is a bounded lattice
$\leq$ is the order induced by the operations in $L$ ( $a \leq b$ if $a \land b = a$ )

Then

\leq

is a partial order with least element

⊥

, greatest element

⊤

, and for any

a, b \in L

, we have

a \land b = \inf {a, b}

and

a \land b = \sup {a, b}

. Conversely, every partial order with all finite infs and sups is a bounded lattice.

Proof. Exercise. □

Classically, we say that $Γ ⊨ t$ if for every valuation $v : L \to {0, 1}$ with $v (p) = 1$ for all $p \in Γ$ we have $v (t) = 1$ .

We might want to replace ${0, 1}$ with some other Boolean algebra to get a semantics for IPC, with an accompanying Completeness Theorem. But Boolean algebras believe in the Law of Excluded Middle!

Definition 1.4.4 (Heyting algebra). A Heyting algebra is a bounded lattice equipped with a binary operation $\Rightarrow : H \times H \to H$ such that

a \land b \leq c ⟺ a \leq (b \Rightarrow c)

for all $a, b, c \in L$ .

A morphism of Heyting algebras is a function that preserves all finite meets, finite joins, and $\Rightarrow$ .

Example 1.4.5.

(1) Every Boolean algebra is a Heyting algebra: define $a \Rightarrow b : = a^{*} \lor b$ , where $a^{*}$ is the complement of $a$ . Note that we must have $a^{*} = (a \Rightarrow ⊥)$ .
(2) Every topology on a set $X$ is a Heyting algebra, where
$(U \Rightarrow V) : = int ((X ∖ U) \cup V) .$
(3) A finite distributive lattice has to be a Heyting algebra (see Example Sheet 2).

Definition 1.4.6 (Valuation in Heyting algebras). Let $H$ be a Heyting algebra and $L$ be a propositional language with a set $P$ of primitive propositions. An $H$ -valuation is a function $v : P \to H$ , extended to the whole of $L$ recursively by setting:

$v (⊥) = ⊥$ ,
$v (A \land B) = v (A) \land v (B)$ ,
$v (A \lor B) = v (A) \lor v (B)$ ,
$v (A \to B) = v (A) \Rightarrow v (B)$ .

A proposition $A$ is $H$ -valid if $v (A) = ⊤$ for all $H$ -valuations $v$ , and is an $H$ -consequence of a (finite) set of propositions $Γ$ if $v (\land Γ) \leq v (A)$ for all $H$ -valuations $v$ (written $Γ ⊨_{H} A$ ).

Lemma 1.4.7 (Soundness of Heyting semantics). Assuming that:

$H$ is a Heyting algebra
$v : L \to H$ is a valuation

Then

Γ ⊢_{IPC} A

implies

Γ ⊨_{H} A

Proof. By induction over the structure of the proof $Γ ⊢ A$ .

(Ax) As $v ((\land Γ) \land A) = v (\land) \land v (A) \leq v (A)$ for any $Γ$ and $A$ .
( $\land$ -I) $A = B \land C$ and we have derivations $Γ_{1} ⊢ B$ , $Γ_{2} ⊢ C$ , with $Γ_{1}, Γ_{2} \subseteq Γ$ . By the induction hypothesis, we have $v (\land Γ) \leq v (\land Γ_{1}) \cap v (\land Γ_{2}) \leq v (B) \land v (C) = v (B \land C) = v (A)$ , i.e. $Γ ⊨_{H} A$ .
( $\to$ -I) $A = B \to C$ and so we must have $Γ \cup {B} ⊢ C$ . By induction hypothesis, we have $v (\land Γ) \land v (B) = v (\land γ \land B) \leq v (C)$ . By the definition of $\Rightarrow$ , this implies $v (\land Γ) \leq [v (B) \Rightarrow v (C)] = v (B \to C) = v (A)$ , i.e. $Γ ⊨_{H} A$ .
( $\lor$ -I) $A = B \lor C$ and without loss of generality we have a derivation $Γ ⊢ B$ . By the induction hypothesis we have $v (\land Γ) \leq v (B)$ , but $v (B \lor C) = v (B) \lor v (C)$ , and hence $v (B) \leq v (B \lor C) = v (A)$ .
( $\land$ -E) By the induction hypothesis, we have $v (\land Γ) \leq v (B \land C) = v (B) \land v (C) \leq v (B), v (B)$ .
( $\to$ -E) We know that $v (A \to B) = (v (A) \Rightarrow v (B))$ . From $v (A \to B) \leq v (A) \Rightarrow v (B)$ , we derive $v (A) \land v (A \to B) \leq v (B)$ by definition of $\Rightarrow$ . So if $v (\land Γ) \leq v (A \to B)$ and $v (\land Γ) \leq v (A)$ , then $v (\land Γ) \leq v (B)$ , as needed.
( $\lor$ -E) By induction hypothesis: $v (A \lor \land Γ) \leq v (C)$ , $v (B \lor \land Γ) \leq v (C)$ and $v (\land Γ) \leq v (A \lor B) = v (A) \lor v (B)$ . This last fact means that $v (\land Γ) \land (v (A) \lor v (B)) = v (\land Γ)$ . Now this is the same as $(v (\land Γ) \land v (A)) \lor (v (\land Γ) \land v (B))$ as Heyting algebras are distributive lattices (see Example Sheet 2), and this is $\leq v (C)$ by the first two inequalities of this paragraph.
( $⊥$ -E) If $v (\land Γ) \leq v (⊥) = ⊥$ , then $v (\land Γ) = ⊥$ , in which case $v (\land Γ) \leq v (A)$ for any $A$ by minimality of $⊥$ in $H$ . □

Example 1.4.8. The Law of Excluded Middle is not intuitionistically valid. Let $p$ be a primitive proposition and consider the Heyting algebra given by the topology ${\emptyset, {1}, {1, 2}}$ on ${1, 2}$ .

We can define a valuation $v$ with $v (p) = {1}$ , in which case $v (\neg p) = \neg {1} = int (X ∖ {1}) = \emptyset$ .

So $v (p \lor \neg p) = {1} \lor \emptyset = {1} \neq ⊤$ . Thus Soundness of Heyting semantics implies that $⁄ ⊢_{IPC} p \lor \neg p$ .

Example 1.4.9. Peirce’s Law $((p \to q) \to p) \to p$ is not intuitionistically valid.

Take the valuation on the usual topology of $ℝ^{2}$ that maps $p$ to $ℝ^{2} ∖ {(0, 0)}$ and $q$ to $\emptyset$ .

Classical completeness: $Γ ⊢_{CPC} A$ if and only if $Γ ⊨_{2} A$ .

Intuitionistic completeness: no single finite replacement for $2$ .

Definition (Lindenbaum-Tarski algebra). Let $Q$ be a logical doctrine (CPC, IPC, etc), $L$ be a propositional language, and $T$ be an $L$ -theory. The Lindenbaum-Tarski algebra $F^{Q} (T)$ is built in the following way:

The underlying set of $F^{Q} (T)$ is the set of equivalence classes $[φ]$ of propositions $φ$ , where $φ \sim ψ$ when $T, φ ⊢_{Q} ψ$ and $T, ψ ⊢_{Q} φ$ ;
If $⋈$ is a logical connective in the fragment $Q$ , we set $[φ] ⋈ [ψ] : = [φ ⋈ ψ]$ (should check well-defined: exercise).

We’ll be interested in the case $Q = CPC$ , $Q = IPC$ , and $Q = IPC ∖ {\to}$ .

Proposition 1.4.10. The Lindenbaum-Tarski algebra of any theory in $IPC ∖ {\to}$ is a distributive lattice.

Proof. Clearly, $\land$ and $\lor$ inherit associativity and commutativity, so in order for $F^{IPC ∖ {\to}} (T)$ to be a lattice we need only to check the absorption laws:

\begin{array}{l} [φ] \lor [φ \land ψ] & = [φ] & (α) \\ [φ] \land [φ \lor ψ] & = [φ] & (β) \end{array}

Equation ( $α$ ) is true since $T, φ ⊢_{I P C ∖ {\to}} φ \lor (φ \land ψ)$ by ( $\lor$ -I), and also $T, φ \lor (φ \land ψ) ⊢_{IPC ∖ {\to}} φ$ by ( $\lor$ -E). Equation ( $β$ ) is similar.

Now, for distributivity: $T, φ \land (ψ \lor χ) ⊢ (φ \land ψ) \lor (φ \land χ)$ by ( $\land$ -E) followed by ( $\lor$ -E):

$φ \land (ψ \lor χ)$	( $\land$ -E)

$φ ψ \lor χ$	( $\lor$ -E)

$(φ \land ψ) \lor (φ \land χ)$

Conversely, $T, ((φ \land ψ) \lor (φ \land χ)) ⊢ φ \land (ψ \lor χ)$ by ( $\lor$ -E) followed by ( $\land$ -I). □

Lemma 1.4.11. The Lindenbaum-Tarski algebra of any theory relative to IPC is a Heyting algebra.

Proof. We already saw that $F^{IPC} (T)$ is a distributive lattice, so it remains to show that $[φ] \Rightarrow [ψ] : = [φ \to ψ]$ gives a Heyting implication, and that $F^{IPC} (T)$ is bounded.

Suppose that $[φ \land [ψ] \leq [χ]$ , i.e. $τ, φ \land ψ ⊢_{IPC} χ$ . We want to show that $[φ] \leq [ψ \to χ]$ , i.e. $τ, φ ⊢ (ψ \to χ)$ . But that is clear:

$φ [ψ]$

$φ \land ψ$	(hyp)

$χ$	( $\to$ -I, $ψ$ )

$ψ \to χ$

Conversely, if $τ, φ ⊢ (ψ \to χ)$ , then we can prove $τ, φ \land ψ ⊢ χ$ :

$φ \land ψ$	( $\land$ -E)

$φ ψ$	(hyp)

$ψ \to χ ψ$	( $\to$ -E)

$χ$

So defining $[φ] \Rightarrow [ψ] : = [φ \to ψ]$ provides a Heyting $\Rightarrow$ .

The bottom element of $F^{IPC} (T)$ is just $[⊥]$ : if $[φ]$ is any element, then $T, ⊥ ⊢_{IPC} φ$ by $⊥$ -E.

The top element is $⊤ : = [⊥ \to ⊥$ : if $φ$ is any proposition, then $[φ] \leq [⊥ \to ⊥]$ via

$φ [⊥]$	( $⊥$ -E)

$⊥$

$⊥ \to ⊥$

□

Theorem 1.4.12 (Completeness of the Heyting semantics). A proposition is provable in IPC if and only if it is $H$ -valid for every Heyting algebra $H$ .

Proof. One direction is easy: if $⊢_{IPC} φ$ , then there is a derivation in IPC, thus $⊤ \leq v (φ)$ for any Heyting algebra $H$ and valuation $v$ , by Soundness of Heyting semantics. But then $v (φ) = ⊤$ and $φ$ is $H$ -valid.

For the other direction, consider the Lindenbaum-Tarski algebra $F (L)$ of the empty theory relative to IPC, which is a Heyting algebra by Lemma 1.4.11. We can define a valuation $v$ by extending $P \to F (L)$ , $p \mapsto [p]$ to all propositions.

As $v$ is a valuation, it follows by induction (and the construction of $F (L)$ ) that $v (φ) = [φ]$ for all propositions.

Now $φ$ is valid in every Heyting algebra, and so is valid in $F (L)$ in particular. So $v (φ) = ⊤ = [φ]$ , hence $⊤ \to ⊤ ⊢_{IPC} φ$ , hence $⊢_{IPC} φ$ . □

Given a poset $S$ , we can construct sets $a ↑ : = {s \in S : a \leq s}$ called principal up-sets.

Recall that $U \subseteq S$ is a terminal segment if $a ↑ \subseteq U$ for each $a \in U$ .

Proposition 1.4.13. If $S$ is a poset, then the set $T (S) = {U \subseteq S : U is a terminal segment of S}$ can be made into a Heyting algebra.

Proof. Order the terminal segments by $\subseteq$ . Meets and joins are $\cap$ and $\cup$ , so we just need to define $\Rightarrow$ . If $U, V \in T (S)$ , define $(U \Rightarrow V) : = {s \in S : (s ↑) \cap U \subseteq V}$ .

If $U, V, W \in T (S)$ , we have

W \subseteq (U \Rightarrow V) ⟺ (w ↑) \cap U \subseteq V \forall w \in W,

which happens if for every $w \in W$ and $u \in U$ we have $w \leq u ⟹ u \in V$ . But $W$ is a terminal segment, so this is the same as saying that $W \cap U \subseteq V$ . □

Definition 1.4.14 (Kripke model). Let $P$ be a set of primitive propositions. A Kripke model is a tuple $(S, \leq, ⊩)$ where $(S, \leq)$ is a poset (whose elements are called “worlds” or “states”, and whose ordering is called the “accessibility relation”) and $⊩ \subseteq S \times P$ is a binary relation (“forcing”) satisfying the persistence property: if $p \in P$ is such that $s ⊩ p$ and $s \leq s^{'}$ , then $s^{'} ⊩ p$ .

Every valuation $v$ on $T (S)$ induces a Kripke model by setting $s ⊩ p$ is $s \in v (p)$ .

Definition 1.4.15 (Forcing relation). Let $(S, \leq, ⊩)$ be a Kripke model for a propositional language. We define the extended forcing relation inductively as follows:

There is no $s \in S$ with $s ⊩ ⊥$ ;
$s ⊩ φ \land ψ$ if and only if $s ⊩ φ$ and $s ⊩ ψ$ ;
$s ⊩ φ \lor ψ$ if and only if $s ⊩ φ$ or $s ⊩ ψ$ ;
$s ⊩ (φ \to ψ)$ if and only if $s^{'} ⊩ φ$ implies $s^{'} ⊩ ψ$ for every $s^{'} \geq s$ .

It is easy to check that the persistence property extends to arbitrary propositions.

Moreover:

$s ⊩ \neg φ$ if and only if $s^{'} ⁄ ⊩ φ$ for all $s^{'} \geq s$ .
$s ⊩ \neg \neg φ$ if and only if for every $s^{'} \geq s$ , there exists $s^{″} \geq s^{'}$ with $s^{″} ⊩ φ$ .

Notation. $S ⊩ φ$ for $φ$ a proposition if all worlds in $S$ force $φ$ .

Example 1.4.16. Consider the following Kripke models:

In (1), we have $s ⁄ ⊩ \neg p$ , since $s^{'} \geq s$ and $s^{'} ⊩ p$ . We also know that $s ⁄ ⊩ p$ , thus $s ⁄ ⊩ p \lor \neg p$ .

It is also the case that $s ⊩ \neg \neg p$ , yet $s ⁄ ⊩ p$ , so $s ⁄ ⊩ (\neg \neg p \to p)$ either.

In (2), $s ⁄ ⊩ \neg \neg p$ since $s^{'} \geq s$ can’t access a world that forces $p$ . Also $s ⁄ ⊩ \neg p$ either, as $s^{″} \geq s$ forces $p$ . So $s ⁄ ⊩ \neg \neg p \lor \neg p$ .

In (3), $s ⁄ ⊩ (p \to q) \to (\neg p \lor q)$ . All worlds force $p \to q$ , and $s ⁄ ⊩ q$ . So to check the claim we just need to verify that $s ⁄ ⊩ \neg p$ . But that is the case, as $s^{'} \geq s$ and $s^{'} ⊩ p$ .

Definition 1.4.17 (Filter). A filter $F$ on a lattice $L$ is a subset of $L$ with the following properties:

$F \neq \emptyset$
$F$ is a terminal segment of $L$ (i.e., if $f \leq x$ and $f \in F$ , then $x \in F$ )
$F$ is closed under finite meets

Example 1.4.18.

(1) Given an element $j \in I$ of a set $I$ , then the family $F_{j}$ of all subsets of $I$ containing $j$ is a filter on $P (I)$ . Such a filter is called a principal filter.
(2) The family of all cofinite subsets of $I$ is a filter on $P (I)$ , the Fréchet filter.
Exercise: a maximal proper filter (known as an ultra filter) is not principal if and only if it contains the Fréchet filter.
(3) The family of all subsets of $[0, 1]$ with Lebesgue measure $1$ is a filter.

A filter is proper if $F \neq L$ .

A filter $F$ on a Heyting algebra is prime if it is proper and satisfies: whenever $(x \lor y) \in F$ , we can conclude that $x \in F$ or $y \in F$ .

If $F$ is a proper filter and $x \notin F$ , then there is a prime filter extending $F$ that still doesn’t contain $x$ (by Zorn’s Lemma).

Lemma 1.4.19. Assuming that:

$H$ a Heyting algebra
$v$ a $H$ -valuation

Then there is a Kripke model

(S, \leq, ⊩)

such that

v ⊨_{H} φ

if and only if

S ⊩ φ

, for every proposition

φ

Proof (sketch). Let $S$ be the set of all prime filters of $H$ , ordered by inclusion. We write $F ⊩ p$ if and only if $v (p) \in F$ for primitive propositions $p$ .

We prove by induction that $F ⊩ φ$ if and only if $v (φ) \in F$ for arbitrary propositions.

For the implication case, say that $F ⊩ (ψ \to ψ^{'})$ and $v (ψ \to ψ^{'}) = [v (ψ) \Rightarrow v (ψ^{'})] \notin F$ . Let $G^{'}$ be the least filter containing $F$ and $v (ψ)$ . Then

G^{'} = {b : (\exists f \in F) (f \land v (ψ) \leq b)} .

Note that $v (ψ^{'}) \notin G^{'}$ , or else $f \land v (ψ) \leq v (ψ^{'})$ for some $f \in F$ , whence $f \leq v (ψ \to ψ^{'})$ and so $v (ψ \to ψ^{'}) \in F$ (as $F$ is a terminal segment).

In particular, $G^{'}$ is proper. So let $G$ be a prime filter extending $G^{'}$ that does not contain $v (ψ^{'})$ (exists by Zorn’s lemma).

By the induction hypothesis, $G ⊩ ψ$ , and since $F ⊩ (ψ \to ψ^{'})$ and $G^{'}$ (this $G$ ) contains $F$ , we have that $G ⊩ ψ^{'}$ . But then $v (ψ^{'}) \in G$ , contradiction.

This settles that $F ⊩ (ψ \to ψ^{'})$ implies $v (ψ \to ψ^{'}) \in F$ .

Conversely, say that $v (ψ \to ψ^{'}) \in F \subseteq G ⊩ ψ$ . By the induction hypothesis, $v (ψ) \in G$ , and so $v (ψ) \Rightarrow v (ψ) \in G$ (as $F \subseteq G$ ). But then $v (ψ^{'}) \geq v (ψ) \land (v (ψ) \Rightarrow v (ψ^{'})) \in G$ , as $G$ is a filter.

So the induction hypothesis gives $G ⊩ ψ^{'}$ , as needed.

The cases for the other connectives are easy ( $\lor$ needs primality). So $(S, \leq, ⊩)$ is a Kripke model. Want to show that $v ⊨_{H} φ$ if and only if $S ⊩ φ$ , for each $φ$ .

Conversely, say $S ⊩ φ$ , but $v ⁄ ⊨_{H} φ$ . Since $v (φ) \neq ⊤$ , there must be a proper filter that does not contain it. We can extend it to a prime filter $G$ that does not contain it, but then $G ⁄ ⊩ φ$ , contradiction. □

Theorem 1.4.20 (Completeness of the Kripke semantics). Assuming that:

$φ$ a proposition

Then

Γ ⊢_{IPC} φ

if and only if for all Kripke models

(S, \leq, ⊩)

, the condition

S ⊩ Γ

implies

S ⊩ φ

Proof. Soundness: induction over the complexity of $φ$ .

Adequacy: Say $Γ ⁄ ⊢_{IPC} φ$ . Then $v ⊨_{H} Γ$ but $v ⁄ ⊨_{H} φ$ for some Heyting algebra $H$ and $H$ -valuation $v$ (Theorem 1.4.12). But then Lemma 1.4.19 applied to $H$ and $v$ provides a Kripke model $(S, \leq, ⊩)$ such that $S ⊩ Γ$ , but $S ⁄ ⊩ φ$ , contradicting the hypothesis on every Kripke model. □

1.5 Negative translations

Definition 1.5.1 (Double-negation translation). We recursively define the $\neg \neg$ -translation $φ^{N}$ of a proposition $φ$ in the following way:

If $p$ is a primitive proposition, then $p^{N} : = \neg \neg p$ ;
${(φ \land ψ)}^{N} : = φ^{N} \land ψ^{N}$
${(φ \to ψ)}^{N} : = φ^{N} \to ψ^{N}$
${(φ \lor ψ)}^{N} : = \neg (\neg φ^{N} \land \neg ψ^{N})$
${(\neg φ)}^{N} : = \neg φ^{N}$

Lemma 1.5.2. Assuming that:

$H$ a Heyting algebra

Then the map

\neg \neg : H \to H

preserves

\land

and

\Rightarrow

Proof. Example Sheet 2. □

Lemma 1.5.3 (Regularisation). Assuming that:

$H$ a Heyting algebra

Then

(1) The subset $H_{\neg \neg} : = {x \in H : \neg \neg x = x}$ is a Boolean algebra;
(2) For every Heyting homomorphism $g : H \to B$ into a Boolean algebra, there is a unique map of Boolean algebras $g_{\neg \neg} : H_{\neg \neg} \to B$ such that $g (x) = g_{\neg \neg} (\neg \neg x)$ for all $x \in H$ .

Proof.

(1) Give $H_{\neg \neg} : = {x \in H : \neg \neg x = x}$ the inherited order, so that $\land$ , $\Rightarrow$ , $⊥$ and $⊤$ (which are preserved by $\neg \neg$ ) remain the same. We just need to define disjunctions in $H_{\neg \neg}$ properly.
Define $a \lor_{\neg \neg} b : = \neg \neg (a \lor b)$ in $H$ . It is easy to show that this gives $\sup {a, b}$ in $H_{\neg \neg}$ (as $\neg \neg$ preserves order), so $H_{\neg \neg}$ is a Heyting algebra.

As every element of $H_{\neg \neg}$ is regular (i.e. $\neg \neg x = x$ ), it is a Boolean algebra (see Example Sheet 2).
(2) Given a Heyting homomorphism $g : H \to B$ , where $B$ is a Boolean algebra, define $g_{\neg \neg} : H \to B$ as $g_{H_{\neg \neg}}$ . It clearly preserves $⊥, ⊤, \land, \Rightarrow$ , as those operations in $H_{\neg \neg}$ are inherited from $H$ .
But we also have
$\begin{array}{l} g_{\neg \neg} (a \lor_{\neg \neg} b) & = g |_{H_{\neg \neg}} (\neg \neg (a \lor b)) \\ = \neg \neg (g (a) \lor g (b)) \\ = g (a) \lor g (b) & B is Boolean \\ = g_{\neg \neg} (a) \lor g_{\neg \neg} (b) \end{array}$
Thus $g_{\neg \neg}$ is a morphism of Boolean algebras. Note that any $x \in H$ provides an element $\neg \neg x \in H_{\neg \neg}$ , since $\neg \neg \neg \neg x = \neg \neg x$ in $H$ . Additionally,
$\begin{array}{l} g_{\neg \neg} (\neg \neg x) & = g (\neg \neg x) \\ = \neg \neg g (x) \\ = g (x) \end{array}$
for all $x \in H$ (as $g (x)$ is in a Boolean algebra).

Now, if $h : H_{\neg \neg} \to B$ is a morphism of Boolean algebras with $g (x) = h (\neg \neg x)$ for all $x \in H$ , then $h (a) = h (\neg \neg a) = g (a) = g_{\neg \neg} (a)$ for all $a \in H$ . So $g_{\neg \neg}$ is unique with this property. □

In particular, if $S$ is a set, then $F^{Heyt} {(S)}_{\neg \neg} ≅ F^{Bool} (S)$ .

Theorem 1.5.4 (Glivenko’s Theorem). Assuming that:

$φ$ and $ψ$ are propositions

Then

⊢_{CPC} φ \to ψ

if and only if

⊢_{IPC} \neg \neg φ \to \neg \neg ψ

Proof.

$\Rightarrow$ If $⊢_{CPC} φ \to ψ$ , then $⊤ \leq φ \to ψ$ in $F^{Bool} (L) = F^{Heyt} {(L)}_{\neg \neg}$ . As the inclusion $i : F^{Heyt} {(L)}_{\neg \neg} \to F^{Heyt} (L)$ strictly preserves $\leq$ and $\to$ , it follows that $\begin{array}{l} i (⊤) & \leq i (φ \to ψ) \\ = φ \to ψ \\ = \neg \neg (φ \to ψ) & as φ \to ψ \in F^{Heyt} {(L)}_{\neg \neg} \\ = \neg \neg φ \to \neg \neg ψ \end{array}$
in $F^{Heyt} (L)$ , so $⊢_{IPC} \neg \neg φ \to \neg \neg ψ$ .
$\Leftarrow$ Obvious. □

Corollary 1.5.5. Assuming that:

$φ$ a proposition

Then

⊢_{CPC} φ

if and only if

⊢_{IPC} φ^{N}

Proof. Induction over the complexity of formulae. □

Corollary 1.5.6. CPC is inconsistent if and only if IPC is inconsistent.

Proof.

$\Rightarrow$ If CPC is inconsistent, then there is $φ$ such that $⊢_{CPC} φ$ and $⊢_{IPC} \neg φ$ . But then $⊢_{IPC} \neg \neg φ$ and $⊢_{IPC} \neg φ$ , so $⊢_{IPC} ⊥$ .
$\Leftarrow$ Obvious. □

2 Computability

“If a ‘religion’ is defined to be a system of ideas that contains improvable statements, then Gödel taught us that mathematics is not only a religion; it is the only religion that can prove itself to be on.” – John Barrow

2.1 Recursive functions and $λ$ -computability

Definition 2.1.1 (Partial recursive function). The class of recursive functions is the smallest class of partial functions of the form $ℕ^{k} \to ℕ$ that contains the basic functions:

Projections: $Π_{i}^{m} : (n_{1}, \dots, n_{m}) \mapsto n_{i}$ ;
Successor: $S^{+} : n \mapsto n + 1$ ;
Zero: $z : n \mapsto 0$

and is closed under:

Compositions: if $g : ℕ^{k} \to ℕ$ is partial recursive and so are $h_{1}, \dots, h_{k} : ℕ^{m} \to ℕ$ , then the function $f : ℕ^{m} \to ℕ$ given by $f (\bar{n}) = g (h_{1} (\bar{n}), \dots, h_{k} (\bar{n}))$ is partial recursive.
Primitive recursion: Given partial recursive functions $g : ℕ^{m} \to ℕ$ and $h : ℕ^{m + 2} \to ℕ$ , the function $f : ℕ^{m + 1} \to ℕ$ defined by
${\begin{matrix} f (0, \bar{n}) : = g (\bar{n}) \\ f (k + 1, \bar{n}) : = h (f (k, \bar{n}), k, \bar{n}) \end{matrix}$
Minimisation: Suppose $g : ℕ^{m + 1} \to ℕ$ is partial recursive. Then the function $f : ℕ^{m} \to ℕ$ that maps $\bar{n}$ to the least $n$ such that $g (n, \bar{n}) = 0$ (if it exists) is partial recursive.

Notation: $f (\bar{n}) = μ n . g (n, \bar{n}) = 0$ .

The class of functions produced by the same conditions but excluding minimisation is called the class of primitive recursive functions.

A partial recursive function that is defined everywhere is called a total recursive function.

The terms of the untyped $λ$ -calculus $Λ$ are given by the grammar

Λ : = V | λ V . Λ | Λ Λ,

where $V$ is a (countable) set of variables.

The notions we previously discussed ( $α$ -equality, $β$ -reduction, $η$ -reduction, etc) apply tit for tat.

Example 2.1.2. Let $ω : = λ x . x x$ and $Ω : = ω ω$ . Then $Ω = (λ x . x x) ω \to_{β} ω ω = Ω$ . This shows that we can have an infinite reduction chain of $λ$ -terms.

Question: If $M ↠_{β} N$ , $M ↠_{β} N^{'}$ , do we have $N ↠_{β} M^{'}$ and $N^{'} ↠_{β} M^{'}$ for some $M^{'}$ ?

Idea: “Simultaneously reduce” all the redexes in $M$ to get a term $M^{*}$ . This might have new redexes, so we can iterate the process to get terms $M^{2 *}, M^{3 *}, \dots$ .

$M$ should reduce to $M^{*}$ , so we have $M ↠_{β} M^{*} ↠_{β} M^{2 *}, \dots$ . We’ll see that if $M$ reduces to $N$ in $k$ steps, then $N ↠_{β} M^{k *}$ .

Using this, we will show (assuming $s \geq r$ ):

To get there, we want to build $M^{*}$ with two properties:

(1) $M ↠_{β} M^{*}$ ;
(2) If $M ↠_{β} N$ , then $N ↠_{β} M^{*}$ .

Definition 2.1.3 (Takahashi Translation). The Takahashi translation $M^{*}$ of a $λ$ -term $M$ is recursively defined as follows:

(1)
$x^{*} : = x$ , for $x$ a variable;
(2)
If $M = (λ x . P) Q$ is a redex, then $M^{*} : = P^{*} [x : = Q^{*}]$ ;
(3)
If $M = P Q$ is a $λ$ -application, then $M^{*} : = P^{*} Q^{*}$ ;
(4)
If $M = λ x . P$ is a $λ$ -abstraction, then $M^{*} : = λ x . P^{*}$ .

These rules are numbered by order of precedence, in case of ambiguity. We also define $M^{0 *} : = M$ and $M^{(n + 1) *} : = {(M^{n *})}^{*}$ .

Note that $M^{*}$ is not necessarily in $β$ -normal form, for example if $M = (λ x . x y) (λ y . y)$ , then

M^{*} = {(x y)}^{*} [x : = {(λ y . y)}^{*}] = (x y) [x : = λ y . y] = (λ y . y) y .

Lemma 2.1.4. Assuming that:

$M$ and $N$ are $λ$ -terms

Then

(1)
$FV (M^{*}) \subseteq FV (M)$ ;
(2)
$M ↠_{β} M^{*}$ ;
(3)
If $M \to_{β} N$ , then $N ↠_{β} M^{*}$ .

Proof. Induction over the structure of $λ$ -terms. □

Lemma 2.1.5. Takahashi translation preserves $β$ -contraction:

{((λ x . P) Q)}^{*} ↠_{β} {(P [x : = Q])}^{*} .

Proof. By definition, ${((λ x . P) Q)}^{*} = P^{*} [x : = Q^{*}]$ . By induction over the structure of $P$ , we can check that:

If $Q$ is not a $λ$ -abstraction, then $P^{*} [x : = Q^{*}] = {(P [x : = Q])}^{*}$ ,
If $Q = λ y . Q_{1}$ , then $P^{*} [x : = {(λ y . Q_{1})}^{*}] ↠_{β} {(P [x : = λ y . Q_{1}])}^{*}$ . □

Lemma 2.1.6. Assuming that:

$M \to_{β} N$

Then

M^{*} ↠_{β} N^{*}

Proof. Induction over the structure of $M$ . We’ll leave the easier cases as exercises, and focus on when $M$ is a redex, or when $M = P_{1} P_{2}$ , where $P_{1}$ is not a $λ$ -abstraction and $N = Q_{1} P_{2}$ with $P_{1} \to_{β} Q_{1}$ .

Suppose that $M = (λ x . P_{1}) P_{2}$ is a redex. Then there are three possibilities for $N$ .

(1) $N = P_{1} [x : = P_{2}]$ : here $M^{*} ↠_{β} N^{*}$ by the previous lemma.

(2)

N = (λ x . Q_{1}) P_{2}

, where

P_{1} \to_{β} Q_{1}

: here

N^{*} = Q_{1}^{*} [x : = P_{2}^{*}]

. By the induction hypothesis,

P_{1}^{*} ↠_{β} Q_{1}^{*}

, so

M^{*} = P_{1}^{*} [x : = P_{2}^{*}] ↠_{β} Q_{1}^{*} [x : = P_{2}^{*}] = N .

(3) $N = (λ x . Q_{1}) Q_{2}$ , where $P_{2} \to_{β} Q_{2}$ : is similar.

Now suppose $M = P_{1} P_{2}$ , where $P_{1}$ is not a $λ$ -abstraction, and $N = Q_{1} P_{2}$ with $P_{1} \to_{β} Q_{1}$ . Here $M^{*} = P_{1}^{*} P_{2}^{*}$ . If $Q_{1}$ is not a $λ$ -abstraction, the result is clear. So let $Q_{1} = λ y . R$ . Applying the induction hypothesis to $P_{1} \to_{β} λ y . R$ , we get $P_{1}^{*} ↠_{β} λ y . R^{*}$ . Thus

M^{*} = P_{1}^{*} P_{2}^{*} ↠_{β} (λ y . R^{*}) P_{2}^{*} \to_{β} R^{*} [y : = P_{2}^{*}] = N^{*} . □

Corollary 2.1.7. If $M ↠_{β} N$ , then $M^{*} \to_{β} N^{*}$ .

Proof. Induction over the length of the chain $M ↠_{β} N$ , using Lemma 2.1.6. □

Applying this multiple times, $M ↠_{β} N$ implies $M^{n *} ↠_{β} N^{n *}$ for all $n < ω$ .

Theorem 2.1.8. Assuming that:

$M$ $β$ -reduces to $N$ in $n$ steps

Then

N ↠_{β} M^{n *}

Proof. By induction over $n$ . The base case is clear, as $n = 0$ implies $M = N$ .

For $n > 0$ , there is a term $R$ with $M \to_{β} R \to_{(n - 1) β} N$ . By induction hypothesis, $N ↠_{β} R^{n - 1 *}$ . Since $M \to_{β} R$ , we have $R ↠_{β} M^{*}$ by Lemma 2.1.4. Thus we get $R^{n - 1 *} ↠_{β} M^{n *}$ by the previous observation. Putting it all together:

N ↠_{β} R^{n - 1 *} ↠_{β} M^{n *} . □

Theorem 2.1.9 (Church, Rosser, 1936). Assuming that:

$M, N_{1}, N_{2}$ are $λ$ -terms such that $M ↠_{β} N_{1}, N_{2}$

Then there is a

λ

-term

N

such that

N_{1}, N_{2} ↠_{β} N

Proof. Say $M \to_{r β} N_{1}$ , $M \to_{s β} N_{2}$ . Without loss of generality, say $r \leq s$ . By Theorem 2.1.8, we have that $N_{1} ↠_{β} M^{r *}$ and $N_{2} ↠_{β} M^{s *}$ . But $M^{r *} ↠_{β} M^{s *}$ by successive applications of Lemma 2.1.4 (as $r \leq s$ ). So take $N = M^{s *}$ . □

Reminder of the picture to think of:

This has some important consequences:

If $M \equiv_{β} N$ , then they $↠_{β}$ to the same term;
If the $β$ -normal form of a term exists, it is unique;
We can use this to show that two terms are not $β$ -equivalent.

Example. $λ x . x$ and $λ x . λ y . x$ are different terms in $β$ -normal form, so they can’t be $β$ -equivalent.

Definition 2.1.10 (Church numeral). Let $n$ be a natural number. Its corresponding Church numeral $c_{n}$ is the $λ$ -term $c_{n} : = λ s . λ z . s^{n} (z)$ , where $s^{n} (z)$ denotes

\underset{n times}{\underset{⏟}{s (s (\dots (s}} z) \dots) .

Example 2.1.11. $c_{0} = λ s . λ z . z$ is the ‘function’ that takes $s$ to the identity map.

$c_{1} = λ s . λ z . λ s (z)$ is the ‘function’ that takes $s$ to itself.

$c_{2} = λ s . λ z . s s (z)$ takes a function $s$ to its $2$ -fold composite $z \mapsto s (s (z))$ .

Definition 2.1.12 (lambda-definability). A partial function $f : ℕ^{k} \to ℕ$ is $λ$ -definable if there is a $λ$ -term $F$ such that $F c_{n_{1}} \dots c_{n_{k}} \equiv_{β} c_{f (n_{1}, \dots, n_{k})}$ .

Proposition 2.1.13 (Rosser). Define the following $λ$ -term:

$A_{+} : = λ x . λ y . λ s . λ z . x s (y s (z))$ ,
$A_{*} : = λ x . λ y . λ s . x (y s)$ ,
$A_{e} : = λ x . λ y . y x$ .

Then for all $n, m \in ℕ$ :

$A_{+} c_{n} c_{m} \equiv_{β} c_{n + m}$ ;
$A_{*} c_{n} c_{m} \equiv_{β} c_{n m}$ ;
$A_{e} c_{n} c_{m} \equiv_{β} c_{n^{m}}$ if $m > 0$ .

Proof. We’ll show that $A_{+} c_{n} c_{m} \equiv_{β} c_{n + m}$ , and leave the rest to you.

First note that

c_{n} s z = (λ f . λ x . f^{n} (x)) s z \equiv_{β} (λ x . s^{n} (x)) z \equiv_{β} s^{n} (z) .

So:

\begin{array}{l} A_{+} c_{n} c_{m} & = (λ x . λ y . λ s . λ z . x s (y s z)) c_{n} c_{m} \\ \equiv_{β} (λ y . λ s . λ z . c_{n} s (y s z)) c_{m} \\ \equiv_{β} λ s . λ z . c_{n} s (c_{m} s z)) \\ \equiv_{β} λ s . λ z . s^{n} (s^{m} z) \\ \equiv_{β} λ s . λ z . s^{n} (s^{m} z) \\ \equiv_{β} λ s . λ z . s^{m + n} (z) \\ \equiv_{β} c_{n + m} □ \end{array}

In a similar fashion, we can also encode binary truth-values:

Proposition 2.1.14. Define the $λ$ -terms:

$⊤ : = λ x . λ y . x$
$⊥ : = λ x . λ y . y$
$(if B then P else Q : = B P Q)$

Then for $λ$ -terms $P$ and $Q$ , we have

(i)
$(if ⊤ then P else Q) \equiv_{β} P$ ;
(ii)
$(if ⊥ then P else Q) \equiv_{β} Q$ .

Proof. Just compute it! □

With this, we can encode logical connectives via:

$\neg p : = if p then ⊥ else ⊤$ ;
$\land p_{1} p_{2} : = if p_{1} then (if p_{2} then ⊤ else ⊥) else ⊥$ ;
$\lor p_{1} p_{2} : = if p_{1} then ⊤ else (if p_{2} then ⊤ else ⊥)$ .

We can also encode pairs: if we define $[P, Q] : = λ x . x P Q$ , then $[P, Q] ⊤ \equiv_{β} P$ and $[P, Q] ⊥ \equiv_{β} Q$ . However, it is not true that $[M ⊤, M ⊥] \equiv_{β} M$ !

Recursively defining terms within the $λ$ -calculus requires a clever idea: we see such a term as a solution to a fixed point equation $F = λ x . M$ where $F$ occurs somewhere in $M$ .

Theorem 2.1.15 (Fixed Point Theorem). There is a $λ$ -term $Y$ such that, for all $F$ :

F (Y F) \equiv_{β} Y F .

Proof. Define

Y = λ f . (λ x . f (x x)) λ x . f (x x) .

If we compute $Y F$ , we get:

\begin{array}{l} Y F & = (λ f . (λ x . f (x x)) λ x . f (x x)) F \\ \equiv_{β} (λ x . F (x x)) λ x . F (x x) \\ \equiv_{β} F ((λ x . F (x x)) (λ x . F (x x))) \\ \equiv_{β} F ((λ f . (λ x . f (x x)) λ x . f (x x)) F) \\ \equiv_{β} F (Y F) □ \end{array}

We call any combinator (i.e. a $λ$ -term without free variables) $Y$ satisfying the property $F (Y F) \equiv_{β} Y F$ for all terms $F$ a fixed-point combinator.

Corollary 2.1.16. Given a $λ$ -term $M$ , there is a $λ$ -term $F$ such that $F \equiv_{β} M [f : = F]$ .

Proof. Take $F = Y λ f . M$ . Then

F \equiv_{β} (λ f . M) Y (λ f . M) \equiv_{β} (λ f . M) F \equiv_{β} M [f : = F] . □

Example 2.1.17. Suppose $D$ is a $λ$ -term encoding a predicate, i.e. $P c_{n} \equiv_{β} ⊥$ or $⊤$ for every $n \in ℕ$ . Let’s write down a $λ$ -termthat encodes a program that takes a number and computes the next number satisfying the predicate.

First consider

M : = λ f . λ x . (if (P x) then x else f (S x)),

where $S$ encodes the successor map. Our goal is to have $M$ run on itself. This can be done by using the term $F : = Y M$ . Indeed:

F c_{n} \equiv_{β} (if P c_{n} then c_{n} else F c_{n + 1})

for every $n \in ℕ$ .

Notation. $λ x s z . f$ will be short hand for $λ x . λ s . λ z . f$ (and the obvious generalisation to any number of variables, labelled in any way).

Lemma 2.1.18. The basic partial recursive functions are $λ$ -definable.

Proof. The $i$ -th projection $ℕ^{k} \to ℕ$ is definable by $π_{i}^{k} : λ x_{1} \dots λ x_{k} . x_{i}$ .

Successor is implemented by $S : = λ x . λ s . λ z . s (x s z)$ .

The zero map is given by $Z : = λ x . c_{0}$ .

Just compute! □

Lemma 2.1.19. The class of $λ$ -definable functions is closed under composition.

Proof. Say $G$ is a $λ$ -term defining $g : ℕ^{k} \to ℕ$ , and that $λ$ -terms $H_{1}, \dots, H_{k}$ define $h_{1}, \dots, h_{k} : ℕ^{m} \to ℕ$ . Then the composite map $f : \bar{n} \mapsto g (h_{1} (\bar{n}), \dots, h_{k} (\bar{n}))$ is definable by the term

F : = λ x_{1} \dots x_{m} : (G (H_{1} x_{1} \dots x_{m}) \dots (H_{k} x_{1} \dots x_{m}))

by inspection. □

Lemma 2.1.20. The class of $λ$ -definable functions is closed under primitive recursion.

Proof. Suppose $f : ℕ^{m + 1} \to ℕ$ is obtained from $h : ℕ^{m + 2} \to ℕ$ and $g : ℕ^{m} \to ℕ$ by primitive recursion.

\begin{array}{l} f (0, \bar{n}) & : = g (\bar{n}) \\ f (k + 1, \bar{n}) & : = h (f (k, \bar{n}), k, \bar{n}) \end{array}

and the $λ$ -terms $H$ and $G$ define $h$ and $h$ respectively.

We need a $λ$ -term to keep track of a pair that records the current state of computation: the value of $k$ and the value of $f$ at that stage.

So define

T : = λ p . [S (p π_{1}), H (p π_{2}) (p π_{1}) x_{1} \dots x_{n}],

which acts on a pair $[c_{k}, c_{f (k, \bar{n}}]$ by updating the iteration data. Then $f$ ought to be definable by

F : = λ x . λ x_{1} \dots x_{m} . x T [c_{0}, G x_{1} \dots x_{m}] π_{2} .

Indeed,

\begin{array}{l} F c_{k} c_{n_{1}} \dots c_{n_{m}} & \equiv_{β} c_{k} T [c_{0}, G c_{n_{1}} \dots c_{n_{m}}] π_{2} \\ \equiv_{β} T^{k} [c_{0}, c_{g (π)}] π_{2} \end{array}

by definition of $c_{k}$ , and since

\begin{array}{l} T [c_{k}, c_{f (k, π)}] & \equiv_{β} [S c_{k}, H c_{f (k, \bar{n})} c_{k} c_{n_{1}}, \dots, c_{n_{m}}] \\ \equiv_{β} [c_{k + 1}, c_{h (f (k, \bar{n}), k, \bar{n})}] \end{array}

we have

F c_{k} c_{n_{1}} \dots c_{n_{m}} \equiv_{β} T^{k} ([c_{0}, G c_{n_{1}} \dots c_{n_{m}}]) π_{2} \equiv_{β} c_{f (k, \bar{n})}

as needed. □

Lemma 2.1.21. The $λ$ -definable functions are closed under minimisation.

Proof. Suppose $G$ $λ$ -defines $g : ℕ^{m + 1} \to ℕ$ , and that $f : ℕ^{m} \to ℕ$ is defined from $g$ by minimisation: $f (\bar{n}) = μ k . g (k, \bar{n}) = 0$ .

We can $λ$ -define $f$ by implementing an algorithm that searches for the least $k$ in the following way:

First define a term that can check if a Church numeral is $c_{0}$ , for example

zero? : = λ x . x (λ y . ⊥) ⊤ .

You can check that

zero? c_{n} \equiv_{β} {\begin{matrix} ⊤ & if n = 0 \\ ⊥ & otherwise \end{matrix} .

Now we want a term that, on input $k$ , checks if $g (k, \bar{n}) = 0$ and returns $k$ if so, else runs itself on $k + 1$ . If we can do this, running it on input $k = 0$ will perform the search.

Let:

Search : = λ f . λ g . λ k . λ x_{1} \dots λ x_{m} . (if zero? (g k x_{1} \dots x_{m}) then k else (f (g (S k) x_{1} \dots x_{m}))),

and set

F : = λ x_{1} \dots λ x_{m} . (Y Search) G c_{0} x_{1} \dots x_{m} .

Note that

(Y Search) G c_{k} c_{n_{1}} \dots c_{n_{m}} \equiv_{β} Search (Y Search) G c_{k} c_{n_{1}} \dots c_{n_{m}},

which is

if zero? (G c_{k} c_{n_{1}} \dots c_{n_{m}}) then c_{k} else ((Y Search) G c_{k + 1} c_{n_{1}} \dots c_{n_{m}} .

Thus

(Y Search) G c_{k} c_{n_{1}} \dots c_{n_{m}} \equiv_{β} c_{k}

if $g (k, \bar{n}) = 0$ and

(Y Search) G c_{k} c_{n_{1}} \dots c_{n_{m}} \equiv_{β} (Y Search) G c_{k + 1} c_{1} \dots c_{m}

otherwise, as $g$ is $λ$ -defined by $G$ . Hence

F c_{n_{1}} \dots c_{n_{m}} \equiv_{β} (Y Search) G c_{0} c_{n_{1}} \dots c_{n_{m}} \equiv_{β} c_{f (\bar{n})}

if $f$ is defined on $\bar{n}$ . So $F$ $λ$ -defines $f$ . □

Lemma 2.1.22. Every partial recursive function is $λ$ -definable.

Definition 2.1.23 (Godel numbering). Let $L$ be a first-order language. A Gödel numbering is an injection $L ↪ ℕ$ that is:

(1)
Computable (assuming some notion of computability for strings of symbols over a finite alphabet);
(2)
Its image is a recursive subset of $ℕ$ ;
(3)
Its inverse (where defined) is also computable.

Notation. We will use $⌈ φ ⌉$ to be the Gödel numbering of an element of $L$ , for some fixed choice of Gödel numbering.

One way: assign a unique number $n_{s}$ to each symbol $s$ in your finite alphabet $σ$ . We can then define

⌈ s_{0} \dots s_{k} ⌉ : = \sum_{i = 0}^{k} (n_{s_{i}} + 1) .

Remark. We can also encode proofs: add a symbol $#$ to the alphabet and code a proof with lines $φ_{0}, \dots, φ_{k}$ as $⌈ φ_{0} # φ_{1} # \dots # φ_{k} ⌉$ .

Theorem 2.1.24. Assuming that:

$f$ is $λ$ -definable

Then

f

is partial recursive.

Proof (sketch). Assign Gödel numbers $⌈ τ ⌉$ to $λ$ -terms $τ$ . We can then consider a partial recursive function in $N (t)$ that on input $t$ checks if $t$ is the Gödel numbering of a $λ$ -term $τ$ , and returns the Gödel numbering of its $β$ -normal form if it exists (undefined otherwise).

We also have partial recursive functions that convert $n$ to $⌈ c_{n} ⌉$ and vice-versa. Finally, say $f$ is a partial function defined by a $λ$ -term $F$ . We can compute $f (\bar{m})$ by first converting Church numerals to their Gödel numbers, then append the result to $⌈ F ⌉$ in order to get $⌈ F c_{n_{1}} \dots c_{n_{k}} ⌉$ , then apply $N$ .

If $f$ is defined on $\bar{n}$ , then $F c_{n_{1}} \dots c_{n_{k}}$ has a $β$ -normal form, and what we get is $⌈ c_{f (\bar{n})} ⌉$ . Otherwise $N (⌈ F c_{n_{1}} \dots c_{n_{k}} ⌉)$ is not defined.

We finish by going back from $⌈ c_{f (\bar{n})} ⌉$ to $f (\bar{n})$ . □

2.2 Decidability in Logic

Recall that a subset $X \subseteq ℕ$ is recursive (or decidable) if its characteristic map is total recursive.

Definition 2.2.1 (Recursively enumerable). We say that $X \subseteq ℕ$ is recursively enumerable if any of the following are true:

(1)
$X$ is the image of some partial recursive $f : ℕ \to ℕ$ ;
(2)
$X$ is the image of some total recursive $f : ℕ \to ℕ$ ;
(3)
$X = dom f$ , for $f$ a partial recursive $f : ℕ \to ℕ$ .

Note, if $X$ and $ℕ ∖ X$ are both recursively enumerable, then $X$ is recursive. Note that the set of partial recursive function is countable, so we can fix an enumeration ${f_{0}, f_{1}, \dots}$ .

Example 2.2.2. The subset $W = {(i, x) : f_{i} is defined on x} \subseteq ℕ^{2}$ is recursively enumerable, but not recursive.

Definition 2.2.3 (Recursive / decidable language). A language $L$ is recursive if there is an algorithm that decides whether a string of symbols is an $L$ -formula.

An $L$ -theory $T$ is recursive if membership in $T$ is decidable (for $L$ -sentences).

An $L$ -theory $T$ is decidable if there is an algorithm for deciding whether $T ⊨ φ$ .

We will work with recursive from now on.

Theorem 2.2.4 (Craig). Assuming that:

$T$ is a first order theory with a recursively enumerable set of axioms

Then

T

admits a recursive axiomatisation.

Proof. By hypothesis, there is a total recursive $f$ such that the axioms of $T$ are exactly ${f (n) : n \in ℕ}$ .

Idea: Replace $f (n)$ with something equivalent, but with a shape that lets us retrieve $n$ . Let

ψ_{n} = \land_{k = 1}^{n} (f (n))

for each $n$ and

T^{*} : = {ψ_{n} : n \in ℕ} .

Then $T^{*}$ has the same deductive closure as $T$ . As formulae have finite length, we can check in finite time whether some $χ$ is $f (0)$ or some $\land_{k = 1}^{n} A_{n}$ . By appropriate use of brackets, we can make sure that such an $n$ is “unique” if we are working with some $ψ_{n}$ .

In the first case, we halt and say we have a member of $T^{*}$ . In the second case, we check if $A = f (n)$ , saying we have a member of $T^{*}$ if so, and that we don’t otherwise.

We can do this because we can scan the list ${f (n) : n < ω}$ and check symbol by symbol whether $f (n)$ matches $A$ , which takes finite time.

If the input is not of the right shape, we halt and decide that it is $\notin T^{*}$ . □

Lemma 2.2.5. The set of (Gödel numberings for) total recursive functions is not recursively enumerable.

Proof. Suppose otherwise, so there is a total recursive function whose image is the set of Gödel numberings of total recursive functions.

So for any total recursive $r$ , there is $n$ such that $⌈ f (n) ⌉ = r$ . Define $g : ℕ \to ℕ$ by $g (n) = ⌈ f (n) ⌉ (n) + 1$ . This is certainly total recursive, but can’t be the function coded by $f (m)$ for any $m$ , contradiction. □

Definition 2.2.6 (Language of arithmetic). The language of arithmetic is the first-order language $L_{PA}$ with signature $(0, 1, +, \cdot, <)$ . The base theory of arithmetic is the $L_{PA}$ -theory ${PA}^{-}$ whose axioms express that:

(1)
$+$ and $\cdot$ are commutative and associative, with identity elements $0$ and $1$ respectively;
(2)
$\cdot$ distributes over $+$ ;
(3)
$<$ is a linear ordering compatible with $+$ and $\cdot$ ;
(4)
$\forall x . \forall y . (x < y \to \exists z . x + z = y)$ ;
(5)
$0 < 1 \land \forall x . (x > 0 \to x \geq 1)$ ;
(6)
$\forall x . x \geq 0$ .

The (first-order) theory of Peano arithmetic PA is obtained from ${PA}^{-}$ by adding the scheme of induction: for each $L_{PA}$ -formula $φ (x, \bar{y})$ , the axiom

I φ : = \forall \bar{y} . (φ (0, \bar{y}) \land \forall x . (φ (x, \bar{y}) \to φ (x + 1, \bar{y})) \to \forall x . φ (x, \bar{y})) .

Definition 2.2.7 (Delta0-formula, Sigma1-formula). A $Δ_{0}$ -formula of PA is one whose quantifiers are bounded, i.e. $\exists x < t . φ (x)$ or $\forall x < t . φ (x)$ , where $t$ is not free in $φ$ and $φ$ is quantifier free.

We say $φ (\bar{x})$ is a $Σ_{1}$ -formula if there is a $Δ_{0}$ -formula $ψ (\bar{x}, \bar{y})$ such that

PA ⊢ φ (\bar{x}) \leftrightarrow \exists \bar{y} . ψ (\bar{x}, \bar{y}) .

It is a $Π_{1}$ -formula if there is a $Δ_{0}$ -formula $ψ (\bar{x}, \bar{y})$ such that

PA ⊢ φ (\bar{x}) ⟺ \forall \bar{y} . ψ (\bar{x}, \bar{y}) .

In Example Sheet 4, you will prove that the characteristic function of a $Δ_{0}$ -definable set is partial recursive. We will show that the $Σ_{1}$ -definable sets are precisely the recursively enumerable ones.

Recall that defining $⟨ x, y ⟩ = \frac{(x + y) (x + y + 1)}{2} + y$ yields a total recursive bijection $ℕ^{2} \to ℕ$ .

Applying this a bunch of times, we get total recursive bijections $ℕ^{k} \to ℕ$ by $⟨ v, \bar{w} ⟩ = ⟨ v, ⟨ \bar{w} ⟩ ⟩$ .

This is not good, as we have a different function for each $k$ . We’d like a “pairing function” that lets us see a number as a code for a sequence of any length.

This can be done within any model of PA by using a single function $β (x, y)$ (known as Gödel’s $β$ -function) which is definable in PA.

We want an arithmetic procedure that can associate a code to sequences of any length, and such that the entries of the sequence can be recovered from the code.

We will do this by a clever application of the Chinese Remainder Theorem.

Suppose given a sequence $x_{0}, x_{1}, \dots, x_{n - 1}$ of natural numbers. We want numbers $m + 1, 2 m + 1, \dots, n m + 1$ to serve as moduli, with $x_{i} < (i + 1) m + 1$ , and all of which are pairwise coprime. If we can find $m$ such that these conditions hold, then there is a number $a$ such that $a \equiv x_{i} (m o d (i + 1) m + 1)$ .

Taking $m = \max (n, x_{0}, \dots, x_{m - 1})!$ works.

We say that the pair $(a, m)$ codes the sequence.

Definition 2.2.8 (beta indexing). The function $β : ℕ^{2} \to ℕ$ is defined by $β (x, i) = a % (m (i + 1) + 1)$ , where $a$ and $m$ are the unique numbers such that $x = ⟨ a, m ⟩$ .

Remark. The forumula $β (x, y) = z$ is given in PA by a $Δ_{0}$ -formula. We will use the notation ${(x)}_{i}$ for $β (x, i)$ ; thus the decoding property is that ${(x)}_{i} = x_{i}$ if $x = ⟨ a, m ⟩$ codes $x_{0}, \dots, x_{n - 1}$ .

Lemma 2.2.9 (Godel’s Lemma). Assuming that:

$M ⊨ PA$
$n \in ℕ$
$x_{0}, \dots, x_{n - 1} \in M$

Then there is

u \in M

such that

M ⊨ {(u)}_{i} = x_{i}

for all

i < n

Theorem 2.2.10. Assuming that:

$f : ℕ^{k} \to ℕ$ a partial function

Then

f

is recursive if and only if there is a

Σ_{1}

-formula

𝜃 (\bar{x}, y)

such that

y = f (\bar{x}) ⟺ ℕ ⊨ 𝜃 (\bar{x}, y)

Proof.

\Leftarrow

Suppose that

y = f (\bar{x})

Σ_{1}

-definable by

𝜃 (\bar{x}, y) : = \exists \bar{z} . φ (\bar{x}, y, \bar{z})

(so

φ \in Δ_{0}

The function $fi r s t (x) = (μ y \leq x) . \exists z \leq x . (x = ⟨ y, z ⟩)$ is primitive recursive. By minimisation, the function

g (\bar{x}) = μ z . (\exists v, \bar{w} \leq z . (z = ⟨ v, \bar{w} ⟩ \land φ (\bar{x}, v, \bar{w})))

is partial recursive.

Since $⟨ v, \bar{w} ⟩ = ⟨ v, ⟨ \bar{w} ⟩ ⟩$ for tuples $\bar{w}$ , we have that $fi r s t (⟨ v, \bar{w} ⟩) = v$ . Thus

fi r s t (g (\bar{x})) = {\begin{matrix} The least y such that ℕ ⊨ 𝜃 (\bar{x}, y) & if there is such y \\ undefined & otherwise \end{matrix}

as for each $\bar{x} \in ℕ$ there is at most one $y$ such that $ℕ ⊨ 𝜃 (\bar{x}, y)$ . Now $ℕ ⊨ 𝜃 (\bar{x}, y) ⟺ y = f (\bar{x})$ , so $f (\bar{x}) = fi r s t (g (\bar{x}))$ whenever defined. So $f$ is partial recursive.

\Rightarrow

We will show that the class of all functions with

Σ_{1}

-graphs contains the basic functions and is closed under composition, primitive recursion, and minimisation.

The graphs of zero, successor, and $i$ -th projection are the formulae $y = 0$ , $y = x + 1$ , and $y = x_{i}$ respectively, so are $Σ_{1}$ -definable.

If $f (x_{1}, \dots, x_{k})$ and $g_{1} (\bar{z}), \dots, g_{k} (\bar{z})$ all have $Σ_{1}$ -graphs, then the graph of the composite is given by:

\exists u_{1}, \dots, u_{k} . \land_{i = 1}^{n} (u_{i} = g_{i} (\bar{z}) \land y = f (u_{1}, \dots, u_{k})) .

This is equal to a $Σ_{1}$ -formula, as those are closed under $\land, \exists$ . If $f (\bar{x}, y)$ is obtained by primitive recursion

{\begin{matrix} f (\bar{x}, 0) = g (\bar{x}) \\ f (\bar{x}, y + 1) = h (\bar{x}, y, f (\bar{x}, y)) \end{matrix}

where $g$ and $h$ have $Σ_{1}$ -graphs, then we can use Godel’s Lemma to show that the graph of $f$ is given by

\exists u, v . (v = g (\bar{x}) \land {(u)}_{0} = v \land {(u)}_{y} = z \land \forall i < y . \exists r, s . [r = {(u)}_{i} \land s = {(u)}_{i + 1} \land s = h (\bar{x}, i, r)] .

We do this by coding the sequence $f (\bar{x}, 0), f (\bar{x}, 1), \dots, f (\bar{x}, y)$ by $u$ . This formula is equal to a $Σ_{1}$ -formula since:

(1) $z = {(x)}_{y}$ is $Δ_{0}$ ;

(2) If the graph of

h

is defined by

\exists \bar{t} . ψ (\bar{x}, i, r, s, \bar{t})

with

ψ \in Δ_{0}

, then

\forall i < y . \exists r, s [r = {(u)}_{i} \land s = {(u)}_{i + 1} \land s = h (\bar{x}, i, r)]

is equal to

\exists w . \forall i < y . \exists r, s, \bar{t} \leq w (r = {(u)}_{i} \land s = {(u)}_{i + 1} \land ψ (\bar{x}, i, r, s, \bar{t}))

as we can take $w$ to be the maximum between suitable $r, s, \bar{t}$ with $r = {(u)}_{i}$ , $s = {(u)}_{i + 1}$ , $ψ (\bar{x}, i, r, s, \bar{t})$ with $i = 0, 1, \dots, y - 1$ .

A similar argument gives closure under minimisation.

If $f (\bar{x})$ is $μ y . g (\bar{x}, y) = 0$ and the graph of $g$ is definable by a $Σ_{1}$ -formula, then the graph of $f$ is definable by

\exists u . ({(u)}_{y} = 0 \land \forall i < y . ({(u)}_{i} \neq 0 \land \underset{(*)}{\underset{⏟}{\forall j \leq y . \exists v (v = g (\bar{x}, j) \land v = {(u)}_{j})}}))

by using Godel’s Lemma to code $g (\bar{x}, 0), g (\bar{x}, 1), \dots, g (\bar{x}, f (\bar{x}))$ .

Again, this is equal to a $Σ_{1}$ -formula if the graph of $g$ is given by $\exists \bar{w} φ (\bar{x}, y, z, \bar{w})$ with $φ \in Δ_{0}$ , then $(*)$ is equal in $ℕ$ to

\exists s . \forall j \leq y . \exists v, \bar{w} \leq s . (v = {(u)}_{j} \land φ (\bar{x}, j, v, \bar{w})) . □

Corollary 2.2.11. A subset $A \subseteq ℕ^{k}$ is recursively enumerable if and only if there is a $Σ_{1}$ -formula $ψ (x_{1}, \dots, x_{k})$ such that, given $\bar{x} \in ℕ^{k}$ , we have $\bar{x} \in A$ if and only if $ℕ ⊨ ψ (x)$ .

Proof.

$\Rightarrow$ If $A$ is recursively enumerable, then there is a recursive $f$ such that $A = dom (f)$ . Given $\bar{x} \in ℕ^{k}$ , we thus have $x \in A$ if and only if $ℕ ⊨ \exists v . v = f (\bar{x})$ . But $\exists v . v = f (\bar{x})$ is equal to a $Σ_{1}$ -formula by Theorem 2.2.10.
$\Leftarrow$ Conversely, if $A$ is defined in $ℕ$ by a $Σ_{1}$ -formula $ψ$ , define $f (\bar{x}) = 0$ if $ℕ ⊨ ψ (\bar{x})$ , and $f (\bar{x}) ↑$ otherwise. The graph of $f$ is given by $y = 0 \land ψ (\bar{x})$ , which is $Σ_{1}$ , and so $f$ is recursive by Theorem 2.2.10. But $A = dom (f)$ , so $A$ is recursively enumerable. □

Any model of PA $^{-}$ includes a copy of $ℕ$ inside of it: consider the standard natural numbers

\underset{̲}{n} = \underset{n}{\underset{⏟}{S S S \dots S}} 0 .

In fact, $ℕ$ embeds in any model PA $^{-}$ as an initial segment: essentially because

PA^{-} ⊢ \forall x . (x \leq \underset{̲}{k} \to x = \underset{̲}{0} \land x = \underset{̲}{1} \land \dots \land x = \underset{̲}{k}) .

In Example Sheet 4, you will see that $ℕ$ is a $Δ_{0}$ -elementary substructure of any model of PA $^{-}$ : every $Δ_{0}$ -sentence $φ (\underset{̲}{n})$ true in $ℕ$ is also true in the model.

Definition 2.2.12 (Representation of a total function). Let $f : ℕ^{k} \to ℕ$ be total and $T$ be any $L_{PA}$ -theory extending PA $^{-}$ . We say that $f$ is represented in $T$ if there is an $L_{PA^{-}}$ formula $𝜃 (x_{1}, \dots, x_{k}, y)$ such that, for all $\bar{n} \in ℕ^{k}$ :

(a)
$T ⊢ \exists! y . 𝜃 (\bar{n}, y)$
(b)
If $k = f (\bar{n})$ , then $T ⊢ 𝜃 (\bar{n}, \underset{̲}{k})$

Lemma 2.2.13. Every total recursive function $f : ℕ^{k} \to ℕ$ is $Σ_{1}$ -represented in PA $^{-}$ .

Proof. The graph of $f$ is given by a $Σ_{1}$ -formula by Theorem 2.2.10, say $\exists \bar{z} . φ (\bar{x}, y, \bar{z})$ where $φ \in Δ_{0}$ . Without loss of generality, we may assume that $\bar{z}$ is a single variable (for example, rewrite $\exists z . \exists \bar{w} < z . φ (\bar{x}, y, \bar{w})$ ).

Let $ψ (\bar{x}, y, z)$ be the $Δ_{0}$ -formula

φ (\bar{x}, y, z) \land \forall u, v \leq y + z . (u + v < y + z \to \neg φ (\bar{x}, u, v)) .

Then the $Σ_{1}$ -formula $𝜃 (\bar{x}, y) : = \exists z . ψ (\bar{x}, y, z)$ represents $f$ in PA $^{-}$ .

We show $PA^{-} ⊢ 𝜃 (\bar{n}, k)$ first, where $k = f (\bar{n})$ . Note that $k$ is the unique element of $ℕ$ such that $ℕ ⊨ \exists z . φ (\bar{n}, k, z)$ , as $f$ is a function.

Take $l$ to be the first natural number such that $ℕ ⊨ φ (\bar{n}, k, l)$ . Then $ℕ ⊨ ψ (\bar{n}, k, l)$ too, whence $ℕ ⊨ \exists z . ψ (\bar{n}, k, z)$ . But any $Σ_{1}$ -sentence true in $ℕ$ is true in any model of PA $^{-}$ (c.f. Example Sheet 4), so $PA^{-} ⊢ \exists z . ψ (\bar{n}, k, z)$ , i.e. $PA^{-} ⊢ 𝜃 (\bar{n}, k)$ .

To see that $PA^{-} ⊢ \exists! y . 𝜃 (\bar{n}, y)$ , let $l$ be the first number such that $ℕ ⊨ φ (\bar{n}, k, l)$ , where $k = f (\bar{n})$ . Suppose $a, b \in M ⊨ PA^{-}$ , with $M ⊨ ψ (\bar{n}, a, b)$ . We will show that $a = k$ . Completeness settles the claim. Again, $φ (\bar{n}, k, l)$ is a $Δ_{0}$ -sentence true in $ℕ$ , thus true in $M$ .

Using the fact that $<$ is a linear ordering in $M$ , we have $a, b \leq k + l \in ℕ$ , so $a, b \in ℕ$ (as $ℕ$ is an initial segment of $M$ ). Now $M ⊨ ψ (\bar{n}, a, b) \in Δ_{0}$ , hence $ℕ ⊨ ψ (\bar{x}, a, b)$ and thus $ℕ ⊨ \exists z . φ (\bar{n}, a, z)$ . Thus $a = k$ as needed. □

Corollary 2.2.14. Every recursive set $A \subseteq ℕ^{k}$ is $Σ_{1}$ -representable in PA $^{-}$ .

Proof. The characteristic function $χ_{A}$ of $A$ is total recursive, so $χ_{A} (\bar{x}) = y$ is represented by some $Σ_{1}$ -formula $𝜃 (\bar{x}, y)$ in PA $^{-}$ . But then $𝜃 (\bar{x}, 1)$ represents $A$ in PA $^{-}$ . □

Lemma 2.2.15 (Diagonalisation Lemma). Assuming that:

$T$ an $L_{PA}$ -theory
in $T$ , every total recursive function is $Σ_{1}$ -represented
$𝜃 (x)$ an $L_{PA}$ -formula with one free variable $x$

Then there is an

L_{PA}

-sentence

G

such that

T ⊢ G \leftrightarrow 𝜃 (⌈ G ⌉) .

Moreover, if $𝜃$ is a $Π_{1}$ -formula, then we can take $G$ to be a $Π_{1}$ -sentence.

Proof. Define a total recursive function $diag$ this way: on input $n \in ℕ$ , check if $n = ⌈ σ (x) ⌉$ is the Gödel numbering of some $L_{PA}$ -formula $σ (x)$ . If so, return $⌈ \forall y . (y = \underset{̲}{n} \to σ (y)) ⌉$ , else return $0$ .

As $diag$ is total recursive, it is $Σ_{1}$ -represented in $T$ by some $δ (x, y)$ . Consider the formula

ψ (x) : = \forall z . (δ (x, z) \to 𝜃 (z)) .

Let $n = ⌈ ψ (x) ⌉$ and $G : = \forall y . (y = \underset{̲}{n} \to ψ (y))$ . This makes $G$ the sentence whose Gödel numbering is $diag (⌈ ψ (x) ⌉)$ . It is obvious that $T ⊢ G \leftrightarrow ψ (\underset{̲}{n})$ , so we know that

T ⊢ G \leftrightarrow \forall z . (δ (\underset{̲}{n}, z) \to 𝜃 (z)) . (α)

Now $δ (x, y)$ represents $diag$ in $T$ , and $diag (n) = ⌈ G ⌉$ by construction, hence

T ⊢ \forall z . (δ (\underset{̲}{n}, z) \leftrightarrow z = ⌈ G ⌉) . (β)

Combining ( $α$ ) and ( $β$ ), we get $T ⊢ G \leftrightarrow 𝜃 (⌈ G ⌉)$ as needed.

Finally, note that if $𝜃 \in Π_{1}$ , then both $ψ$ and $G$ are equal to a $Π_{1}$ -formula. □

Theorem 2.2.16 (Crude Incompleteness). Assuming that:

$T$ be a recursive set of (Gödel numberings of) $L_{PA}$ -sentences
$T$ is consistent (never includes both $φ$ and $\neg φ$ )
$T$ contains all the $Σ_{1}$ and $Π_{1}$ sentences provable in PA $^{-}$

Then there is a

Π_{1}

-sentence

τ

such that

τ \notin T

and

\neg τ \notin T

Proof. Let $𝜃 (x)$ be a $Σ_{1}$ -formula that represents $T$ in PA $^{-}$ , so that

x \in T ⟺ PA^{-} ⊢ 𝜃 (x) and x \notin T ⟺ PA^{-} ⊢ \neg 𝜃 (x) .

This exists since $T$ is recursive. By the Diagonalisation Lemma, there is a $Π_{1}$ -sentence $τ$ such that $PA^{-} ⊢ τ \leftrightarrow \neg 𝜃 (⌈ τ ⌉)$ .

If $⌈ τ ⌉ \in T$ , then $PA^{-} ⊢ 𝜃 (⌈ τ ⌉)$ , and thus $PA^{-} ⊢ \neg τ$ . But then $⌈ \neg τ ⌉ \in T$ (as $\neg τ \in Σ_{1}$ and $PA^{-}$ proves it).

If $⌈ \neg τ ⌉ \in T$ , then $τ \notin T$ , so $PA^{-} ⊢ \neg 𝜃 (⌈ τ ⌉)$ , and thus $PA^{-} ⊢ τ$ . As $τ \in Π_{1}$ and $PA^{-} ⊢ τ$ , we have $⌈ τ ⌉ \in T$ .

Since $T$ is consistent, we can’t have either of $⌈ τ ⌉$ or $⌈ \neg τ ⌉$ in $T$ . □

Corollary 2.2.17 (Godel-Rosser Theorem). Let $T$ be a consistent $L_{PA}$ -theory extending $PA^{-}$ and admitting a recursively enumerable axiomatisation. Then $T$ is $Π_{1}$ -incomplete: there is a $Π_{1}$ -sentence $τ$ such that $T ⁄ ⊢ τ$ and $T ⁄ ⊢ \neg τ$ .

Proof. By Craig’s Theorem, we may assume that $T$ is recursive. Suppose that $T$ is $Π_{1}$ -complete, and consider the set $S$ of (Gödel numberings of) all the $Σ_{1}$ and $Π_{1}$ sentences in $L_{PA}$ that $T$ proves.

The set $S$ is recursive: we can effectively decide if a given sentence is $Σ_{1}$ or $Π_{1}$ , then check if $⌈ σ ⌉ \in S$ by systematically searching through all proofs using the axioms in $T$ , until we either find a proof of $σ$ or a proof of $\neg σ$ . Since $T$ is $Π_{1}$ -complete, there is always such a proof, and we’ll find it in finite time.

But then $S$ satisfies the hypotheses of Theorem 2.2.16, so there is a $Π_{1}$ -sentence $τ$ with $⌈ τ ⌉ \notin S$ and $⌈ \neg τ ⌉ \notin S$ , contradicting $Π_{1}$ -completeness of $T$ . □

Definition 2.2.18 (Recursive structure). A (countable) $L_{PA}$ -structure $M$ is recursive if there are total recursive functions $\oplus : ℕ^{2} \to ℕ$ , $\otimes : ℕ^{2} \to ℕ$ , a binary recursive relation $≼ \subseteq ℕ^{2}$ , and natural numbers $n_{0}, n_{1} \in ℕ$ such that $M ≅ (ℕ, \oplus, \otimes, ≼, n_{0}, n_{1})$ as $L_{PA}$ -structures.

We will show that the usual $ℕ$ is the only recursive model of $PA$ (up to $≅$ ).

Strategy:

(1) Given a countable model $M$ of $PA$ , we note that we encode subsets of $ℕ$ as elements of $M$ ;
(2) If $M$ is non-standard, then there is an element that codes a non-recursive set;
(3) If $M$ also has recursive $\oplus$ , then there is a membership decision procedure for any subset that it codes.

Note that there is a $Σ_{1}$ -formula $pr (x, y)$ that captures $y$ being the $x$ -th prime, and $PA ⊢ \forall x . \exists! y . pr (x, y)$ . So if $ℕ$ thinks that $k$ is the $n$ -th prime, then any model of $PA$ thinks so too. Write $π_{n}$ for the $n$ -th prime.

Lemma 2.2.19 (Overspill). Assuming that:

$M$ a non-standard model of $PA$
$φ (x)$ an $L_{PA}$ -formula
$M ⊨ φ (n)$ for all standard natural numbers $n$

Then there is a nonstandard natural number

e

such that

M ⊨ φ (e)

Proof. Say $M ⊨ φ (n)$ for all standard $n$ , but only them. Then $M ⊨ φ (0)$ and $M ⊨ \forall n . (φ (n) \to φ (n + 1))$ holds (if $φ (n)$ holds, then $n$ and hence $n + 1$ are standard).

By $I φ$ (induction), we conclude that $M ⊨ \forall n . φ (n)$ . But $M$ is non-standard, so there is non-standard $e \in M$ with $φ (e)$ , contradiction. □

Fix some $m \in ℕ$ , and a property $φ (x)$ of the natural numbers.

There is a number $c$ such that $\forall k < m . (φ (k) \leftrightarrow π_{k} | c)$ , namely the product of all primes $π_{k}$ with $k < m$ and $φ (k)$ .
We perceive $c$ as a code for the numbers with the property $φ$ below $m$ , which we can decode by prime factorisation.

Definition 2.2.20 (Canonically coded). A subset $S \subseteq ℕ$ is canonically coded in a model $M$ of $PA$ if there is $c \in M$ such that

S = {n \in ℕ : \exists y . (π_{\underset{̲}{n}} \times y = c)}

where $\underset{̲}{n}$ denotes the standard number $n$ in the model.

We could use other formulas to code subsets. Th subsets of $ℕ$ coded in $M$ are those $S \subseteq ℕ$ for which there is a $PA$ -formula $φ (x, y)$ and $c \in M$ such that $S = {n \in ℕ : M ⊨ φ (\underset{̲}{n}, c)}$ .

As it turns out, coding via $Σ_{1}$ -formulae gives nothing new:

Proposition 2.2.21. Assuming that:

$C (u, x)$ be a $Δ_{0}$ -formula
$M$ a non-standard model of $PA$

Then given any

\tilde{b} \in M

, there is

c \in M

such that, for any

n \in ℕ

M ⊨ \exists k < \tilde{b} . C (k, n) \leftrightarrow \exists y . (π_{\underset{̲}{n}} \times y) = c .

Proof (sketch*). The following formula holds in $ℕ$ for any $n$ :

\forall b . \exists a . \forall u < n . (\exists k < b . C (k, u) \leftrightarrow \exists y . (π_{u} \times y) = a) .

This is by the reasoning we gave when introducing codes, which works due to the bound on $k$ and $u$ . This can be proved in $PA$ *.

Thus

M ⊨ \forall b . \exists a . \forall u < \underset{̲}{n} . (\exists k < b . C (k, u) \leftrightarrow \exists y . (π_{u} \times y = a))

for any $n \in ℕ$ . So by Lemma 2.2.19 there is a non-standard $w \in M$ such that

M ⊨ \forall b . \forall a . \forall u < w . (\exists k < b . C (k, u) \leftrightarrow \exists y . (π_{u} \times y = a)) .

So for any $\tilde{b} \in M$ , there must be $c \in M$ such that

M ⊨ \forall u < w . (\exists k < \tilde{b} . C (k, u) \leftrightarrow \exists y . (π_{u} \times y = c)) .

Now $w$ is non-standard, so $M ⊨ \underset{̲}{n} < w$ for all $n \in ℕ$ . So for any $\tilde{b} \in M$ there is $c \in M$ with

M ⊨ \exists k < \tilde{b} . C (k, n) \leftrightarrow \exists y . (π_{\underset{̲}{n}} \times y = c)

for all $n \in ℕ$ . □

Definition 2.2.22 (Recursively inseparable). We say that subsets $A, B \subset ℕ$ are recursively inseparable if they are disjoint and there is no recursive $C \subseteq ℕ$ with $B \cap C = \emptyset$ and $A \subseteq C$ .

Proposition 2.2.23. There are recursively enumerable subsets $A, B \subseteq ℕ$ that are recursively inseparable.

Proof. Fix an effective enumeration ${φ_{n} : n < ω}$ of the partial recursive functions. Define $A = {n \in ℕ : φ_{n} (n) = 0}$ and $B = {n \in ℕ : φ_{n} (n) = 1}$ , which are clearly disjoint and are clearly recursively enumerable.

Suppose there is a recursive $C$ with $A \subseteq C$ and $B \cap C = \emptyset$ , and write $χ_{C}$ for its (total recursive) characteristic function. There must be $u \in ℕ$ such that $χ_{C} = φ_{u}$ , as $χ_{C}$ is total recursive.

Since $χ_{C} (u) ↓$ and is either $0$ or $1$ , we have either $u \in A$ or $u \in B$ .

If $u \in A$ , then $χ_{C} (u) = φ_{u} (u) = 0$ , so $u \notin C$ , contradicting $A \subseteq C$ ; so $u \in B$ . But then $χ_{C} (u) = φ_{u} (u) = 1$ , so $u \in C$ , contradicting $B \cap C = \emptyset$ . Thus $A$ and $B$ are recursively inseparable. □

Lemma 2.2.24. Assuming that:

$M ⊨ PA$ non-standard

Then there is a non-recursive set

S

which is canonically coded in

M

Proof. Say $A, B \subseteq ℕ$ are recursively enumerable and recursively inseparable. By Corollary 2.2.11, there are $Σ_{1}$ -formulae $\exists u . a (u, x)$ and $\exists u . b (u, x)$ defining $A$ and $B$ respectively (so $a$ and $b$ are $Δ_{0}$ -formulae).

Fix $n \in ℕ$ . As the sets are disjoint, we have:

ℕ ⊨ \forall v < n . \forall w < n . \forall x < n . \neg (a (v, x) \land b (w, x)) .

As this sentence is $Δ_{0}$ , it follows, for any non-standard $M ⊨ PA$ and $\underset{̲}{n} \in M$ that:

M ⊨ \forall v < \underset{̲}{n} . \forall w < \underset{̲}{n} . \forall x < \underset{̲}{n} . \neg (a (v, x) \land b (w, x)) .

By Overspill, there is some non-standard $c \in M$ such that

M ⊨ \forall v < c . \forall w < c . \forall x < x . \neg (a (v, x) \land b (w, x)) . (∗)

Now define $X : = {n \in ℕ : \exists v < c . a (v, \underset{̲}{n})}$ . Note that:

$A \subseteq X$ : let $n \in A$ , so that $ℕ ⊨ a (m, n)$ for some $m \in ℕ$ (a $A$ is defined by $\exists u . a (u, x)$ ). Then $M ⊨ a (\underset{̲}{m}, \underset{̲}{n})$ , as $a$ is $Δ_{0}$ . Hence $M ⊨ \exists v < c . a (v, \underset{̲}{n})$ as any standard $\underset{̲}{m}$ is below $c$ as it is non-standard. But then $n \in X$ .
$B \cap X = \emptyset$ : if $n \in B$ , then $ℕ ⊨ b (m, n)$ for some $m$ , so arguing as before we get $M ⊨ \exists w < c . b (w, \underset{̲}{n})$ . By ( $*$ ), we can deduce $M ⊨ \neg \exists v < c . a (v, \underset{̲}{n})$ . So $n \notin X$ .

As $A$ and $B$ are recursively inseparable, $X$ can’t be recursive. This shows that $M$ must encode a non-recursive set, which implies that it must canonically encode a non-recursive set by Proposition 2.2.21. □

Theorem 2.2.25 (Tennenbaum). Assuming that:

$M = (M, \oplus, \otimes, ≼, n_{0}, n_{1})$ a countable non-standard model of $PA$

Then

\oplus

is not recursive.

Proof. As $M$ is countable, we may as well assume that $M = ℕ$ , $n_{0} = 0$ , $n_{1} = 1$ .

By Lemma 2.2.24, there is some $c \in M$ that canonically codes a non-recursive subset $X = {n : M ⊨ \exists y . (π_{\underset{̲}{n}} \times y = c)} \subseteq ℕ$ .

As $PA$ proves that

π_{\underset{̲}{n}} \times x = \underset{π_{n} times}{\underset{⏟}{x + \dots + x}},

we have that

π_{\underset{̲}{n}} \times y = \underset{π_{n} times}{\underset{⏟}{y + \dots + y}}

for all $y \in M$ . So $n \in X$ if and only if there is $d \in M$ such that

c = \underset{π_{n} times}{\underset{⏟}{d \oplus \dots \oplus d}} .

Suppose $\oplus$ is recursive. Then we can can through $ℕ$ (which is $M$ ) and look for some $d \in M$ that realises the disjunction of:

{\begin{matrix} c = \underset{π_{n} x ’s}{\underset{⏟}{x \oplus \dots \oplus x}} \\ c = \underset{π_{n} x ’s}{\underset{⏟}{x \oplus \dots \oplus x}} \oplus 1 \\ \dots c = \underset{π_{n} x ’s}{\underset{⏟}{x \oplus \dots \oplus x}} \oplus \underset{π_{n} - 1 ones}{\underset{⏟}{1 \oplus \dots \oplus 1}} \end{matrix}

As $\oplus$ is recursive, we can decide whether the disjunction holds of a given $d$ . Moreover, the search for such $d$ always terminates:

Euclidean division is provable in $PA$ : for any $u, v \in M$ with $v \neq 0$ , there are unique $q, r \in M$ such that $r ≼ v$ and $u = (v \otimes q) \oplus r$ .
$PA ⊢ \forall x . (x < π_{1} \leftrightarrow (x = 0 \land x = 1 \land \dots \land x = (1 + \dots + 1));$

Combining these, we get that division of $c$ by $π_{\underset{̲}{n}}$ in $M$ leaves a unique quotient $d \in M$ , and remainder $r ≼ π_{\underset{̲}{n}}$ , which is either $0$ or $1$ or $1 \oplus 1$ or …or $1 \oplus 1 \oplus \dots \oplus 1$ ( $π_{n} - 1$ times); i.e. one of the disjunctions from before.