*To*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Subject*: Re: [isabelle] Where to learn about HOL vs FOL?*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Thu, 31 Jan 2013 13:20:28 +0000*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <op.wrrj47uzule2fv@cardamome>*References*: <op.wrrj47uzule2fv@cardamome>*Sender*: ramana.kumar at gmail.com

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

**References**:**[isabelle] Where to learn about HOL vs FOL?***From:*Yannick Duchêne (Hibou57)

- Previous by Date: Re: [isabelle] Evaluation of List.coset
- Next by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Previous by Thread: [isabelle] Where to learn about HOL vs FOL?
- Next by Thread: Re: [isabelle] Where to learn about HOL vs FOL?
- Cl-isabelle-users January 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list