Filter
Top Products
88 CHAPTER 11. PRINCIPLES OF DEFINITION
n ∈ E
(n + 2) ∈ E
Read literally, such a definition merely places some constraints on the set E,
asserting its ‘closure’ under the rules, and does not, in general, determine it uniquely.
For example, the set of even numbers satisfies the above, but so does the set of
natural numbers, the set of integers, the set of rational numbers and even the the
whole set of real numbers! But implicit in writing a definition like this is that E
is the least set which is closed under the rules. It is when understood in this sense
that the above defines the even numbers.
This convention, however, needs to be justified by showing that there is a least
set closed under the rules. A good try is to consider the set of all sets which
are closed under the rules, and take their intersection. If only we knew that this
intersection was closed under the rules, then it would certainly be the least such
set. But in general we don’t know that, as the following example illustrates:
n ∈ E
n ∈ E
There are no sets at all closed under this rule! However it turns out that a simple
syntactic restriction on the rules is enough to guarantee that the intersection is
closed under the rules. Crudely speaking, the hypotheses must make only ‘positive’
assertions about membership in S. To state this precisely, observe that we can
collect together all the rules in a single assertion of the form:
∀x. P[S, x] ⇒ x ∈ S
The following example for the even numbers should be a suitable paradigm to
indicate how:
∀n. (n = 0 ∨ ∃m. n = m + 2 ∧ m ∈ E) ⇒ n ∈ E
If we make the abbreviation f(S) = {x | P[S, x]} the assertion can be written
f(S) ⊆ S. Our earlier plan was to take the intersection of all subsets S which
have this property, and hope that the intersection too is closed under the rules.
A sufficient condition for this is given in the following fixpoint theorem due to
Knaster (1927) and Tarski (1955) (which holds for an arbitrary complete lattice):
if f : ℘(X) → ℘(X) is monotone, i.e. for any S ⊆ X and T ⊆ X
S ⊆ T ⇒ f(S) ⊆ f(T)
then if we define
F =
{S ⊆ X | f(S) ⊆ S}
not only is f(F ) ⊆ F but F is actually a fixpoint of f, i.e. f(F) = F . HOL Light
can take an inductive definition and generally manage to prove monotonicity for
itself, providing the user with three useful theorems. The first says that the defined
set is closed under the rules, the second that it is the least set closed under the
rules, and the third gives a case analysis theorem saying that everything in the set
is generated by applying the rules to something else in the set. For example, we
can define finiteness of sets (or, viewed as a set, the set of all finite sets) as follows: