FOM: Why HOL is stronger than FOL
Till Mossakowski
till at Informatik.Uni-Bremen.DE
Sat Mar 20 20:43:57 EST 1999
Dear FOMers,
I just noticed that there is an ongoing discussion about
the relation of quantifier-based and
lambda-abstraction based second-order logic.
Since I am writing a paper about the specification
language higher-order CASL, I take this opportunity
to present my view on a related subject, namely
the relation between FOL and HOL,
and I am interested in feedback.
HOL is stronger than FOL because it has
1) a finite description of infinitely many sorts, together
with implicit operations
a) function and predicate types (with application)
b) product types (with tupling)
2) lambda-abstraction (a binding mechanism
more flexible than quantifiers, leading to more terms)
Connected with this is comprehension.
In first-order logic without axiom schemes,
comprehension requires an infinite number of axioms,
while in HOL, it is built-in.
Also connected with this is a more powerful
unification, which involves beta-reduction.
Resolution proofs thus become shorter, at the price
of having unification undecidable, and without
most general unifiers.
3) the Hilbert operator leads to even more terms,
and it allows shorter proofs than the
axiom of choice.
4) Logical connectives are definable, since
formulae are terms of sort bool.
All these features are orthogonal and can be
separately added to FOL (except that lambda
abstraction depends on higher types).
Especially for (semi-)automated
theorem proving, the following above become
important.
I agree with Steve (Fri, 19 Mar 1999 18:16:53)
that HOL should be considered
with Henkin semantics, so the possibility
of categorical axiomatizations of the naturals
and the reals are *not* a feature of HOL.
Thus, in principle, HOL can be reduced to FOL,
but at the price of getting more cumbersome
axiom systems and proofs.
Till Mossakowski
More information about the FOM
mailing list