Page 79 - Textos de Matemática Vol. 40

2.2. Name induction 67 Since the last line is an instance of (Acc.1) of Theorem 2.2.2, this axiom is
verified. In the same way, (IDacc.2)N follows from (Acc.2): 1
[(∀x.(∀y.φ(x, y) → ψ(y)) → ψ(x)) → ∀x.Pφ(x) → ψ(x)]N
↔ (∀x ∈˙ nat.(∀y ∈˙ nat.φN (x, y) → ψN (y)) → ψN (x))
→ ∀x ∈˙ nat.Acc(nat, tφN , x) → ψN (x)
↔ Closed(nat, tφN , ψN ) → ∀x.Acc(nat, tφN , x) → ψN (x).
The last line is an instance of (Acc.2), and we have finished the embedding of IDacc . ⊣
2.2.4 Modelling NEM in ID1
In this Section, we embed NEM within the theory ID1 of non-iterated inductive definitions.
In [Fef75], Feferman presents an inductive model construction for explicit mathematics. Beeson shows in [Bee85] that for the system EETJ + (LEM-IN) this construction may be carried out in the theory ID1, cf. also [Mar94, MS98].
In fact, we use Beeson’s formalization for the analysis of NEM using, in addition, the induction principle of ID1 to verify name induction (LEM-IR). The only differences are the adaption to the finite axiomatization of elementary com- prehension and the (trivial) verification of uniqueness of generators (LEM-UG) which was not part of the original formulation of EETJ.
We start with a standard interpretation ·∗ of the applicative structure using the relation App(x, y, z) := {x}(y) ≃ z in the sense of ordinary recursion, cf. [FJ93]. Here, the constants of LEM are interpreted by numerals of LPA coding appropriate number-theoretic functions satisfying the axioms of EETJ. With respect to the generators we have to choose numerals according to the following codes which will be used for the interpretation of the type structure:
• ⟨1⟩ codes the type of numerals,
• ⟨2⟩ codes the type of pairs with identical elements,
• ⟨3, a⟩ codes the complement of the type coded by a,
• ⟨4, a, b⟩ codes the intersection of the two types coded by a and b,
• ⟨5, a⟩ codes the domain of a function given as a type of ordered pairs coded by a
• ⟨6,f,a⟩ codes the inverse images of f, i.e., the type of all individuals x with fx is an element of the type coded by a,
• ⟨7, a, f⟩ codes the join of f over the type coded by a.
1