Re: [isabelle] Where to learn about HOL vs FOL?

On 1/31/2013 12:54 AM, Yannick Duchêne (Hibou57) wrote:
Hi people,

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 with Isabelle/HOL:

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 logic.
    For example, HOL admits categorical axiomatizations of the natural
numbers, and of the real numbers, which are impossible with first-order logic. However, by a result of Gödel, HOL with standard semantics does
    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 MHonArc.