Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: info-hol@leopard.cs.byu.edu
Subject: Re: hardware and higher-order logic
In-Reply-To: Your message of "Thu, 16 Jun 94 10:29:54 BST." <9406160929.AA18543@switha.dcs.gla.ac.uk>
Date: Thu, 16 Jun 94 15:35:22 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:057960:940616143621"@cl.cam.ac.uk>


Tom Melham writes:

| By the way, there's a common misconception that just because you're
| working in higher order logic, *everything* becomes a lot harder.
| First-order logic is just a sublanguage of higher-order logic - with
| pretty much the same rules and syntax. And quite often one finds oneself
| essentially in this first-order subworld - where the first-order proofs
| are no harder than usual.

I would say that higher order logic (as implemented in HOL) is simpler than
first order logic, in the same sense that complex analysis is simpler than
real analysis. That is, though superficially more sophisticated, it has
great elegance and clarity and isn't hedged with ad-hoc restrictions.
(Arguably the syntax of FOL is more difficult than HOL's, btw.)

It's true that restriction to "elementary" (first order) propositions often
makes the deductive process much easier -- in the extreme, decidable. But
one might point out other interesting fragments (e.g. equational logic) that
also have nice deductive properties, and that isn't to say we should
restrict ourselves *entirely* to them (though some people do take that view
of course!)

The primacy of first order logic in mathematical circles is probably due to
the fact that one can teach a nice undergraduate course based around a few
interesting metatheorems. However the question of actually *doing*
mathematics, or hardware verification, in a logical formalism makes quite
different demands on that formalism from metamathematical interest. To me
there is every reason to prefer HOL because of the superior expressive power
that Tom mentions.

There is a good discussion of both the philosophy and technicalities
connected with higher order logic in Shapiro's book "Foundations without
Foundationalism" published in 1991 by Oxford University Press.

John.