CHURCH, ALONZO.

A formulation of the simple theory of types.

(No place), The Association for Symbolic Logic, 1940.

Large 8vo. Bound in blue half cloth with silver lettering to spine. In "Journal of Symbolic Logic", Volume 5. Small paper label to lower part of spine and upper inner margin of front board. Stamp to title-page and last leaf, otherwise internally fine. Pp. 56-68. (Entire copy: IV, 188 pp.).

First printing of Church's seminal paper in which he introduced his Type Theory: A simpler and more general Type Theory than the one introduced by Bertrand Russell in 1908 and Whitehead & Russell in 1927.

"Church's type theory is a formal logical language which includes first-order logic, but is more expressive in a practical sense. It is used, with some modifications and enhancements, in most modern applications of type theory. It is particularly well suited to the formalization of mathematics and other disciplines and to specifying and verifying hardware and software. A great wealth of technical knowledge can be expressed very naturally in it. With possible enhancements, Church's type theory constitutes an excellent formal language for representing the knowledge in automated information systems, sophisticated automated reasoning systems, systems for verifying the correctness of mathematical proofs, and certain projects involving logic and artificial intelligence." (SEP)

Order-nr.: 60429