[isabelle] Where to learn about HOL vs FOL?

Hi people,

I hope my question won't look too much stupid to logics gurus.

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…

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.