Title: Daniel's Flashcards / Year 4 / Term 1 / Logic and Computability

html: Theorem 1.1.1 (Diaconescu). The law of excluded middle can be intuitionistically deduced from the Axiom of Choice.
proof: 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 ∈ { 0 , 1 } : φ ∨ ( x = 0 ) } B : = { x ∈ { 0 , 1 } : φ ∨ ( x = 1 ) } .
As 0 ∈ A and 1 ∈ B, we have that { A , B } is a family of inhabited sets, thus admits a choice function f : { A , B } → A ∪ B by the Axiom of Choice. This satisfies f ( A ) ∈ A and f ( B ) ∈ B by definition.
Thus we have
( f ( A ) = 0 ∨ φ ) ∧ ( f ( B ) = 1 ∨ φ )
and f ( A ) , f ( B ) ∈ { 0 , 1 }. Now f ( A ) ∈ { 0 , 1 } means that ( f ( A ) = 0 ) ∨ ( f ( A ) = 1 ) and similarly for f ( B ).
We can have the following:
- (1) We have a proof of f ( A ) = 1, so φ ∨ ( 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 ¬ ⁡ φ: 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 ¬ ⁡ φ. □
nothing: True

html: 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: Proof. Induction over the size of proofs. □
cloze1: True

html: Definition 1.2.1 (Simply typed lambda-term). The set Λ Π of simply typed λ-terms is defined by the grammar
Λ Π : = V ⏟ variables | λ V : Π . Λ Π ⏟ λ -abstraction | Λ Π Λ Π ⏟ λ -application .
A context is a set of pairs { x 1 : τ 1 , … , x n : τ n } where the x i are (distinct) variables and each τ i ∈ Π. We write C for the set of all possible contexts. Given a context Γ ∈ C, we also write Γ , x : τ for the context Γ ∪ { 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.
nothing: True

html: Definition 1.2.2 (Typability relation). We define the typability relation ⊩ ⊆ C × Λ Π × Π 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 σ , τ ∈ Π be types, and M be a λ-term. If Γ , x : σ ⊩ M : τ, then Γ ⊩ ( λ x : σ . M ) : ( σ → τ ).
- (3)
Let Γ be a context, σ , τ ∈ Π be types, and M , N ∈ Λ Π be terms. If Γ ⊩ M : ( σ → τ ) and Γ ⊩ N : σ, then Γ ⊩ ( M N ) : τ.
nothing: True

html: Definition 1.2.3 (beta-reduction). The β-reduction relation is the smallest relation → β on Λ Π closed under the following rules:
- ( λ x : σ . P ) Q → β P [ x : = Q ],
- if P → β P ′, then for all variables x and types σ ∈ Π, we have λ x : σ . P → β λ x : σ . P ′,
- P → β P ′ and z as a λ-term, then P Z → β P ′ Z and Z P → β Z P ′.
We also define β-equivalence ≡ β as the smallest equivalence relation containing → β.
nothing: True

html: Lemma 1.2.5 (Free variables lemma). Assuming that:
- Γ ⊩ M : σ
Then
- (1) If Γ ⊆ Γ ′, then Γ ′ ⊩ M : σ.
- (2) The free variables of M occur in Γ.
- (3) There is a context Γ ∗ ⊆ Γ comprising exactly the free variables in M, with Γ ∗ ⊩ M : σ.
proof: Proof. Exercise. □
nothing: True

html: Lemma 1.2.6 (Generation Lemma).
- (1)
For every variable x, context Γ, and type σ, if Γ ⊩ x : σ, then x : σ ∈ Γ;
- (2)
If Γ ⊩ ( M N ) : σ, then there is a type τ such that Γ ⊩ M : τ → σ and Γ ⊩ N : τ;
- (3)
If Γ ⊩ ( λ x . M ) : σ, then there are types τ and ρ such that Γ , x : τ ⊩ M : ρ and σ = ( τ → ρ ).
proof: Proof. By induction on the derivation of M → β N, using Lemma 1.2.6 and Lemma 1.2.7. □
nothing: True

html: 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 ] : σ.
proof: Proof. By induction on the derivation of M → β N, using Lemma 1.2.6 and Lemma 1.2.7. □
nothing: True

html: Proposition 1.2.8 (Subject reduction). Assuming that:
- Γ ⊩ M : σ
- M → β N
Then Γ ⊩ N : σ.
proof: Proof. By induction on the derivation of M → β N, using Lemma 1.2.6 and Lemma 1.2.7. □
nothing: True

html: 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 : σ.
proof: 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). □
nothing: True

html: Definition (b e t a-normal form). A λ-term M is in β-normal form if there is no term N such that M → β N.
nothing: True

html: Corollary 1.2.10 (Uniqueness of normal form). If a simply typed λ-term admits a β-normal form, then it is unique.
proof: 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). □
nothing: True

html: Proposition 1.2.11 (Uniqueness of types).
- (1)
If Γ ⊩ M : σ and Γ ⊩ M : τ, then σ = τ.
- (2)
If Γ ⊩ M : σ, Γ ⊩ N : τ, and M ≡ β N, then σ = τ.
proof: 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). □
nothing: True

html: Definition 1.2.13 (Height). The height function is the recursively defined map h : Π → ℕ that maps a type variable to 0, and a function type σ → τ to 1 + max ⁡ ( h ( σ ) , h ( τ ) ).
We extend the height function from types to β-redexes by taking the height of its λ-abstraction.
nothing: True

html: Theorem 1.2.14 (Weak normalisation for lambda(->)). Assuming that:
- Γ ⊩ M : σ
Then there is a finite reduction path M : = M 0 → β M 1 → β M 2 → β ⋯ → β M n, where M n is in β-normal form.
proof: Proof (“Taming the Hydra”). The idea is to apply induction on the complexity of M. Define a function m : Λ Π → ℕ × ℕ by
m ( M ) = { ( 0 , 0 ) if M is in β -normal form ( h ( M ) , r e d e x ( M ) ) otherwise ,
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 ω × ω 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 : ( ρ → μ ) … x P ρ … ) ( λ y : ρ . Q μ ) P → μ, then it reduces to … ( λ y : ρ . Q μ ) ρ → μ P μ …, in which case there is a new redex of height h ( ρ → μ ) < h.
- (2) We have Δ = ( λ x : τ . ( λ y : ρ . R μ ) ) P τ occurring in M in the scenario Δ ρ → μ Q ρ. Say Δ reduces to λ y : ρ . R 1 μ. Then we create a new redex of height h ( ρ → μ ) < h ( τ → ( ρ → μ ) ) = h.
- (3) The last possibility is that Δ = ( λ x : ( ρ → μ ) . x ) ( λ y : ρ . P μ ), and that it occurs in M as Δ ρ → μ Q ρ. Reduction then gives the redex ( λ y : ρ . P μ ) ρ → μ Q ρ of height h ( ρ → μ ) < 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). □
nothing: True

html: Theorem 1.2.15 (Strong Normalisation for lambda(->)). Assuming that:
- Γ ⊩ M : σ
Then there is no infinite reduction sequence M → β M 1 → β ⋯.
proof: Proof. See Example Sheet 1. □
nothing: True

html: Proposition 1.3.1 (Curry-Howard for IPC(->)). Assuming that:
- Γ is a context for λ ( → )
- φ a proposition
Then
- (1) If Γ ⊩ M : φ, then | Γ | = { τ ∈ Π : ( x : τ ) ∈ Γ for some x } ⊢ IPC( → ) φ
- (2) If | Γ | ⊢ IPC( → ) φ, then there is a simply typed λ-term M ∈ λ ( → ) such that { ( x ψ : ψ ) | ψ ∈ Γ } ⊩ M : φ.
proof: 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 : φ | = | Γ ′ | ∪ { φ }.
If the derivation has M of the form λ x : σ . N and φ = σ → τ, then we must have Γ , x : σ ⊩ N : τ. By the induction hypothesis, we have that | Γ , x : σ | ⊢ τ, i.e. | Γ | , σ ⊢ τ. But then | Γ | ⊢ σ → τ by (→-I).
If the derivation has the form Γ ⊩ ( P Q ) : φ, then we must have Γ ⊩ P : ( σ → φ ) and Γ ⊩ Q : σ. By the induction hypothesis, we have that | Γ | ⊢ σ → φ and | Γ | ⊢ σ, so | Γ | ⊢ φ by (→-E).
- (2) Again, we induct over the derivation of Γ ⊢ φ. Write Δ = { ( x ψ : ψ ) | ψ ∈ Γ }. Then we only have a few ways to construct a proof at a given stage. Say the derivation is of the form Γ , φ ⊢ φ. If φ ∈ Γ, then clearly Δ ⊩ x φ : φ, and if φ ∉ Γ then Δ , x φ : φ ⊩ x φ : φ.
Suppose the derivation is at a stage of the form
Γ ⊢ φ → ψ Γ ⊢ φ Γ ⊢ ψ .
Then by the induction hypothesis, there are λ-terms M and N such that Δ ⊩ M : ( φ → ψ ) and Δ ⊩ N : φ, from which Δ ⊩ ( M N ) : φ.
Finally, if the stage is given by
Γ , φ ⊢ ψ Γ ⊢ φ → ψ ,
then we have two sub-cases:
  - If φ ∈ Γ, 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 ) : ( φ → ψ ) as needed.
  - If φ ∉ Γ, then the induction hypothesis gives Δ , x φ : φ ⊩ M : ψ for some M, thus Δ ⊩ ( λ x φ : φ . M ) : ( φ → ψ ) as needed. □
