Page 71 - Textos de Matemática Vol. 40

2.1. Explicit mathematics 59 III. Basic type existence axioms. In the following we provide a finite axioma-
tization of uniform elementary comprehension plus join.
Natural numbers
R(nat) ∧ ∀x(x ∈˙ nat ↔ N(x)). Identity
R(id) ∧ ∀x(x ∈˙ id ↔ (∃y)(x = (y, y))). Complements
R(a) → R(co(a)) ∧ ∀x(x ∈˙ co(a) ↔ x ∈/˙ a). Intersections
R(a)∧R(b) → R(int(a,b))∧∀x(x∈˙ int(a,b)↔x∈˙ a∧x∈˙ b). Domains
R(a) → R(dom(a)) ∧ ∀x(x ∈˙ dom(a) ↔ ∃y((x, y) ∈˙ a)). Inverse images
R(a) → R(inv(a,f))∧∀x(x∈˙ inv(a,f)↔fx∈˙ a). Joins
R(a)∧(∀x∈˙ a)R(fx) → R(j(a,f))∧Σ(a,f,j(a,f)).
In this last axiom, the formula Σ(a, f, b) expresses that b names the disjoint
union of f over a, i.e.,
Σ(a,f,b) := ∀x(x∈˙ b↔∃y∃z(x=(y,z)∧y∈˙ a∧z∈˙ fy)).
Considering the axioms for R, intuitively, one may look at a name of a type as its characteristic function. This view illustrates best the intensional character of the names in contrast to the extensional one of the types. Alternatively, Marzetta gave an interpretation of R(t,X) based on the idea that “t is a G¨odel number of an arithmetical formula, which defines the type X”. This interpretation involves a formalization of the syntax (“G¨odelization”) which is given in [Mar94, Section 3.2.3].
Uniqueness of generators. Sometimes, we also want additional axioms which guarantee that different generators create different names. This can be achieved by adding, for example, axioms of the following kind:
Uniqueness of generators with respect to LEM is given by the collection (LEM-UG) of the following axioms for all syntactically different generators r0 and r1 and arbitrary generators s and t of LEM: