Page 75 - Textos de Matemática Vol. 40

2.2. Name induction 63
(1) ∀x.R(co(x)) → R(x),
(2) ∀x,y.R(int(x,y))→R(x)∧R(y),
(3) ∀x.R(dom(x)) → R(x),
(4) ∀f,x.R(inv(f,x))→R(x),
(5) ∀f,x.R(j(x,f))→R(x)∧∀y∈˙ x.R(fy).
To show Str(R) in NEM, we first note that the closure of the names under condition C is guaranteed by the type existence axioms of EETJ:
EETJ ⊢ C(R, x) → R(x). Lemma 2.2.1. NEM ⊢ Str(R).
Proof. The proof is straightforward, using (LEM-IR) for the formula C(R, x), i.e., we have
(∀x.C(C(R, x), x) → C(R, x)) → ∀x.R(x) → C(R, x).
The premiss follows immediately from the preceding remark and the fact that φ occurs only positively in C(φ, x). From the consequence ∀x.R(x) → C(R, x) we get the required conclusion Str(R) by substituting the different names. For example, for clause (5) we have
R(j(x,f)) → C(R,j(x,f))
→ ∃g,z.j(x,f)=j(z,g)∧R(z)∧∀y∈˙ z.R(gy) → ∃g,z.x=z∧f =g∧R(z)∧∀y∈˙ z.R(gy) → R(x)∧∀y∈˙x.R(fy).
For this argument, the uniqueness of generators (LEM-UG) is essential. ⊣ 2.2.2 Accessible parts in NEM
For the proof-theoretic analysis of NEM, the crucial property is the possibility
of defining accessible parts. This will be used in the next Section to embed the
theory IDacc within NEM. 1
Let us introduce the following abbreviation:
Closed(a, b, φ) := ∀x ∈˙ a.(∀y ∈˙ a.(y, x) ∈˙ b → φ(y)) → φ(x).
If b is a name for a binary relation, then Closed(a, b, φ) expresses that φ holds for all elements c ∈˙ a if it holds for all predecessors of c in a with respect to the relation named by b.
Using this abbreviation we can state the following Proposition which is the
essential step of the embedding of IDacc. 1