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

â 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:

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

> 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

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