Re: [isabelle] [Hol-info] Genesis of Church's simple theory of types, Wiedijk's criticism concerning the (current) HOL family
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.
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.
On 22/10/2016 03:41, Ken Kubota wrote:
â I have now added the quotes on the genesis of Church's simple theory
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.
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
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
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
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
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
Until recently the more widely know text by Hilbert and Ackermann was
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
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
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
I wondered what the significance of the shape of boxes in the diagram
It looked like most of the rectangles were proof tools and the
were theories, but that seems not quite consistent.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and