nothing: True

html: Definition 1.3.3 (Full STlambdaC). The types of the full simply typed λ-calculus are generated by the following grammar:
Π : = U | Π → Π | Π × Π | Π + Π | 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.
nothing: True

html: Definition 1.4.1 (Lattice). A lattice is a set L equipped with binary commutative and associative operations ∧ and ∨ that satisfy the absorption laws:
a ∨ ( a ∧ b ) = a ; a ∧ ( a ∨ b ) = a ,
for all a , b ∈ L.
A lattice is:
- Distributive if a ∧ ( b ∨ c ) = ( a ∧ b ) ∨ ( a ∧ c ) for all a , b , c ∈ L.
- Bounded if there are elements ⊥ , ⊤ ⁡ ∈ L such that a ∨ ⊥ = a and a ∧ ⊤ ⁡ = a.
- Complemented if it is bounded and for every a ∈ L there is a ∗ ∈ L such that a ∧ a ∗ = ⊥ and a ∨ a ∗ = ⊤ ⁡.
A Boolean algebra is a complemented distributive lattice.
nothing: True

html: Proposition 1.4.3. Assuming that:
- L is a bounded lattice
- ≤ is the order induced by the operations in L (a ≤ b if a ∧ b = a)
Then ≤ is a partial order with least element ⊥, greatest element ⊤ ⁡, and for any a , b ∈ L, we have a ∧ b = inf ⁡ { a , b } and a ∧ b = sup ⁡ { a , b }. Conversely, every partial order with all finite infs and sups is a bounded lattice.
proof: Proof. Exercise. □
cloze1: True

html: Definition 1.4.4 (Heyting algebra). A Heyting algebra is a bounded lattice equipped with a binary operation ⇒ : H × H → H such that
a ∧ b ≤ c ⟺ a ≤ ( b ⇒ c )
for all a , b , c ∈ L.
A morphism of Heyting algebras is a function that preserves all finite meets, finite joins, and ⇒.
nothing: True

html: 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 → H, extended to the whole of L recursively by setting:
- v ( ⊥ ) = ⊥,
- v ( A ∧ B ) = v ( A ) ∧ v ( B ),
- v ( A ∨ B ) = v ( A ) ∨ v ( B ),
- v ( A → B ) = v ( A ) ⇒ 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 ( ∧ ⁡ Γ ) ≤ v ( A ) for all H-valuations v (written Γ ⊨ H A).
nothing: True

html: Lemma 1.4.7 (Soundness of Heyting semantics). Assuming that:
- H is a Heyting algebra
- v : L → H is a valuation
Then Γ ⊢ IPC A implies Γ ⊨ H A.
proof: Proof. By induction over the structure of the proof Γ ⊢ A.
- (Ax) As v ( ( ∧ ⁡ Γ ) ∧ A ) = v ( ∧ ) ∧ v ( A ) ≤ v ( A ) for any Γ and A.
- (∧-I) A = B ∧ C and we have derivations Γ 1 ⊢ B, Γ 2 ⊢ C, with Γ 1 , Γ 2 ⊆ Γ. By the induction hypothesis, we have v ( ∧ ⁡ Γ ) ≤ v ( ∧ Γ 1 ) ∩ v ( ∧ Γ 2 ) ≤ v ( B ) ∧ v ( C ) = v ( B ∧ C ) = v ( A ), i.e. Γ ⊨ H A.
- (→-I) A = B → C and so we must have Γ ∪ { B } ⊢ C. By induction hypothesis, we have v ( ∧ ⁡ Γ ) ∧ v ( B ) = v ( ∧ γ ∧ B ) ≤ v ( C ). By the definition of ⇒, this implies v ( ∧ ⁡ Γ ) ≤ [ v ( B ) ⇒ v ( C ) ] = v ( B → C ) = v ( A ), i.e. Γ ⊨ H A.
- (∨-I) A = B ∨ C and without loss of generality we have a derivation Γ ⊢ B. By the induction hypothesis we have v ( ∧ ⁡ Γ ) ≤ v ( B ), but v ( B ∨ C ) = v ( B ) ∨ v ( C ), and hence v ( B ) ≤ v ( B ∨ C ) = v ( A ).
- (∧-E) By the induction hypothesis, we have v ( ∧ ⁡ Γ ) ≤ v ( B ∧ C ) = v ( B ) ∧ v ( C ) ≤ v ( B ) , v ( B ).
- (→-E) We know that v ( A → B ) = ( v ( A ) ⇒ v ( B ) ). From v ( A → B ) ≤ v ( A ) ⇒ v ( B ), we derive v ( A ) ∧ v ( A → B ) ≤ v ( B ) by definition of ⇒. So if v ( ∧ ⁡ Γ ) ≤ v ( A → B ) and v ( ∧ ⁡ Γ ) ≤ v ( A ), then v ( ∧ ⁡ Γ ) ≤ v ( B ), as needed.
- (∨-E) By induction hypothesis: v ( A ∨ ∧ ⁡ Γ ) ≤ v ( C ), v ( B ∨ ∧ ⁡ Γ ) ≤ v ( C ) and v ( ∧ ⁡ Γ ) ≤ v ( A ∨ B ) = v ( A ) ∨ v ( B ). This last fact means that v ( ∧ ⁡ Γ ) ∧ ( v ( A ) ∨ v ( B ) ) = v ( ∧ Γ ). Now this is the same as ( v ( ∧ ⁡ Γ ) ∧ v ( A ) ) ∨ ( v ( ∧ Γ ) ∧ v ( B ) ) as Heyting algebras are distributive lattices (see Example Sheet 2), and this is ≤ v ( C ) by the first two inequalities of this paragraph.
- (⊥-E) If v ( ∧ ⁡ Γ ) ≤ v ( ⊥ ) = ⊥, then v ( ∧ ⁡ Γ ) = ⊥, in which case v ( ∧ ⁡ Γ ) ≤ v ( A ) for any A by minimality of ⊥ in H. □
nothing: True

html: 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 φ ∼ ψ when T , φ ⊢ Q ψ and T , ψ ⊢ Q φ;
- If ⋈ is a logical connective in the fragment Q, we set [ φ ] ⋈ [ ψ ] : = [ φ ⋈ ψ ] (should check well-defined: exercise).
nothing: True

html: Proposition 1.4.10. The Lindenbaum-Tarski algebra of any theory in IPC ∖ { → } is a distributive lattice.
proof: Proof. Clearly, ∧ and ∨ inherit associativity and commutativity, so in order for F IPC ∖ { → } ( T ) to be a lattice we need only to check the absorption laws:
[ φ ] ∨ [ φ ∧ ψ ] = [ φ ] ( α ) [ φ ] ∧ [ φ ∨ ψ ] = [ φ ] ( β )
Equation (α) is true since T , φ ⊢ I P C ∖ { → } φ ∨ ( φ ∧ ψ ) by (∨-I), and also T , φ ∨ ( φ ∧ ψ ) ⊢ IPC ∖ { → } φ by (∨-E). Equation (β) is similar.
Now, for distributivity: T , φ ∧ ( ψ ∨ χ ) ⊢ ( φ ∧ ψ ) ∨ ( φ ∧ χ ) by (∧-E) followed by (∨-E):
φ ∧ ( ψ ∨ χ ) | (∧-E)
φ ψ ∨ χ | (∨-E)
( φ ∧ ψ ) ∨ ( φ ∧ χ )
Conversely, T , ( ( φ ∧ ψ ) ∨ ( φ ∧ χ ) ) ⊢ φ ∧ ( ψ ∨ χ ) by (∨-E) followed by (∧-I). □

