Re: [isabelle] Where to learn about HOL vs FOL?
Adding to Gottfried´s selected readings, I strongly recommend the highly
"The Seven Virtues of Simple Type Theory' by William Farmer (Journal of
Applied Logic 6, 2008.
On Thu, Jan 31, 2013 at 12:04 PM, Gottfried Barrow <gottfried.barrow at gmx.com
> 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.
> 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:
> 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:
> 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:
> 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":
> Alfio recently pointed me to "Introduction to Type Theory" by Geuvers
> which makes comparisons between type theory and set theory:
> 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:
> 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.
>> 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
>> 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