Page 70 - Textos de Matemática Vol. 40

58 Chapter 2. Explicit Mathematics
As additional atomic formulae of LEM we have s ∈ U and R(s,U). The formula R(s,U) is used to express that the individual s represents the type U orisaname ofU.
The formulae of LEM (φ, ψ, . . .) are built up from the atomic formulae by use of the usual propositional connectives and quantification in both sorts, over individuals as well as over types.
The following table contains a list of useful abbreviations:
U⊂V := U=V := s∈˙ t := U∈V := ∃x ∈˙ s.φ(x) := ∀x ∈˙ s.φ(x) := s=˙ t := s ⊂˙ t := R(s) :=
∀x.x∈U →x∈V, U⊂V∧V⊂U, ∃X.R(t,X)∧s∈X, ∃x.R(x,U)∧x∈V,
∃x.x ∈˙ s ∧ φ(x),
∀x.x ∈˙ s → φ(x), ∃X.R(s,X)∧R(t,X), ∃X,Y.R(s,X)∧R(t,Y)∧X⊂Y, ∃X.R(s,X).
The vector notation U⃗ and ⃗s is sometimes used to denote finite sequences of type variables U1,...,Um and individual terms s1,...,sn, respectively, whose lengths are given by the context. For example, for U⃗ = U1, . . . , Un and ⃗s = s1,...,sn we write:
R(⃗s,U⃗) := R(s1,U1)∧···∧R(sn,Un), R(⃗s) := R(s1)∧···∧R(sn).
The axioms. Our definition of EETJ, which provides a framework for explicit elementary types with join, is based on a finite axiomatization of ele- mentary comprehension. This approach is essential for the formulation of name induction below. In contrast, the original definition of EETJ employs an infinite axiom schema. A theorem of Feferman and Ja¨ger [FJ96] shows that this schema is derivable from the finite axiomatization.
In contrast to the logic of partial terms which is used for the first order part, we use classical logic for the second order part.
The nonlogical axioms of EETJ can be divided into the following groups. I. Applicative axioms. The axioms of BON.
II. Explicit representation and equality. The following axioms state that each type has a name, that there are no homonyms and that R respects the extensional equality of types.
(1) ∃xR(x,U),
(2) R(a,U)∧R(a,V)→U =V, (3) U = V ∧ R(s, U ) → R(s, V ).