[isabelle] Where to learn about HOL vs FOL?
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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and