html: Lemma 1.4.11. The Lindenbaum-Tarski algebra of any theory relative to IPC is a Heyting algebra.
proof: Proof. We already saw that F IPC ( T ) is a distributive lattice, so it remains to show that [ φ ] ⇒ [ ψ ] : = [ φ → ψ ] gives a Heyting implication, and that F IPC ( T ) is bounded.
Suppose that [ φ ∧ [ ψ ] ≤ [ χ ], i.e. τ , φ ∧ ψ ⊢ IPC χ. We want to show that [ φ ] ≤ [ ψ → χ ], i.e. τ , φ ⊢ ( ψ → χ ). But that is clear:
φ [ ψ ] |
φ ∧ ψ | (hyp)
χ | (→-I, ψ)
ψ → χ
Conversely, if τ , φ ⊢ ( ψ → χ ), then we can prove τ , φ ∧ ψ ⊢ χ:
φ ∧ ψ | (∧-E)
φ ψ | (hyp)
ψ → χ ψ | (→-E)
χ
So defining [ φ ] ⇒ [ ψ ] : = [ φ → ψ ] provides a Heyting ⇒.
The bottom element of F IPC ( T ) is just [ ⊥ ]: if [ φ ] is any element, then T , ⊥ ⊢ IPC φ by ⊥-E.
The top element is ⊤ ⁡ : = [ ⊥ → ⊥: if φ is any proposition, then [ φ ] ≤ [ ⊥ → ⊥ ] via
φ [ ⊥ ] | (⊥-E)
⊥ |
⊥ → ⊥
□

html: 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: Proof. One direction is easy: if ⊢ IPC φ, then there is a derivation in IPC, thus ⊤ ⁡ ≤ 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 → F ( L ), p ↦ [ 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 ⊤ ⁡ → ⊤ ⁡ ⊢ IPC φ, hence ⊢ IPC φ. □
nothing: True

html: Proposition 1.4.13. If S is a poset, then the set T ( S ) = { U ⊆ S : U is a terminal segment of S } can be made into a Heyting algebra.
proof: Proof. Order the terminal segments by ⊆. Meets and joins are ∩ and ∪, so we just need to define ⇒. If U , V ∈ T ( S ), define ( U ⇒ V ) : = { s ∈ S : ( s ↑ ) ∩ U ⊆ V }.
If U , V , W ∈ T ( S ), we have
W ⊆ ( U ⇒ V ) ⟺ ( w ↑ ) ∩ U ⊆ V ∀ ⁡ w ∈ W ,
which happens if for every w ∈ W and u ∈ U we have w ≤ u ⟹ u ∈ V. But W is a terminal segment, so this is the same as saying that W ∩ U ⊆ V. □

html: Definition 1.4.14 (Kripke model). Let P be a set of primitive propositions. A Kripke model is a tuple ( S , ≤ , ⊩ ) where ( S , ≤ ) is a poset (whose elements are called “worlds” or “states”, and whose ordering is called the “accessibility relation”) and ⊩ ⊆ S × P is a binary relation (“forcing”) satisfying the persistence property: if p ∈ P is such that s ⊩ p and s ≤ s ′, then s ′ ⊩ p.
nothing: True

html: Definition 1.4.15 (Forcing relation). Let ( S , ≤ , ⊩ ) be a Kripke model for a propositional language. We define the extended forcing relation inductively as follows:
- There is no s ∈ S with s ⊩ ⊥;
- s ⊩ φ ∧ ψ if and only if s ⊩ φ and s ⊩ ψ;
- s ⊩ φ ∨ ψ if and only if s ⊩ φ or s ⊩ ψ;
- s ⊩ ( φ → ψ ) if and only if s ′ ⊩ φ implies s ′ ⊩ ψ for every s ′ ≥ s.
nothing: True

html: Definition 1.4.17 (Filter). A filter F on a lattice L is a subset of L with the following properties:
- F ≠ ∅
- F is a terminal segment of L (i.e., if f ≤ x and f ∈ F, then x ∈ F)
- F is closed under finite meets
nothing: True

html: Lemma 1.4.19. Assuming that:
- H a Heyting algebra
- v a H-valuation
Then there is a Kripke model ( S , ≤ , ⊩ ) such that v ⊨ H φ if and only if S ⊩ φ, for every proposition φ.
proof: 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 ) ∈ F for primitive propositions p.
We prove by induction that F ⊩ φ if and only if v ( φ ) ∈ F for arbitrary propositions.
For the implication case, say that F ⊩ ( ψ → ψ ′ ) and v ( ψ → ψ ′ ) = [ v ( ψ ) ⇒ v ( ψ ′ ) ] ∉ F. Let G ′ be the least filter containing F and v ( ψ ). Then
G ′ = { b : ( ∃ ⁡ f ∈ F ) ( f ∧ v ( ψ ) ≤ b ) } .
Note that v ( ψ ′ ) ∉ G ′, or else f ∧ v ( ψ ) ≤ v ( ψ ′ ) for some f ∈ F, whence f ≤ v ( ψ → ψ ′ ) and so v ( ψ → ψ ′ ) ∈ 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 ⊩ ( ψ → ψ ′ ) and G ′ (this G) contains F, we have that G ⊩ ψ ′. But then v ( ψ ′ ) ∈ G, contradiction.
This settles that F ⊩ ( ψ → ψ ′ ) implies v ( ψ → ψ ′ ) ∈ F.
Conversely, say that v ( ψ → ψ ′ ) ∈ F ⊆ G ⊩ ψ. By the induction hypothesis, v ( ψ ) ∈ G, and so v ( ψ ) ⇒ v ( ψ ) ∈ G (as F ⊆ G). But then v ( ψ ′ ) ≥ v ( ψ ) ∧ ( v ( ψ ) ⇒ v ( ψ ′ ) ) ∈ G, as G is a filter.
So the induction hypothesis gives G ⊩ ψ ′, as needed.
The cases for the other connectives are easy (∨ needs primality). So ( S , ≤ , ⊩ ) 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 ( φ ) ≠ ⊤ ⁡, 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. □
cloze1: True

html: Theorem 1.4.20 (Completeness of the Kripke semantics). Assuming that:
- φ a proposition
Then Γ ⊢ IPC φ if and only if for all Kripke models ( S , ≤ , ⊩ ), the condition S ⊩ Γ implies S ⊩ φ.
proof: 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 Hand v provides a Kripke model ( S , ≤ , ⊩ ) such that S ⊩ Γ, but S ⁄ ⊩ φ, contradicting the hypothesis on every Kripke model. □
nothing: True

html: Definition 1.5.1 (Double-negation translation). We recursively define the ¬ ⁡ ¬ ⁡-translation φ N of a proposition φ in the following way:
- If p is a primitive proposition, then p N : = ¬ ⁡ ¬ ⁡ p;
- ( φ ∧ ψ ) N : = φ N ∧ ψ N
- ( φ → ψ ) N : = φ N → ψ N
- ( φ ∨ ψ ) N : = ¬ ⁡ ( ¬ ⁡ φ N ∧ ¬ ⁡ ψ N )
- ( ¬ ⁡ φ ) N : = ¬ ⁡ φ N
nothing: True

html: Lemma 1.5.2. Assuming that:
- H a Heyting algebra
Then the map ¬ ⁡ ¬ ⁡ : H → H preserves ∧ and ⇒.
proof: Proof. Example Sheet 2. □
cloze1: True

html: Lemma 1.5.3 (Regularisation). Assuming that:
- H a Heyting algebra
Then
- (1) The subset H ¬ ⁡ ¬ ⁡ : = { x ∈ H : ¬ ⁡ ¬ ⁡ x = x } is a Boolean algebra;
- (2) For every Heyting homomorphism g : H → B into a Boolean algebra, there is a unique map of Boolean algebras g ¬ ⁡ ¬ ⁡ : H ¬ ⁡ ¬ ⁡ → B such that g ( x ) = g ¬ ⁡ ¬ ⁡ ( ¬ ⁡ ¬ ⁡ x ) for all x ∈ H.
proof: Proof.
- (1) Give H ¬ ⁡ ¬ ⁡ : = { x ∈ H : ¬ ⁡ ¬ ⁡ x = x } the inherited order, so that ∧, ⇒, ⊥ and ⊤ ⁡ (which are preserved by ¬ ⁡ ¬ ⁡) remain the same. We just need to define disjunctions in H ¬ ⁡ ¬ ⁡ properly.
Define a ∨ ¬ ⁡ ¬ ⁡ b : = ¬ ⁡ ¬ ⁡ ( a ∨ b ) in H. It is easy to show that this gives sup ⁡ { a , b } in H ¬ ⁡ ¬ ⁡ (as ¬ ⁡ ¬ ⁡ preserves order), so H ¬ ⁡ ¬ ⁡ is a Heyting algebra.
As every element of H ¬ ⁡ ¬ ⁡ is regular (i.e. ¬ ⁡ ¬ ⁡ x = x), it is a Boolean algebra (see Example Sheet 2).
- (2) Given a Heyting homomorphism g : H → B, where B is a Boolean algebra, define g ¬ ⁡ ¬ ⁡ : H → B as g H ¬ ⁡ ¬ ⁡. It clearly preserves ⊥ , ⊤ ⁡ , ∧ , ⇒, as those operations in H ¬ ⁡ ¬ ⁡ are inherited from H.
But we also have
g ¬ ⁡ ¬ ⁡ ( a ∨ ¬ ⁡ ¬ ⁡ b ) = g | H ¬ ⁡ ¬ ⁡ ( ¬ ⁡ ¬ ⁡ ( a ∨ b ) ) = ¬ ⁡ ¬ ⁡ ( g ( a ) ∨ g ( b ) ) = g ( a ) ∨ g ( b ) B is Boolean = g ¬ ⁡ ¬ ⁡ ( a ) ∨ g ¬ ⁡ ¬ ⁡ ( b )
Thus g ¬ ⁡ ¬ ⁡ is a morphism of Boolean algebras. Note that any x ∈ H provides an element ¬ ⁡ ¬ ⁡ x ∈ H ¬ ⁡ ¬ ⁡, since ¬ ⁡ ¬ ⁡ ¬ ⁡ ¬ ⁡ x = ¬ ⁡ ¬ ⁡ x in H. Additionally,
g ¬ ⁡ ¬ ⁡ ( ¬ ⁡ ¬ ⁡ x ) = g ( ¬ ⁡ ¬ ⁡ x ) = ¬ ⁡ ¬ ⁡ g ( x ) = g ( x )
for all x ∈ H (as g ( x ) is in a Boolean algebra).
Now, if h : H ¬ ⁡ ¬ ⁡ → B is a morphism of Boolean algebras with g ( x ) = h ( ¬ ⁡ ¬ ⁡ x ) for all x ∈ H, then h ( a ) = h ( ¬ ⁡ ¬ ⁡ a ) = g ( a ) = g ¬ ⁡ ¬ ⁡ ( a ) for all a ∈ H. So g ¬ ⁡ ¬ ⁡ is unique with this property. □
nothing: True

html: Theorem 1.5.4 (Glivenko’s Theorem). Assuming that:
- φ and ψ are propositions
Then ⊢ CPC φ → ψ if and only if ⊢ IPC ¬ ⁡ ¬ ⁡ φ → ¬ ⁡ ¬ ⁡ ψ.
proof: Proof.
- ⇒ If ⊢ CPC φ → ψ, then ⊤ ⁡ ≤ φ → ψ in F Bool ( L ) = F Heyt ( L ) ¬ ⁡ ¬ ⁡. As the inclusion i : F Heyt ( L ) ¬ ⁡ ¬ ⁡ → F Heyt ( L ) strictly preserves ≤ and →, it follows that i ( ⊤ ⁡ ) ≤ i ( φ → ψ ) = φ → ψ = ¬ ⁡ ¬ ⁡ ( φ → ψ ) as φ → ψ ∈ F Heyt ( L ) ¬ ⁡ ¬ ⁡ = ¬ ⁡ ¬ ⁡ φ → ¬ ⁡ ¬ ⁡ ψ
in F Heyt ( L ), so ⊢ IPC ¬ ⁡ ¬ ⁡ φ → ¬ ⁡ ¬ ⁡ ψ.
- ⇐ Obvious. □
nothing: True

html: Corollary 1.5.5. Assuming that:
- φ a proposition
Then ⊢ CPC φ if and only if ⊢ IPC φ N.
proof: Proof. Induction over the complexity of formulae. □
cloze1: True

html: Corollary 1.5.6. CPC is inconsistent if and only if IPC is inconsistent.
proof: Proof.
- ⇒ If CPC is inconsistent, then there is φ such that ⊢ CPC φ and ⊢ IPC ¬ ⁡ φ. But then ⊢ IPC ¬ ⁡ ¬ ⁡ φ and ⊢ IPC ¬ ⁡ φ, so ⊢ IPC ⊥.
- ⇐ Obvious. □
cloze1: True

html: Definition 2.1.1 (Partial recursive function). The class of recursive functions is the smallest class of partial functions of the form ℕ k → ℕ that contains the basic functions:
- Projections: Π i m : ( n 1 , … , n m ) ↦ n i;
- Successor: S + : n ↦ n + 1;
- Zero: z : n ↦ 0
and is closed under:
- Compositions: if g : ℕ k → ℕ is partial recursive and so are h 1 , … , h k : ℕ m → ℕ, then the function f : ℕ m → ℕ given by f ( n ¯ ) = g ( h 1 ( n ¯ ) , … , h k ( n ¯ ) ) is partial recursive.
- Primitive recursion: Given partial recursive functions g : ℕ m → ℕ and h : ℕ m + 2 → ℕ, the function f : ℕ m + 1 → ℕ defined by
{ f ( 0 , n ¯ ) : = g ( n ¯ ) f ( k + 1 , n ¯ ) : = h ( f ( k , n ¯ ) , k , n ¯ )
- Minimisation: Suppose g : ℕ m + 1 → ℕ is partial recursive. Then the function f : ℕ m → ℕ that maps n ¯ to the least n such that g ( n , n ¯ ) = 0 (if it exists) is partial recursive.
Notation: f ( n ¯ ) = μ n . g ( n , 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.
nothing: True

html: 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 ∗ ) ∗.
nothing: True

html: Lemma 2.1.4. Assuming that:
- M and N are λ-terms
Then
- (1)
FV ⁡ ( M ∗ ) ⊆ FV ⁡ ( M );
- (2)
M ↠ β M ∗;
- (3)
If M → β N, then N ↠ β M ∗.
proof: Proof. Induction over the structure of λ-terms. □
cloze1: True

html: Lemma 2.1.5. Takahashi translation preserves β-contraction:
( ( λ x . P ) Q ) ∗ ↠ β ( P [ x : = Q ] ) ∗ .
proof: Proof. By definition, ( ( λ x . P ) Q ) ∗ = P ∗ [ x : = Q ∗ ]. By induction over the structure of P, we can check that:
- If Qis 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 ] ) ∗. □

html: Lemma 2.1.6. Assuming that:
- M → β N
Then M ∗ ↠ β N ∗.
proof: 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 → β 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 → β 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 → β 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 → β 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 → β λ y . R, we get P 1 ∗ ↠ β λ y . R ∗. Thus
M ∗ = P 1 ∗ P 2 ∗ ↠ β ( λ y . R ∗ ) P 2 ∗ → β R ∗ [ y : = P 2 ∗ ] = N ∗ . □
cloze1: True

html: Corollary 2.1.7. If M ↠ β N, then M ∗ → β N ∗.
proof: Proof. Induction over the length of the chain M ↠ β N, using Lemma 2.1.6. □

html: Theorem 2.1.8. Assuming that:
- M β-reduces to N in n steps
Then N ↠ β M n ∗.
proof: 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 → β R → ( n − 1 ) β N. By induction hypothesis, N ↠ β R n − 1 ∗. Since M → β 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 ∗ . □
cloze1: True

html: 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: Proof. Say M → r β N 1, M → s β N 2. Without loss of generality, say r ≤ 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 ≤ s). So take N = M s ∗. □
nothing: True

