Page 72 - Textos de Matemática Vol. 40

60 Chapter 2. Explicit Mathematics
(1) r0 ̸= r1,
(2) ∀x.sx̸=nat∧sx̸=id,
(3) ∀x,y.sx=ty → s=t∧x=y.
2.1.2 Elementary comprehension.
An LEM formula φ is called elementary if it contains neither the relation symbol R nor bound type variables. In the original formulation of explicit mathematics, elementary comprehension is not dealt with by a finite axiomatization, but directly as an infinite axiom schema. According to a theorem in Feferman and Ja¨ger [FJ96], reformulated in Lemma 2.1.1 below, this schema of uniform elementary comprehension is provable from our finite axiomatization. Join is not needed for this argument.
Lemma 2.1.1 (Elementary comprehension). Let φ be an elementary LEM formula with no (distinct) individual variables other than z1 , . . . , zm+1 and no (distinct) type variables other than Z1 , . . . , Zn . Then there exists a closed individual term t of LEM, depending on φ, such that EETJ proves for all individual terms ⃗a = a1,...,am, ⃗b = b1,...,bn and type terms S⃗ = S1,...,Sn that:
1. R(⃗b,S⃗) → R(t(⃗a,⃗b)),
2. R(⃗b,S⃗) → ∀x.x∈˙ t(⃗a,⃗b)↔φ[x,⃗a,S⃗].
Informally, we will write {x : φ(x)} for the collection of all individuals c satisfying φ(c). Using this notation, the Lemma expresses that, for elementary formulae φ[u, ⃗y, Y⃗ ], the following holds:
1. {x:φ[x,⃗a,S⃗]}isatype,
2. there is a name t(⃗a,⃗b) for this type which is given uniformly in the indi-
vidual parameters and the names of the type parameters.
Sometimes, however, this formulation of elementary comprehension is too
restricted. Below, we therefore present a modified form. Before doing this, however, we introduce some further convenient shorthand notations.
Let U⃗ = U1,...,Un and ⃗s = s1,...,sn be sequences of type variables and individual terms of LEM, respectively, and let φ(U⃗ ) be an elementary LEM formula. Then we write φ(⃗s) for the LEM formula which results from φ(U⃗ ) by replacing for i = 1,...,n each occurrence of t ∈ Ui by t ∈˙ si. In addition, given a sequence ⃗r = r1, . . . , rm of individual terms of LEM, then ⃗r(⃗s) stands for the sequence of individual terms r1(⃗s), . . . , rm(⃗s) of LEM.
Lemma 2.1.2 (Modified elementary comprehension). Let φ be an elementary LEM formula with no (distinct) individual variables other than z1 , . . . , zm+1 and