Re: [isabelle] [Hol-info] Genesis of Church's simple theory of types, Wiedijk's criticism concerning the (current) HOL family



Hello Ken,

Not wanting to crowd your diagram too much, but I think maybe HOL Zero (my system!) deserves a mention. It is a bare bones implementation of the logic, and is designed to be highly trustworthy and robust.

  http://www.proof-technologies.com/holzero.html

It can be used to create simple natural deduction proofs, but is mainly intended as a proof checker to replay (via some proof recording mechanism) formal proofs performed on other systems. It has successfully replayed two quarters of the Flyspeck Project, for example, that were originally performed in HOL Light in 1.4 billion primitive inference steps. Another intended role is a pedagogical example of a basic HOL system, with a simple coding style and lots of code comments explaining what is going on, which also helps trustworthiness.

Mark Adams.

On 22/10/2016 03:41, Ken Kubota wrote:
â I have now added the quotes on the genesis of Church's simple theory of types,
and on the invention of Î-calculus and the origin of the Î-notation
in the "Historical Notes" section at:
	http://dx.doi.org/10.4444/100.111

Also interesting might be Freek Wiedijk's criticism
concerning the (current) HOL family quoted in the "Criticism" section.

Ken Kubota

____________________

Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100



Anfang der weitergeleiteten Nachricht:

Von: Ken Kubota <mail at kenkubota.de>

Concerning Roger Jones' remarks, let me first note that a legend ("significance of the shape of boxes") can be found on top of the 2nd page, as it doesn't fit on the first anymore.

Please also note the arrow from lambda calculus (LC) to simple type theory (STT), narrowing the interest to theories based on LC. The purpose is mainly to distinguish the logics based on LC by their expressiveness in terms of their syntactic features, where STT is characterized by having no type variables in their object language at all. From this perspective, the very early developments prior to LC can be neglected, as Church's 1940 paper is the today's standard reference. For me, even Church's 1940 logic is baroque, as I grew up with Andrews' Q0, which is much more
elegant, cleaner, and natural.
However, for historical accuracy, I already considered adding a quote mentioning Ramsey and Chwistek from http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf (p. 12) in the Historical Notes section. Note that Church mentions both, and Carnap, in the first footnote
of his 1940 article.


Am 18.10.2016 um 15:34 schrieb Roger Bishop Jones <rbj at rbjones.com>:

Credit for the Simple Theory of Types
=======================

Ken's diagram makes it look like this theory begins with Church.

Its not entirely uncontroversial as to who should have credit for devising this system. Most frequently credit has been given to Ramsey, but though he seems to have had the idea pretty early on, he never formulated the logical system in detail (and one might think that the idea of simplifying Russell's ramified theory would have occurred to others).

Recent scholarship suggests that the first fully detailed account of STT as a formal system is due to Rudolf Carnap, who, in the course of writing a logistics textbook to facilitate the application of formal logic in mathematics and science, decided to
base it around the simplified rather than the ramified type theory.
I think this particular formulation may have escaped attention because the book "Abriss der Logistik" was written in German and has never been translated into
English.
Until recently the more widely know text by Hilbert and Ackermann was thought
to be the first formal account of the simple theory of types.
STT appears I believe, only in the second edition of their text, so though the first edition (1928) precedes Carnap's (1929) text, he still was in first with STT.
There were many later textbooks which presented this version of STT
(not based on the lambda-calculus and having "power set" as the primitive
type constructor), which was probably the dominant conception of STT
(and may still be, among logicians) until Mike Gordon adopted
and adapted Church's version for HOL.

So maybe a little circle with "(Ramsey/Carnap)" at the top of the STT box?

I wondered what the significance of the shape of boxes in the diagram was. It looked like most of the rectangles were proof tools and the elipses
were theories, but that seems not quite consistent.

Roger Jones


------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info at lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info




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