FOM: Why HOL is stronger than FOL

[Till Mossakowski]

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