Page 74 - Textos de Matemática Vol. 40

62 Chapter 2. Explicit Mathematics
As related work we can refer to Martin-Lo¨f’s type theory. There, our induction principle corresponds to certain elimination rules which have first been considered by Palmgren and later by Rathjen, also in connection with universes, [Pal98, GR94].
Studer remarked that in type systems dealing with record or object types the concept of structural rule is important. Simplifying, we may say that these rules rely on the assumption that the universe of types consists of record or ob- ject types only, cf. e.g., [AC96]. Name induction may be seen as a generalization of this idea since it allows us to prove that the only types that exist are those which are created by the generators.
2.2.1 The theory NEM
In order to state the formal definition of name induction, we introduce as aux- iliary notation the closure condition C(φ,a) as the disjunction of the following formulae:
(1) a=nat∨a=id,
(2) ∃x.a = co(x) ∧ φ(x),
(3) ∃x,y.a=int(x,y)∧φ(x)∧φ(y),
(4) ∃x.a = dom(x) ∧ φ(x),
(5) ∃f,x.a=inv(f,x)∧φ(x),
(6) ∃f,x.a=j(x,f)∧φ(x)∧∀y∈˙ x.φ(fy).
The schema of name induction is now given by
(LEM-IR) (∀x.C(φ, x) → φ(x)) → ∀x.R(x) → φ(x),
for arbitrary formulae φ(x) of LEM.
The theory NEM of explicit mathematics with name induction consists of
the axioms of EETJ plus (LEM-UG), (LEM-IN) and (LEM-IR).
Name strictness. This notion is analogous to the strictness of definedness,
implemented in the logic of partial terms, and the N-strictness for the natural numbers, discussed above in Section 1.7.
Considering the predicate R in EETJ, we see that names are built up by the use of the generators nat, id, co, int, dom, inv, and j. However, there is no restriction on whether other terms may belong to R as well. For example, if co(a) is a name, then in general there is no need for a being a name, too.
As a first consequence of (LEM-IR), we prove name strictness which says that the (appropriate) arguments of generators of names are names, too. This is represented by the conjunction Str(R) of the following clauses: