Filter
Top Products
5.6. CLASSICAL AXIOMS 55
∀x. P (x) ⇒ P(εx. P(x))
The intuitive reading of εx. P(x) is ‘some x such that P(x)’, which is an
invaluable idiom when expressing some mathematical assertions. (Note that
if there isn’t anything satisfying P (x), then εx. P(x) is still well-defined, but
one can’t prove any interesting properties of it.) However the above axiom
isn’t just an innocent convenience: it is a form of the Axiom of (global)
Choice; since P can contain other variables, one can pass from ∀x. ∃y. P [x, y]
to ∀x. P[x, εy. P [x, y]]. Rather surprisingly, it also makes the logic classical,
i.e. allows us to prove the theorem ∀p. p ∨ ¬p; see Beeson (1984) for the
proof we use.
• Finally we introduce a new type ind of ‘individuals’, and add an axiom of
infinity, asserting that the type ind is infinite. The Dedekind/Peirce definition
of ‘infinite’ is used:
∃f : ind → ind. (∀x
1
, x
2
. (f(x
1
) = f(x
2
)) ⇒ (x
1
= x
2
))∧
¬(∀y. ∃x. y = f(x))
That is, we assert the existence of a function from the type of individuals to
itself that is injective but not surjective. Such a mapping is impossible if the
type is finite, since it would entail that it can be put into 1-1 correspondence
with a proper subset of itself.
From that simple foundation, all the HOL mathematics and applications, in-
cluding those described here, is developed by definitional extension.