Order and Logic
7
we obtain that f
α (x) = f (f
α (x)), and so a = f
α (x) is a fixed point of f .
Clearly, we have x [ a. Furthermore, if b is any pre-fixed point of f with
x [ b, then by monotonicity of f and the fact that f (b) [ b we obtain
f
β (x) [ b for all ordinals β. Hence, a [ b, and so a is both the least pre-fixed
point and the least fixed point of f above x.
To obtain the final conclusion, we simply set x = ⊥ and note then that
x [ f (x).
•
Note that, in particular, the least fixed point of f is equal to f ↑ α for
some ordinal α. We call the smallest ordinal α with this property the closure
ordinal of f .
One other point to make in this context is that Kleene’s theorem shows
that ω-continuity ensures that in finding a fixed point the iteration will not
continue beyond the first infinite ordinal ω. This contrasts with the KnasterTarski theorem, where it may be necessary to iterate beyond ω if one only has
monotonicity of the operators in question. This is a significant point in relation to computability considerations and explains the importance of Kleene’s
theorem in the theory of computation.
1.2 First-Order Predicate Logic
We assume that the reader has a slight familiarity with first-order predicate
logic, but for convenience we summarize next the elementary concepts of the
subject, beginning by formally describing its syntax.
10
1.2.1 Syntax of First-Order Predicate Logic
As usual, an alphabet A consists of the following classes
11 of symbols:
a (possibly empty) collection of constant symbols a, b, c, d, . . .; a non-empty
collection of variable symbols u, v, w, x, y, z, . . .; a (possibly empty) collection
of function symbols f, g, h, . . .; and a non-empty collection of predicate sym10 Our approach to the syntax and semantics of first-order logic is standard and is to be
found in any of the well-known texts on mathematical logic, see, for example, [Hodel, 1995,
Mendelson, 1987]. For fuller details of logic in relation to logic programming, the reader
may care to consult [Apt, 1997] or [Lloyd, 1987].
11 Similarly, our use of classes in the definition of an alphabet is also standard in developing
first-order logic and, in our case, is not intended to hint at foundational issues. In logic
programming practice, the classes referred to, namely, those of constant, variable, function,
and predicate symbols, will be finite sets. When working with the set ground J (P ) defined in
Chapter 2, J will usually (although not necessarily) denote the Herbrand preinterpretation,
and then we will in effect be working with a set containing a possibly denumerable collection
of elements (atoms, in fact).
7
we obtain that f
α (x) = f (f
α (x)), and so a = f
α (x) is a fixed point of f .
Clearly, we have x [ a. Furthermore, if b is any pre-fixed point of f with
x [ b, then by monotonicity of f and the fact that f (b) [ b we obtain
f
β (x) [ b for all ordinals β. Hence, a [ b, and so a is both the least pre-fixed
point and the least fixed point of f above x.
To obtain the final conclusion, we simply set x = ⊥ and note then that
x [ f (x).
•
Note that, in particular, the least fixed point of f is equal to f ↑ α for
some ordinal α. We call the smallest ordinal α with this property the closure
ordinal of f .
One other point to make in this context is that Kleene’s theorem shows
that ω-continuity ensures that in finding a fixed point the iteration will not
continue beyond the first infinite ordinal ω. This contrasts with the KnasterTarski theorem, where it may be necessary to iterate beyond ω if one only has
monotonicity of the operators in question. This is a significant point in relation to computability considerations and explains the importance of Kleene’s
theorem in the theory of computation.
1.2 First-Order Predicate Logic
We assume that the reader has a slight familiarity with first-order predicate
logic, but for convenience we summarize next the elementary concepts of the
subject, beginning by formally describing its syntax.
10
1.2.1 Syntax of First-Order Predicate Logic
As usual, an alphabet A consists of the following classes
11 of symbols:
a (possibly empty) collection of constant symbols a, b, c, d, . . .; a non-empty
collection of variable symbols u, v, w, x, y, z, . . .; a (possibly empty) collection
of function symbols f, g, h, . . .; and a non-empty collection of predicate sym10 Our approach to the syntax and semantics of first-order logic is standard and is to be
found in any of the well-known texts on mathematical logic, see, for example, [Hodel, 1995,
Mendelson, 1987]. For fuller details of logic in relation to logic programming, the reader
may care to consult [Apt, 1997] or [Lloyd, 1987].
11 Similarly, our use of classes in the definition of an alphabet is also standard in developing
first-order logic and, in our case, is not intended to hint at foundational issues. In logic
programming practice, the classes referred to, namely, those of constant, variable, function,
and predicate symbols, will be finite sets. When working with the set ground J (P ) defined in
Chapter 2, J will usually (although not necessarily) denote the Herbrand preinterpretation,
and then we will in effect be working with a set containing a possibly denumerable collection
of elements (atoms, in fact).