html: 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
s ( s ( … ⁡ ( s ⏟ n times z ) … ⁡ ) .
nothing: True

html: Definition 2.1.12 (lambda-definability). A partial function f : ℕ k → ℕ is λ-definable if there is a λ-term F such that F c n 1 … c n k ≡ β c f ( n 1 , … , n k ).
nothing: True

html: 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 ∈ ℕ:
- A + c n c m ≡ β c n + m;
- A ∗ c n c m ≡ β c n m;
- A e c n c m ≡ β c n m if m > 0.
proof: Proof. We’ll show that A + c n c m ≡ β c n + m, and leave the rest to you.
First note that
c n s z = ( λ f . λ x . f n ( x ) ) s z ≡ β ( λ x . s n ( x ) ) z ≡ β s n ( z ) .
So:
A + c n c m = ( λ x . λ y . λ s . λ z . x s ( y s z ) ) c n c m ≡ β ( λ y . λ s . λ z . c n s ( y s z ) ) c m ≡ β λ s . λ z . c n s ( c m s z ) ) ≡ β λ s . λ z . s n ( s m z ) ≡ β λ s . λ z . s n ( s m z ) ≡ β λ s . λ z . s m + n ( z ) ≡ β c n + m □
nothing: True

html: 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 ) ≡ β P;
- (ii)
( if ⊥ then P else Q ) ≡ β Q.
proof: Proof. Just compute it! □
cloze1: True

html: Theorem 2.1.15 (Fixed Point Theorem). There is a λ-term Y such that, for all F:
F ( Y F ) ≡ β Y F .
proof: Proof. Define
Y = λ f . ( λ x . f ( x x ) ) λ x . f ( x x ) .
If we compute Y F, we get:
Y F = ( λ f . ( λ x . f ( x x ) ) λ x . f ( x x ) ) F ≡ β ( λ x . F ( x x ) ) λ x . F ( x x ) ≡ β F ( ( λ x . F ( x x ) ) ( λ x . F ( x x ) ) ) ≡ β F ( ( λ f . ( λ x . f ( x x ) ) λ x . f ( x x ) ) F ) ≡ β F ( Y F ) □
nothing: True

