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 <m...@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 <r...@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@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ 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@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
