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

The Wikipedia article is referring to the fact that there will always be
true statements in HOL that are not the conclusion of any derivation in a
proof calculus.
(This can be contrasted with FOL: there is a sound proof calculus for FOL
with the property that every true FOL statement can be proved in it.)
(The problem in HOL, as I understand it, is that there are too many true
statements, more than could be all the conclusions from a proof calculus.)

It does not say that there cannot be a sound proof calculus for HOL.
Indeed, we think Isabelle/HOL implements one such calculus.

As for how to learn this stuff... I'm sure someone on list will be able to
recommend a good textbook.
Personally I think Wikipedia is OK, but you have to be patient and willing
to read carefully and follow links... and sometimes it may be wrong, so
discussing with others helps :)

On Thu, Jan 31, 2013 at 6:54 AM, Yannick Duchêne (Hibou57) <
yannick_duchene at> wrote:

> 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.