html: Corollary 2.1.16. Given a λ-term M, there is a λ-term F such that F ≡ β M [ f : = F ].
proof: Proof. Take F = Y λ f . M. Then
F ≡ β ( λ f . M ) Y ( λ f . M ) ≡ β ( λ f . M ) F ≡ β M [ f : = F ] . □

html: Lemma 2.1.18. The basic partial recursive functions are λ-definable.
proof: Proof. The i-th projection ℕ k → ℕ is definable by π i k : λ x 1 … λ 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! □

html: Lemma 2.1.19. The class of λ-definable functions is closed under composition.
proof: Proof. Say G is a λ-term defining g : ℕ k → ℕ, and that λ-terms H 1 , … , H k define h 1 , … , h k : ℕ m → ℕ. Then the composite map f : n ¯ ↦ g ( h 1 ( n ¯ ) , … , h k ( n ¯ ) ) is definable by the term
F : = λ x 1 … x m : ( G ( H 1 x 1 … x m ) … ( H k x 1 … x m ) )
by inspection. □

html: Lemma 2.1.20. The class of λ-definable functions is closed under primitive recursion.
proof: Proof. Suppose f : ℕ m + 1 → ℕ is obtained from h : ℕ m + 2 → ℕ and g : ℕ m → ℕ by primitive recursion.
f ( 0 , n ¯ ) : = g ( n ¯ ) f ( k + 1 , n ¯ ) : = h ( f ( k , n ¯ ) , k , n ¯ )
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 … x n ] ,
which acts on a pair [ c k , c f ( k , n ¯ ] by updating the iteration data. Then f ought to be definable by
F : = λ x . λ x 1 … x m . x T [ c 0 , G x 1 … x m ] π 2 .
Indeed,
F c k c n 1 … c n m ≡ β c k T [ c 0 , G c n 1 … c n m ] π 2 ≡ β T k [ c 0 , c g ( π ) ] π 2
by definition of c k, and since
T [ c k , c f ( k , π ) ] ≡ β [ S c k , H c f ( k , n ¯ ) c k c n 1 , … , c n m ] ≡ β [ c k + 1 , c h ( f ( k , n ¯ ) , k , n ¯ ) ]
we have
F c k c n 1 … c n m ≡ β T k ( [ c 0 , G c n 1 … c n m ] ) π 2 ≡ β c f ( k , n ¯ )
as needed. □

html: Lemma 2.1.21. The λ-definable functions are closed under minimisation.
proof: Proof. Suppose G λ-defines g : ℕ m + 1 → ℕ, and that f : ℕ m → ℕ is defined from g by minimisation: f ( n ¯ ) = μ k . g ( k , 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 ≡ β { ⊤ ⁡ if n = 0 ⊥ otherwise .
Now we want a term that, on input k, checks if g ( k , 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 … ⁡ λ x m . ( if zero? ⁡ ( g k x 1 … ⁡ x m ) then k else ( f ( g ( S k ) x 1 … ⁡ x m ) ) ) ,
and set
F : = λ x 1 … λ x m . ( Y Search ⁡ ) G c 0 x 1 … ⁡ x m .
Note that
( Y Search ⁡ ) G c k c n 1 … ⁡ c n m ≡ β Search ⁡ ( Y Search ⁡ ) G c k c n 1 … ⁡ c n m ,
which is
if zero? ⁡ ( G c k c n 1 … ⁡ c n m ) then c k else ( ( Y Search ⁡ ) G c k + 1 c n 1 … ⁡ c n m .
Thus
( Y Search ⁡ ) G c k c n 1 … ⁡ c n m ≡ β c k
if g ( k , n ¯ ) = 0 and
( Y Search ⁡ ) G c k c n 1 … ⁡ c n m ≡ β ( Y Search ⁡ ) G c k + 1 c 1 … ⁡ c m
otherwise, as g is λ-defined by G. Hence
F c n 1 … c n m ≡ β ( Y Search ⁡ ) G c 0 c n 1 … ⁡ c n m ≡ β c f ( n ¯ )
if f is defined on n ¯. So F λ-defines f. □

html: Lemma 2.1.22. Every partial recursive function is λ-definable.
proof: 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 ( 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 … c n k ⌉, then apply N.
If f is defined on n ¯, then F c n 1 … c n k has a β-normal form, and what we get is ⌈ c f ( n ¯ ) ⌉. Otherwise N ( ⌈ F c n 1 … c n k ⌉ ) is not defined.
We finish by going back from ⌈ c f ( n ¯ ) ⌉ to f ( n ¯ ). □

html: 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.
nothing: True

html: Theorem 2.1.24. Assuming that:
- f is λ-definable
Then f is partial recursive.
proof: 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 ( 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 … c n k ⌉, then apply N.
If f is defined on n ¯, then F c n 1 … c n k has a β-normal form, and what we get is ⌈ c f ( n ¯ ) ⌉. Otherwise N ( ⌈ F c n 1 … c n k ⌉ ) is not defined.
We finish by going back from ⌈ c f ( n ¯ ) ⌉ to f ( n ¯ ). □
cloze1: True

html: Definition 2.2.1 (Recursively enumerable). We say that X ⊆ ℕ is recursively enumerable if any of the following are true:
- (1)
X is the image of some partial recursive f : ℕ → ℕ;
- (2)
X is the image of some total recursive f : ℕ → ℕ;
- (3)
X = dom ⁡ f, for f a partial recursive f : ℕ → ℕ.
nothing: True

html: 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 ⊨ φ.
nothing: True

html: 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: Proof. By hypothesis, there is a total recursive f such that the axioms of T are exactly { f ( n ) : n ∈ ℕ }.
Idea: Replace f ( n ) with something equivalent, but with a shape that lets us retrieve n. Let
ψ n = ∧ k = 1 n ( f ( n ) )
for each n and
T ∗ : = { ψ n : n ∈ ℕ } .
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 ∧ ⁡ 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 ∉ T ∗. □
nothing: True

html: Lemma 2.2.5. The set of (Gödel numberings for) total recursive functions is not recursively enumerable.
proof: 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 : ℕ → ℕ 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. □

html: Definition 2.2.6 (Language of arithmetic). The language of arithmetic is the first-order language L PA with signature ( 0 , 1 , + , ⋅ , < ). The base theory of arithmetic is the L PA-theory PA − whose axioms express that:
- (1)
+ and ⋅ are commutative and associative, with identity elements 0 and 1 respectively;
- (2)
⋅ distributes over +;
- (3)
< is a linear ordering compatible with + and ⋅;
- (4)
∀ ⁡ x . ∀ ⁡ y . ( x < y → ∃ ⁡ z . x + z = y );
- (5)
0 < 1 ∧ ∀ ⁡ x . ( x > 0 → x ≥ 1 );
- (6)
∀ ⁡ x . x ≥ 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 , y ¯ ), the axiom
I φ : = ∀ ⁡ y ¯ . ( φ ( 0 , y ¯ ) ∧ ∀ ⁡ x . ( φ ( x , y ¯ ) → φ ( x + 1 , y ¯ ) ) → ∀ ⁡ x . φ ( x , y ¯ ) ) .
nothing: True

html: Definition 2.2.7 (Delta0-formula, Sigma1-formula). A Δ 0-formula of PA is one whose quantifiers are bounded, i.e. ∃ ⁡ x < t . φ ( x ) or ∀ ⁡ x < t . φ ( x ), where t is not free in φ and φ is quantifier free.
We say φ ( x ¯ ) is a Σ 1-formula if there is a Δ 0-formula ψ ( x ¯ , y ¯ ) such that
PA ⁡ ⊢ φ ( x ¯ ) ↔ ∃ ⁡ y ¯ . ψ ( x ¯ , y ¯ ) .
It is a Π 1-formula if there is a Δ 0-formula ψ ( x ¯ , y ¯ ) such that
PA ⁡ ⊢ φ ( x ¯ ) ⟺ ∀ ⁡ y ¯ . ψ ( x ¯ , y ¯ ) .
nothing: True

html: Definition 2.2.8 (beta indexing). The function β : ℕ 2 → ℕ is defined by β ( x , i ) = a % ( m ( i + 1 ) + 1 ), where a and m are the unique numbers such that x = ⟨ a , m ⟩.
nothing: True

html: Lemma 2.2.9 (Godel’s Lemma). Assuming that:
- M ⊨ PA ⁡
- n ∈ ℕ
- x 0 , … , x n − 1 ∈ M
Then there is u ∈ M such that M ⊨ ( u ) i = x i for all i < n.
proof: Proof.
- ⇐ Suppose that y = f ( x ¯ ) is Σ 1-definable by 𝜃 ( x ¯ , y ) : = ∃ ⁡ z ¯ . φ ( x ¯ , y , z ¯ ) (so φ ∈ Δ 0).
The function fi r s t ( x ) = ( μ y ≤ x ) . ∃ ⁡ z ≤ x . ( x = ⟨ y , z ⟩ ) is primitive recursive. By minimisation, the function
g ( x ¯ ) = μ z . ( ∃ ⁡ v , w ¯ ≤ z . ( z = ⟨ v , w ¯ ⟩ ∧ φ ( x ¯ , v , w ¯ ) ) )
is partial recursive.
Since ⟨ v , w ¯ ⟩ = ⟨ v , ⟨ w ¯ ⟩ ⟩ for tuples w ¯, we have that fi r s t ( ⟨ v , w ¯ ⟩ ) = v. Thus
fi r s t ( g ( x ¯ ) ) = { The least y such that ℕ ⊨ 𝜃 ( x ¯ , y ) if there is such y undefined otherwise
as for each x ¯ ∈ ℕ there is at most one y such that ℕ ⊨ 𝜃 ( x ¯ , y ). Now ℕ ⊨ 𝜃 ( x ¯ , y ) ⟺ y = f ( x ¯ ), so f ( x ¯ ) = fi r s t ( g ( x ¯ ) ) whenever defined. So f is partial recursive.
- ⇒ 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 , … , x k ) and g 1 ( z ¯ ) , … , g k ( z ¯ ) all have Σ 1-graphs, then the graph of the composite is given by:
∃ ⁡ u 1 , … , u k . ∧ i = 1 n ( u i = g i ( z ¯ ) ∧ y = f ( u 1 , … , u k ) ) .
This is equal to a Σ 1-formula, as those are closed under ∧ , ∃ ⁡. If f ( x ¯ , y ) is obtained by primitive recursion
{ f ( x ¯ , 0 ) = g ( x ¯ ) f ( x ¯ , y + 1 ) = h ( x ¯ , y , f ( x ¯ , y ) )
where g and h have Σ 1-graphs, then we can use Godel’s Lemma to show that the graph of f is given by
∃ ⁡ u , v . ( v = g ( x ¯ ) ∧ ( u ) 0 = v ∧ ( u ) y = z ∧ ∀ ⁡ i < y . ∃ ⁡ r , s . [ r = ( u ) i ∧ s = ( u ) i + 1 ∧ s = h ( x ¯ , i , r ) ] .
We do this by coding the sequence f ( x ¯ , 0 ) , f ( x ¯ , 1 ) , … , f ( 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 ∃ ⁡ t ¯ . ψ ( x ¯ , i , r , s , t ¯ ) with ψ ∈ Δ 0, then
∀ ⁡ i < y . ∃ ⁡ r , s [ r = ( u ) i ∧ s = ( u ) i + 1 ∧ s = h ( x ¯ , i , r ) ]
is equal to
∃ ⁡ w . ∀ ⁡ i < y . ∃ ⁡ r , s , t ¯ ≤ w ( r = ( u ) i ∧ s = ( u ) i + 1 ∧ ψ ( x ¯ , i , r , s , t ¯ ) )
as we can take w to be the maximum between suitable r , s , t ¯ with r = ( u ) i, s = ( u ) i + 1, ψ ( x ¯ , i , r , s , t ¯ ) with i = 0 , 1 , … , y − 1.
A similar argument gives closure under minimisation.
If f ( x ¯ ) is μ y . g ( x ¯ , y ) = 0 and the graph of g is definable by a Σ 1-formula, then the graph of f is definable by
∃ ⁡ u . ( ( u ) y = 0 ∧ ∀ ⁡ i < y . ( ( u ) i ≠ 0 ∧ ∀ ⁡ j ≤ y . ∃ ⁡ v ( v = g ( x ¯ , j ) ∧ v = ( u ) j ) ⏟ ( ∗ ) ) )
by using Godel’s Lemma to code g ( x ¯ , 0 ) , g ( x ¯ , 1 ) , … , g ( x ¯ , f ( x ¯ ) ).
Again, this is equal to a Σ 1-formula if the graph of g is given by ∃ ⁡ w ¯ φ ( x ¯ , y , z , w ¯ ) with φ ∈ Δ 0, then ( ∗ ) is equal in ℕ to
∃ ⁡ s . ∀ ⁡ j ≤ y . ∃ ⁡ v , w ¯ ≤ s . ( v = ( u ) j ∧ φ ( x ¯ , j , v , w ¯ ) ) . □
nothing: True

html: Theorem 2.2.10. Assuming that:
- f : ℕ k → ℕ a partial function
Then f is recursive if and only if there is a Σ 1-formula 𝜃 ( x ¯ , y ) such that y = f ( x ¯ ) ⟺ ℕ ⊨ 𝜃 ( x ¯ , y ).
proof: Proof.
- ⇐ Suppose that y = f ( x ¯ ) is Σ 1-definable by 𝜃 ( x ¯ , y ) : = ∃ ⁡ z ¯ . φ ( x ¯ , y , z ¯ ) (so φ ∈ Δ 0).
The function fi r s t ( x ) = ( μ y ≤ x ) . ∃ ⁡ z ≤ x . ( x = ⟨ y , z ⟩ ) is primitive recursive. By minimisation, the function
g ( x ¯ ) = μ z . ( ∃ ⁡ v , w ¯ ≤ z . ( z = ⟨ v , w ¯ ⟩ ∧ φ ( x ¯ , v , w ¯ ) ) )
is partial recursive.
Since ⟨ v , w ¯ ⟩ = ⟨ v , ⟨ w ¯ ⟩ ⟩ for tuples w ¯, we have that fi r s t ( ⟨ v , w ¯ ⟩ ) = v. Thus
fi r s t ( g ( x ¯ ) ) = { The least y such that ℕ ⊨ 𝜃 ( x ¯ , y ) if there is such y undefined otherwise
as for each x ¯ ∈ ℕ there is at most one y such that ℕ ⊨ 𝜃 ( x ¯ , y ). Now ℕ ⊨ 𝜃 ( x ¯ , y ) ⟺ y = f ( x ¯ ), so f ( x ¯ ) = fi r s t ( g ( x ¯ ) ) whenever defined. So f is partial recursive.
- ⇒ 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 , … , x k ) and g 1 ( z ¯ ) , … , g k ( z ¯ ) all have Σ 1-graphs, then the graph of the composite is given by:
∃ ⁡ u 1 , … , u k . ∧ i = 1 n ( u i = g i ( z ¯ ) ∧ y = f ( u 1 , … , u k ) ) .
This is equal to a Σ 1-formula, as those are closed under ∧ , ∃ ⁡. If f ( x ¯ , y ) is obtained by primitive recursion
{ f ( x ¯ , 0 ) = g ( x ¯ ) f ( x ¯ , y + 1 ) = h ( x ¯ , y , f ( x ¯ , y ) )
where g and h have Σ 1-graphs, then we can use Godel’s Lemma to show that the graph of f is given by
∃ ⁡ u , v . ( v = g ( x ¯ ) ∧ ( u ) 0 = v ∧ ( u ) y = z ∧ ∀ ⁡ i < y . ∃ ⁡ r , s . [ r = ( u ) i ∧ s = ( u ) i + 1 ∧ s = h ( x ¯ , i , r ) ] .
We do this by coding the sequence f ( x ¯ , 0 ) , f ( x ¯ , 1 ) , … , f ( 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 ∃ ⁡ t ¯ . ψ ( x ¯ , i , r , s , t ¯ ) with ψ ∈ Δ 0, then
∀ ⁡ i < y . ∃ ⁡ r , s [ r = ( u ) i ∧ s = ( u ) i + 1 ∧ s = h ( x ¯ , i , r ) ]
is equal to
∃ ⁡ w . ∀ ⁡ i < y . ∃ ⁡ r , s , t ¯ ≤ w ( r = ( u ) i ∧ s = ( u ) i + 1 ∧ ψ ( x ¯ , i , r , s , t ¯ ) )
as we can take w to be the maximum between suitable r , s , t ¯ with r = ( u ) i, s = ( u ) i + 1, ψ ( x ¯ , i , r , s , t ¯ ) with i = 0 , 1 , … , y − 1.
A similar argument gives closure under minimisation.
If f ( x ¯ ) is μ y . g ( x ¯ , y ) = 0 and the graph of g is definable by a Σ 1-formula, then the graph of f is definable by
∃ ⁡ u . ( ( u ) y = 0 ∧ ∀ ⁡ i < y . ( ( u ) i ≠ 0 ∧ ∀ ⁡ j ≤ y . ∃ ⁡ v ( v = g ( x ¯ , j ) ∧ v = ( u ) j ) ⏟ ( ∗ ) ) )
by using Godel’s Lemma to code g ( x ¯ , 0 ) , g ( x ¯ , 1 ) , … , g ( x ¯ , f ( x ¯ ) ).
Again, this is equal to a Σ 1-formula if the graph of g is given by ∃ ⁡ w ¯ φ ( x ¯ , y , z , w ¯ ) with φ ∈ Δ 0, then ( ∗ ) is equal in ℕ to
∃ ⁡ s . ∀ ⁡ j ≤ y . ∃ ⁡ v , w ¯ ≤ s . ( v = ( u ) j ∧ φ ( x ¯ , j , v , w ¯ ) ) . □
cloze1: True

html: Corollary 2.2.11. A subset A ⊆ ℕ k is recursively enumerable if and only if there is a Σ 1-formula ψ ( x 1 , … , x k ) such that, given x ¯ ∈ ℕ k, we have x ¯ ∈ A if and only if ℕ ⊨ ψ ( x ).
proof: Proof.
- ⇒ If A is recursively enumerable, then there is a recursive f such that A = dom ⁡ ( f ). Given x ¯ ∈ ℕ k, we thus have x ∈ A if and only if ℕ ⊨ ∃ ⁡ v . v = f ( x ¯ ). But ∃ ⁡ v . v = f ( x ¯ ) is equal to a Σ 1-formula by Theorem 2.2.10.
- ⇐ Conversely, if A is defined in ℕ by a Σ 1-formula ψ, define f ( x ¯ ) = 0 if ℕ ⊨ ψ ( x ¯ ), and f ( x ¯ ) ↑ otherwise. The graph of f is given by y = 0 ∧ ψ ( x ¯ ), which is Σ 1, and so f is recursive by Theorem 2.2.10. But A = dom ⁡ ( f ), so A is recursively enumerable. □
cloze1: True

html: Definition 2.2.12 (Representation of a total function). Let f : ℕ k → ℕ 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 , … , x k , y ) such that, for all n ¯ ∈ ℕ k:
- (a)
T ⊢ ∃ ⁡ ! y . 𝜃 ( n ¯ , y )
- (b)
If k = f ( n ¯ ), then T ⊢ 𝜃 ( n ¯ , k ̲ )
nothing: True

html: Lemma 2.2.13. Every total recursive function f : ℕ k → ℕ is Σ 1-represented in PA−.
proof: Proof. The graph of f is given by a Σ 1-formula by Theorem 2.2.10, say ∃ ⁡ z ¯ . φ ( x ¯ , y , z ¯ ) where φ ∈ Δ 0. Without loss of generality, we may assume that z ¯ is a single variable (for example, rewrite ∃ ⁡ z . ∃ ⁡ w ¯ < z . φ ( x ¯ , y , w ¯ )).
Let ψ ( x ¯ , y , z ) be the Δ 0-formula
φ ( x ¯ , y , z ) ∧ ∀ ⁡ u , v ≤ y + z . ( u + v < y + z → ¬ ⁡ φ ( x ¯ , u , v ) ) .
Then the Σ 1-formula 𝜃 ( x ¯ , y ) : = ∃ ⁡ z . ψ ( x ¯ , y , z ) represents f in PA−.
We show PA − ⊢ 𝜃 ( n ¯ , k ) first, where k = f ( n ¯ ). Note that k is the unique element of ℕ such that ℕ ⊨ ∃ ⁡ z . φ ( n ¯ , k , z ), as f is a function.
Take l to be the first natural number such that ℕ ⊨ φ ( n ¯ , k , l ). Then ℕ ⊨ ψ ( n ¯ , k , l ) too, whence ℕ ⊨ ∃ ⁡ z . ψ ( n ¯ , k , z ). But any Σ 1-sentence true in ℕ is true in any model of PA−(c.f. Example Sheet 4), so PA − ⊢ ∃ ⁡ z . ψ ( n ¯ , k , z ), i.e. PA − ⊢ 𝜃 ( n ¯ , k ).
To see that PA − ⊢ ∃ ⁡ ! y . 𝜃 ( n ¯ , y ), let l be the first number such that ℕ ⊨ φ ( n ¯ , k , l ), where k = f ( n ¯ ). Suppose a , b ∈ M ⊨ PA −, with M ⊨ ψ ( n ¯ , a , b ). We will show that a = k. Completeness settles the claim. Again, φ ( 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 ≤ k + l ∈ ℕ, so a , b ∈ ℕ (as ℕ is an initial segment of M). Now M ⊨ ψ ( n ¯ , a , b ) ∈ Δ 0, hence ℕ ⊨ ψ ( x ¯ , a , b ) and thus ℕ ⊨ ∃ ⁡ z . φ ( n ¯ , a , z ). Thus a = k as needed. □

html: Corollary 2.2.14. Every recursive set A ⊆ ℕ k is Σ 1-representable in PA−.
proof: Proof. The characteristic function χ A of A is total recursive, so χ A ( x ¯ ) = y is represented by some Σ 1-formula 𝜃 ( x ¯ , y ) in PA−. But then 𝜃 ( x ¯ , 1 ) represents A in PA−. □

html: 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 ↔ 𝜃 ( ⌈ G ⌉ ) .
Moreover, if 𝜃 is a Π 1-formula, then we can take G to be a Π 1-sentence.
proof: Proof. Define a total recursive function diag ⁡ this way: on input n ∈ ℕ, check if n = ⌈ σ ( x ) ⌉ is the Gödel numbering of some L PA ⁡-formula σ ( x ). If so, return ⌈ ∀ ⁡ y . ( y = n ̲ → σ ( y ) ) ⌉, else return 0.
As diag ⁡ is total recursive, it is Σ 1-represented in T by some δ ( x , y ). Consider the formula
ψ ( x ) : = ∀ ⁡ z . ( δ ( x , z ) → 𝜃 ( z ) ) .
Let n = ⌈ ψ ( x ) ⌉ and G : = ∀ ⁡ y . ( y = n ̲ → ψ ( y ) ). This makes G the sentence whose Gödel numbering is diag ⁡ ( ⌈ ψ ( x ) ⌉ ). It is obvious that T ⊢ G ↔ ψ ( n ̲ ), so we know that
α T ⊢ G ↔ ∀ ⁡ z . ( δ ( n ̲ , z ) → 𝜃 ( z ) ) . (α)
Now δ ( x , y ) represents diag ⁡ in T, and diag ⁡ ( n ) = ⌈ G ⌉ by construction, hence
β T ⊢ ∀ ⁡ z . ( δ ( n ̲ , z ) ↔ z = ⌈ G ⌉ ) . (β)
Combining (α) and (β), we get T ⊢ G ↔ 𝜃 ( ⌈ G ⌉ ) as needed.
Finally, note that if 𝜃 ∈ Π 1, then both ψ and G are equal to a Π 1-formula. □
nothing: True

html: 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 ¬ ⁡ φ)
- T contains all the Σ 1 and Π 1 sentences provable in PA−
Then there is a Π 1-sentence τ such that τ ∉ T and ¬ ⁡ τ ∉ T.
proof: Proof. Let 𝜃 ( x ) be a Σ 1-formula that represents T in PA−, so that
x ∈ T ⟺ PA − ⊢ 𝜃 ( x ) and x ∉ T ⟺ PA − ⊢ ¬ ⁡ 𝜃 ( x ) .
This exists since T is recursive. By the Diagonalisation Lemma, there is a Π 1-sentence τ such that PA − ⊢ τ ↔ ¬ ⁡ 𝜃 ( ⌈ τ ⌉ ).
If ⌈ τ ⌉ ∈ T, then PA − ⊢ 𝜃 ( ⌈ τ ⌉ ), and thus PA − ⊢ ¬ ⁡ τ. But then ⌈ ¬ ⁡ τ ⌉ ∈ T (as ¬ ⁡ τ ∈ Σ 1 and PA − proves it).
If ⌈ ¬ ⁡ τ ⌉ ∈ T, then τ ∉ T, so PA − ⊢ ¬ ⁡ 𝜃 ( ⌈ τ ⌉ ), and thus PA − ⊢ τ. As τ ∈ Π 1 and PA − ⊢ τ, we have ⌈ τ ⌉ ∈ T.
Since T is consistent, we can’t have either of ⌈ τ ⌉ or ⌈ ¬ ⁡ τ ⌉ in T. □
nothing: True

html: 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 ⁄ ⊢ ¬ ⁡ τ.
proof: 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 ⌈ σ ⌉ ∈ S by systematically searching through all proofs using the axioms in T, until we either find a proof of σ or a proof of ¬ ⁡ σ. 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 ⌈ τ ⌉ ∉ S and ⌈ ¬ ⁡ τ ⌉ ∉ S, contradicting Π 1-completeness of T. □
nothing: True

html: Definition 2.2.18 (Recursive structure). A (countable) L PA ⁡-structure M is recursive if there are total recursive functions ⊕ : ℕ 2 → ℕ, ⊗ : ℕ 2 → ℕ, a binary recursive relation ≼ ⊆ ℕ 2, and natural numbers n 0 , n 1 ∈ ℕ such that M ≅ ( ℕ , ⊕ , ⊗ , ≼ , n 0 , n 1 ) as L PA ⁡-structures.
nothing: True

html: 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: Proof. Say M ⊨ φ ( n ) for all standard n, but only them. Then M ⊨ φ ( 0 ) and M ⊨ ∀ ⁡ n . ( φ ( n ) → φ ( n + 1 ) ) holds (if φ ( n ) holds, then n and hence n + 1 are standard).
By I φ (induction), we conclude that M ⊨ ∀ ⁡ n . φ ( n ). But M is non-standard, so there is non-standard e ∈ M with φ ( e ), contradiction. □
nothing: True

html: Definition 2.2.20 (Canonically coded). A subset S ⊆ ℕ is canonically coded in a model M of PA ⁡ if there is c ∈ M such that
S = { n ∈ ℕ : ∃ ⁡ y . ( π n ̲ × y = c ) }
where n ̲ denotes the standard number n in the model.
nothing: True

html: Proposition 2.2.21. Assuming that:
- C ( u , x ) be a Δ 0-formula
- M a non-standard model of PA ⁡
Then given any b ~ ∈ M, there is c ∈ M such that, for any n ∈ ℕ:
M ⊨ ∃ ⁡ k < b ~ . C ( k , n ) ↔ ∃ ⁡ y . ( π n ̲ × y ) = c .
proof: Proof (sketch*). The following formula holds in ℕ for any n:
∀ ⁡ b . ∃ ⁡ a . ∀ ⁡ u < n . ( ∃ ⁡ k < b . C ( k , u ) ↔ ∃ ⁡ y . ( π u × 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 ⊨ ∀ ⁡ b . ∃ ⁡ a . ∀ ⁡ u < n ̲ . ( ∃ ⁡ k < b . C ( k , u ) ↔ ∃ ⁡ y . ( π u × y = a ) )
for any n ∈ ℕ. So by Lemma 2.2.19 there is a non-standard w ∈ M such that
M ⊨ ∀ ⁡ b . ∀ ⁡ a . ∀ ⁡ u < w . ( ∃ ⁡ k < b . C ( k , u ) ↔ ∃ ⁡ y . ( π u × y = a ) ) .
So for any b ~ ∈ M, there must be c ∈ M such that
M ⊨ ∀ ⁡ u < w . ( ∃ ⁡ k < b ~ . C ( k , u ) ↔ ∃ ⁡ y . ( π u × y = c ) ) .
Now w is non-standard, so M ⊨ n ̲ < w for all n ∈ ℕ. So for any b ~ ∈ M there is c ∈ M with
M ⊨ ∃ ⁡ k < b ~ . C ( k , n ) ↔ ∃ ⁡ y . ( π n ̲ × y = c )
for all n ∈ ℕ. □
cloze1: True

html: Definition 2.2.22 (Recursively inseparable). We say that subsets A , B ⊂ ℕ are recursively inseparable if they are disjoint and there is no recursive C ⊆ ℕ with B ∩ C = ∅ and A ⊆ C.
nothing: True

html: Proposition 2.2.23. There are recursively enumerable subsets A , B ⊆ ℕ that are recursively inseparable.
proof: Proof. Fix an effective enumeration { φ n : n < ω } of the partial recursive functions. Define A = { n ∈ ℕ : φ n ( n ) = 0 } and B = { n ∈ ℕ : φ n ( n ) = 1 }, which are clearly disjoint and are clearly recursively enumerable.
Suppose there is a recursive C with A ⊆ C and B ∩ C = ∅, and write χ C for its (total recursive) characteristic function. There must be u ∈ ℕ such that χ C = φ u, as χ C is total recursive.
Since χ C ( u ) ↓ and is either 0 or 1, we have either u ∈ A or u ∈ B.
If u ∈ A, then χ C ( u ) = φ u ( u ) = 0, so u ∉ C, contradicting A ⊆ C; so u ∈ B. But then χ C ( u ) = φ u ( u ) = 1, so u ∈ C, contradicting B ∩ C = ∅. Thus A and B are recursively inseparable. □

html: 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: Proof. Say A , B ⊆ ℕ are recursively enumerable and recursively inseparable. By Corollary 2.2.11, there are Σ 1-formulae ∃ ⁡ u . a ( u , x ) and ∃ ⁡ u . b ( u , x ) defining A and B respectively (so a and b are Δ 0-formulae).
Fix n ∈ ℕ. As the sets are disjoint, we have:
ℕ ⊨ ∀ ⁡ v < n . ∀ ⁡ w < n . ∀ ⁡ x < n . ¬ ⁡ ( a ( v , x ) ∧ b ( w , x ) ) .
As this sentence is Δ 0, it follows, for any non-standard M ⊨ PA ⁡ and n ̲ ∈ M that:
M ⊨ ∀ ⁡ v < n ̲ . ∀ ⁡ w < n ̲ . ∀ ⁡ x < n ̲ . ¬ ⁡ ( a ( v , x ) ∧ b ( w , x ) ) .
By Overspill, there is some non-standard c ∈ M such that
M ⊨ ∀ ⁡ v < c . ∀ ⁡ w < c . ∀ ⁡ x < x . ¬ ⁡ ( a ( v , x ) ∧ b ( w , x ) ) . (∗)
Now define X : = { n ∈ ℕ : ∃ ⁡ v < c . a ( v , n ̲ ) }. Note that:
- A ⊆ X: let n ∈ A, so that ℕ ⊨ a ( m , n ) for some m ∈ ℕ (a A is defined by ∃ ⁡ u . a ( u , x )). Then M ⊨ a ( m ̲ , n ̲ ), as a is Δ 0. Hence M ⊨ ∃ ⁡ v < c . a ( v , n ̲ ) as any standard m ̲ is below c as it is non-standard. But then n ∈ X.
- B ∩ X = ∅: if n ∈ B, then ℕ ⊨ b ( m , n ) for some m, so arguing as before we get M ⊨ ∃ ⁡ w < c . b ( w , n ̲ ). By (∗), we can deduce M ⊨ ¬ ⁡ ∃ ⁡ v < c . a ( v , n ̲ ). So n ∉ 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. □
cloze1: True

html: Theorem 2.2.25 (Tennenbaum). Assuming that:
- M = ( M , ⊕ , ⊗ , ≼ , n 0 , n 1 ) a countable non-standard model of PA ⁡
Then ⊕ is not recursive.
proof: 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 ∈ M that canonically codes a non-recursive subset X = { n : M ⊨ ∃ ⁡ y . ( π n ̲ × y = c ) } ⊆ ℕ.
As PA ⁡ proves that
π n ̲ × x = x + ⋯ + x ⏟ π n times ,
we have that
π n ̲ × y = y + ⋯ + y ⏟ π n times
for all y ∈ M. So n ∈ X if and only if there is d ∈ M such that
c = d ⊕ ⋯ ⊕ d ⏟ π n times .
Suppose ⊕ is recursive. Then we can can through ℕ (which is M) and look for some d ∈ M that realises the disjunction of:
{ c = x ⊕ ⋯ ⊕ x ⏟ π n x ’s c = x ⊕ ⋯ ⊕ x ⏟ π n x ’s ⊕ 1 ⋯ c = x ⊕ ⋯ ⊕ x ⏟ π n x ’s ⊕ 1 ⊕ ⋯ ⊕ 1 ⏟ π n − 1 ones
As ⊕ 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 ∈ M with v ≠ 0, there are unique q , r ∈ M such that r ≼ v and u = ( v ⊗ q ) ⊕ r.
- PA ⁡ ⊢ ∀ ⁡ x . ( x < π 1 ↔ ( x = 0 ∧ x = 1 ∧ ⋯ ∧ x = ( 1 + ⋯ + 1 ) ) ;
Combining these, we get that division of c by π n ̲ in M leaves a unique quotient d ∈ M, and remainder r ≼ π n ̲, which is either 0 or 1 or 1 ⊕ 1 or …or 1 ⊕ 1 ⊕ ⋯ ⊕ 1 (π n − 1 times); i.e. one of the disjunctions from before.
Now we see that X is recursive: if our search provides d such that
M ⊨ c = d ⊕ ⋯ ⊕ d ⏟ π n times ,
then n ∈ X, and if the search gives d satisfying one of the other disjunctions, then n ∉ X.
This contradicts the choice of X, so ⊕ can’t be recursive. □
nothing: True