# 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
discussing with others helps :)

On Thu, Jan 31, 2013 at 6:54 AM, Yannick Duchêne (Hibou57) <
yannick_duchene at yahoo.fr> 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:
>
> http://en.wikipedia.org/wiki/**Higher-order_logic<http://en.wikipedia.org/wiki/Higher-order_logic>
>
>    “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.