Page 81 - Textos de Matemática Vol. 40

2.2. Name induction 69
CIn(ψ, u, z) is the disjunction of the following clauses: • z=⟨0⟩,
• z=⟨1⟩∧∃y.u=⟨y,y⟩,
• ∃x.z=⟨2,x⟩∧ψ0(x)∧ψ2(u,x),
• ∃x,y.z=⟨4,x,y⟩∧ψ0(x)∧ψ0(x)∧ψ1(u,x)∧ψ1(u,y),
• ∃x.z=⟨5,x⟩∧ψ0(x)∧∃v.ψ1(⟨u,v⟩,x),
• ∃f,x.z=⟨6,f,x⟩∧ψ0(x)∧ψ1({f}(u),x),
• ∃f,x.z=⟨7,x,f⟩∧ψ0(x)∧(∀y.¬ψ2(y,x)→ψ0({f}(y)))∧
∃v, w.u = ⟨v, w⟩ ∧ ψ1(v, x) ∧ ψ1(w, {f}(v)).
The defining clauses for CIn are analogous, also containing positive occurrences of ψ only.
Without the leastness property for the fixed point defined by φ we cannot prove that In and In are complementary. Hence, for embedding EETJ+(LEM-IN) within ID1 one has to make use of Aczel’s trick of sorting out all codes a for types where In(·,a) is not the complement of In(·,a). However, in ID1 the leastness condition allows for a direct proof that In and In are complements, cf. [Bee85].
Lemma 2.2.4. ID1 ⊢ Typ(y) → ∀x.In(x, y) ↔ ¬In(x, y).
Theorem 2.2.5. NEM can be embedded within ID1.
Proof. According to the arguments above, we can define an interpretation ·⋆ from LEM in the language of ID1. With the results for EETJ, cf. Theorem 2.1.3, it only remains to check the principle of name induction,
(LEM-IR) (∀x.C(χ, x) → χ(x)) → ∀x.R(x) → χ(x). This can be derived from the leastness principle for Pφ
(∀z.φ(ψ, z) → ψ(z)) → ∀z.Pφ(z) → ψ(z) by choosing a formula ψ(z) so that
ψ(⟨0, x⟩) ↔ ψ(⟨1, ⟨x, y⟩⟩) ↔ ψ(⟨2, ⟨x, y⟩⟩) ↔
ψ(z) ↔
χ⋆ (x),
In(x, y),
In(x, y),
0 = 0 for every other argument z.
Starting from the premiss [∀x.C(χ, x) → χ(x)]⋆ we obtain (∀z.φ(ψ, z) → ψ(z)): assume φ(ψ, z) holds with z = ⟨0, x⟩ for some x. Then we get CTyp(ψ, x) which