Page 78 - Textos de Matemática Vol. 40

66 Chapter 2. Explicit Mathematics This is just the premiss of name induction for ψφ(a,b,y) and we get from
(LEM -IR )
∀y.R(y) → ψφ(a, b, y). By the definition of ψφ(a, b, y), this is
∀y.R(y) → ∀x.Acc(a, b, x) ∧ f (a, b, x) = y → φ(x).
Since the assumption Acc(a,b,x) implies R(f(a,b,x)), we may choose y as f (a, b, x) and all premisses are satisfied. Therefore we finally obtain the re-
quired result φ(x).
⊣
This proof follows essentially the corresponding proof of Theorem 2.3.13 below, where the principle of inductive generation is verified in the presence of universes.
2.2.3 Modelling IDacc in NEM 1
Using the embedding ·N of PA within EETJ we know that LPA formulae are trans- lated into elementary formulae of LEM. Thus, by elementary comprehension we get for every binary formula φ(x,y) of LPA a name tφN for the corresponding type, i.e., EETJ proves that tφN is a name for {(x, y)|N(x) ∧ N(y) ∧ φN (x, y)}. These names will be employed in the proof of the following Theorem to represent the binary relations which are used in the definition of IDacc.
Theorem 2.2.3. There exists a translation ·N from LID into LEM such that IDacc ⊢φ ⇒ NEM⊢φN
for all LID formulae φ.
Proof. To interpret IDacc in NEM we extend the translation ·N by setting
[Pφ(x)]N := Acc(nat,tφN ,x),
where Acc(x,y,z) is defined as in Theorem 2.2.2. Then the proof is done by
induction on the length of the derivation of IDacc ⊢ φ. In addition to the 1
embedding of PA within EETJ, we only need to check the axioms for the new predicate symbols. The translation of (IDacc.1) reads as
[∀x.(∀y.φ(x, y) → Pφ(y)) → Pφ(x)]N
↔ ∀x ∈˙ nat.(∀y ∈˙ nat.φN (x, y) → Acc(nat, tφN , y)) → Acc(nat, tφN , x)
↔ Closed(nat, tφN , Acc(nat, tφN , ·)).
1
1
1
1