*To*: Roger Bishop Jones <rbj at rbjones.com>*Subject*: [isabelle] Genesis of Church's simple theory of types, Wiedijk's criticism concerning the (current) HOL family*From*: Ken Kubota <mail at kenkubota.de>*Date*: Sat, 22 Oct 2016 04:41:27 +0200*Cc*: HOL-info list <hol-info at lists.sourceforge.net>, "Prof. Peter B. Andrews" <andrews at cmu.edu>, cl-isabelle-users at lists.cam.ac.uk*References*: <5E3CAC59-87D9-4C98-A58E-1B435A2F1E41@kenkubota.de>

â 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

**Follow-Ups**:

**References**:

- Previous by Date: [isabelle] Smash flex-flex pairs in calculational reasoning
- Next by Date: Re: [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?
- Previous by Thread: [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?
- Next by Thread: Re: [isabelle] [Hol-info] Genesis of Church's simple theory of types, Wiedijk's criticism concerning the (current) HOL family
- Cl-isabelle-users October 2016 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