Re: [isabelle] Where to learn about HOL vs FOL?
On 1/31/2013 12:54 AM, Yannick Duchêne (Hibou57) wrote:
I hope my question won't look too much stupid to logics gurus.
I collect books written by the logic gurus, and occasionally read the
introductions, so I am qualified to provide links to books.
The standard text that keeps getting mentioned by the logic gurus here
is Andrews' text, which starts with propositional logic and FOL, and
then covers type theory, where types would be the beginning of the
foundation of HOL in general:
FOL begins with the standard logic operators as its primitives, or a few
of them from which the others can be derived, as shown by Definitions
5.1, 5.2, and 5.3 of Bilaniuk's book:
FOL is reasonably fixed in stone and standardized.
HOL begins with variables, functions, and function application as
primitives, as shown by Paulson's "Foundations of Functional
Programming" Definition 1, page 2:
From there (or somewhere else) HOL diverges, where the two biggest
camps would be Coq's higher-order logic, and the HOL family, where HOL
is not to be confused with the general phrase "higher-order logic", and
where John Harrison gives a diagram showing the HOL family of products
on page 9 of "HOL Light Tutorial":
Alfio recently pointed me to "Introduction to Type Theory" by Geuvers
which makes comparisons between type theory and set theory:
Because ZFC sets reigns as King and Queen in the world of mathematics,
and is a FOL language, then HOL vs. FOL is largely "types vs. ZFC sets",
at least for those who even know about the comparison, where education
about types is near non-existence in formal, mathematics education, even
though Church and Curry had their formal degrees in mathematics.
To compare the two, the problem is understanding what HOL is, not what
FOL is, at least for me, since FOL is much simpler, even though HOL
starts with a simple set of primitives.
I shared a list of the books I'd collected on trying to get up to speed
Fortunately, I've decided I probably will be able to be live more
normally, which is to occasionally ponder questions about foundational
logic, but not have to completely understand it all to work at a higher
level. It's a very healthy place to be.
Reading at Wikipedia's page about HOL, something tackled me a bit:
“HOL with standard semantics is more expressive than first-order
For example, HOL admits categorical axiomatizations of the natural
numbers, and of the real numbers, which are impossible with
logic. However, by a result of Gödel, HOL with standard semantics
not admit an effective, sound and complete proof calculus.”
There's also a criticism section on the same page.
Well, I'm not sure to understand what it really means and would like
to know if there are good pointers to understand how and when
difference between HOL and FOL matters, and when and how Isabelle has
to do with it. The quote from Wikipedia looks weird to me, as it seems
to say they may be soundness issue with HOL? Is that really it? I've
never heard about any such assertion before…
This archive was generated by a fusion of
Pipermail (Mailman edition) and