Hostname: page-component-848d4c4894-x24gv Total loading time: 0 Render date: 2024-05-05T22:57:53.286Z Has data issue: false hasContentIssue false
  • English
  • Français

Practical forms of type theory

Published online by Cambridge University Press:  12 March 2014

A. M. Turing
A. M. Turing*
Affiliation:
National Physical Laboratory, Teddington
Get access Rights & Permissions [Opens in a new window]

Extract

Russell's theory of types, though probably not providing the soundest possible foundation for mathematics, follows closely the outlook of most mathematicians. The present paper is an attempt to present the theory of types in forms in which the types themselves only play a rather small part, as they do in ordinary mathematical argument. Two logical systems are described (called the “nested-type” and “concealed-type” systems). It is hoped that the ideas involved in these systems may help mathematicians to observe type theory in proofs as well as in doctrine. It will not be necessary to adopt a formal logical notation to do so.

Type
Articles
Information
The Journal of Symbolic Logic , Volume 13 , Issue 2 , June 1948 , pp. 80 - 94
Copyright
Copyright © Association for Symbolic Logic 1948

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

1 Whitehead, A. N. and Russell, Bertrand, Principia mathematica, Cambridge, England, 1925.Google Scholar

2 We shall use heavy type letters throughout to represent variables or undetermined formulas or tables. They occur only in metamathematical discussions. All our statements are understood to be true whatever substitutions of formulas (or tables, as the case may be) are made for the heavy type capital letters, and whatever substitutions of variables are made for the small heavy type letters.

3 Church, Alonzo, A formulation of the simple theory of types, this Journal, vol. 5 (1940), pp. 66–68.Google Scholar