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



Hi Yannick,

Adding to Gottfried´s selected readings, I strongly recommend the highly
readable

"The Seven Virtues of Simple Type Theory' by William Farmer (Journal of
Applied Logic 6, 2008.

Best!

On Thu, Jan 31, 2013 at 12:04 PM, Gottfried Barrow <gottfried.barrow at gmx.com
> wrote:

> On 1/31/2013 12:54 AM, Yannick Duchêne (Hibou57) wrote:
>
>> Hi people,
>>
>> I hope my question won't look too much stupid to logics gurus.
>>
>
> Yannick,
>
> I collect books written by the logic gurus, and occasionally read the
> introductions, so I am qualified to provide links to books.
>
> The standard text that keeps getting mentioned by the logic gurus here is
> Andrews' text, which starts with propositional logic and FOL, and then
> covers type theory, where types would be the beginning of the foundation of
> HOL in general:
>
> http://www.amazon.com/**Introduction-Mathematical-**Logic-Type-Theory/dp/*
> *1402007639<http://www.amazon.com/Introduction-Mathematical-Logic-Type-Theory/dp/1402007639>
>
> FOL begins with the standard logic operators as its primitives, or a few
> of them from which the others can be derived, as shown by Definitions 5.1,
> 5.2, and 5.3 of Bilaniuk's book:
>
> http://euclid.trentu.ca/math/**sb/pcml/<http://euclid.trentu.ca/math/sb/pcml/>
>
> FOL is reasonably fixed in stone and standardized.
>
> HOL begins with variables, functions, and function application as
> primitives, as shown by Paulson's "Foundations of Functional Programming"
> Definition 1, page 2:
>
> http://www.cl.cam.ac.uk/~lp15/**papers/Notes/Founds-FP.pdf<http://www.cl.cam.ac.uk/~lp15/papers/Notes/Founds-FP.pdf>
>
> From there (or somewhere else) HOL diverges, where the two biggest camps
> would be Coq's higher-order logic, and the HOL family, where HOL is not to
> be confused with the general phrase "higher-order logic", and where John
> Harrison gives a diagram showing the HOL family of products on page 9 of
> "HOL Light Tutorial":
>
> http://www.cl.cam.ac.uk/~**jrh13/hol-light/tutorial_220.**pdf<http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf>
>
> Alfio recently pointed me to "Introduction to Type Theory" by Geuvers
> which makes comparisons between type theory and set theory:
>
> http://www.cs.ru.nl/~herman/**PUBS/IntroTT-improved.pdf<http://www.cs.ru.nl/~herman/PUBS/IntroTT-improved.pdf>
>
> Because ZFC sets reigns as King and Queen in the world of mathematics, and
> is a FOL language, then HOL vs. FOL is largely "types vs. ZFC sets", at
> least for those who even know about the comparison, where education about
> types is near non-existence in formal, mathematics education, even though
> Church and Curry had their formal degrees in mathematics.
>
> To compare the two, the problem is understanding what HOL is, not what FOL
> is, at least for me, since FOL is much simpler, even though HOL starts with
> a simple set of primitives.
>
> I shared a list of the books I'd collected on trying to get up to speed
> with Isabelle/HOL:
>
> http://lists.cam.ac.uk/**mailman/htdig/cl-isabelle-**
> users/2012-June/msg00024.html<http://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-June/msg00024.html>
>
> http://lists.cam.ac.uk/**mailman/htdig/cl-isabelle-**
> users/2012-June/msg00003.html<http://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-June/msg00003.html>
>
> Fortunately, I've decided I probably will be able to be live more
> normally, which is to occasionally ponder questions about foundational
> logic, but not have to completely understand it all to work at a higher
> level. It's a very healthy place to be.
>
> Regards,
> GB
>
>
>
>
>
>> 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…
>>
>
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




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