Page 73 - Textos de Matemática Vol. 40

2.2. Name induction 61
no (distinct) type variables other than Z1,...,Zn, and let ⃗s = s1,...,sn be a sequence of closed individual terms of LEM. Then there exists a closed indi- vidual term t of LEM, depending on φ and ⃗s, such that EETJ proves for all ⃗a = a1,...,am:
1. R(⃗s(⃗a)) → R(t(⃗a)),
2. R(⃗s(⃗a)) → ∀x.x ∈˙ t(⃗a) ↔ φ[x,⃗a,⃗s(⃗a)].
Several results concerning the ontology of names in explicit mathematics, including the undefinability of strong power types and a form of Rice’s theorem for type, may be found in Cantini and Minari [CM99], Ja¨ger [J¨ag97], Jansen [Jan97], and Minari [Min99].
2.1.3 Proof theory of EETJ.
In the context of explicit mathematics it is natural to consider, next to the scheme of formula induction (LEM-IN) for arbitrary formulae, an induction axiom restricted to types:
(T-IN) ∀X.0∈X∧(∀x:N.x∈X→x′ ∈X) → ∀x:N.x∈X.
The proof theory of EETJ is well-known and due to Feferman [Fef79], cf.
also [Bee85, Mar94, Str01].
Theorem 2.1.3. We have the following proof-theoretic equivalences: 1. EETJ + (T-IN) ≡ PA.
2. EETJ + (LEM-IN) ≡ ID1.
It is worth noting that these proof-theoretic equivalences can actually be established by interpretations. In particular, there is a translation ·N of the language of Peano arithmetic into the applicative language, which translates the formulae of PA into elementary formulae of LEM.
2.2 Name induction
In this Section we show that the addition of name induction to the theory EETJ + (LEM-IN) yields a theory proof-theoretically equivalent to ID1.
The principle of name induction expresses that names of types can be built by use of generators only, i.e., that the naming relation R is, so to speak, least. Considering names as intensional representations of sets, we get an intensional version of ∈ induction.
The Section on name induction is based on [KS00].