… 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
