Page 95 - Textos de Matemática Vol. 40

2.3. Universes in explicit mathematics 83
(3) c = dom(b),
(4) ∃f.c = inv(f, b),
(5) ∃f.c=j(b,f),
(6) ∃x,y,f.c=j(x,f)∧(x,y)∈˙ j(la,λz.z)∧b=fy.
Then we set
Remember that the subformula (x, y) ∈˙ j(l a, λz.z) in clause (6) is equivalent to
x∈˙ la∧y∈˙ x. Hence(6)isthesameasthemorefamiliar ∃x,y,f.c=j(x,f)∧x∈˙ la∧y∈˙ x∧b=fy,
saying that b is one of the “predecessors” of c in the case that c is generated by join. The name a itself is considered as an urelement of the least universe containing a; therefore we have the condition c ̸= a in the definition of b `a c for ruling out the possibility that a has `a predecessors.
The candidates for the least universe containing a are a itself, the constants nat as well as id and all names b with at least one element before b and all such belonging to l a,

Cand(a, b) :=
b`a c:=b∈˙ la∧c∈˙ la∧c̸=a∧Bef(a,b,c).
(b = a ∨ b = nat ∨ b = id) ∨ (∃x.Bef(a,x,b)∧∀x.Bef(a,x,b)→x∈˙ la).
All other individuals cannot belong to the least universe containing a. Applying inductive generation, this can be achieved by postulating that the corresponding accessibility relation is reflexive on the non-candidates. A candidate, on the other hand, goes into the intended inductively generated type whenever all its `a predecessors are elements of this type.
¿From Lemma 2.1.2 about modified elementary comprehension, we con- clude that, for every name a, there exists a type coding the intended accessibility relation,
Ar(a):={(x,y):(x=y∧¬Cand(a,y))∨(x`a y∧Cand(a,y))}.
This Lemma also implies that in EETJ, there is a closed individual term ar of LEM which uniformly describes this assignment of the type Ar(a) to the name a, i.e., EETJ proves
R(a) → R(ar a, Ar(a)).
We finish the uniform construction of the least universe containing the name a in T0 + (Lim) + (LEM-UG) by carrying through inductive generation on the type with name l a along the relation coded by Ar(a),
lst := λz.i (l z, ar z).