# A formulation of the simple theory of types

A formulation of the simple theory of types <jats:p>The purpose of the present paper is to give a formulation of the simple theory of types which incorporates certain features of the calculus of λ-conversion. A complete incorporation of the calculus of λ-conversion into the theory of types is impossible if we require that λ<jats:italic>x</jats:italic> and juxtaposition shall retain their respective meanings as an abstraction operator and as denoting the application of function to argument. But the present partial incorporation has certain advantages from the point of view of type theory and is offered as being of interest on this basis (whatever may be thought of the finally satisfactory character of the theory of types as a foundation for logic and mathematics).</jats:p><jats:p>For features of the formulation which are not immediately connected with the incorporation of λ-conversion, we are heavily indebted to Whitehead and Russell, Hilbert and Ackermann, Hilbert and Bernays, and to forerunners of these, as the reader familiar with the works in question will recognize.</jats:p><jats:p>The class of <jats:italic>type symbols</jats:italic> is described by the rules that ı and <jats:italic>o</jats:italic> are each type symbols and that if <jats:italic>α</jats:italic> and <jats:italic>β</jats:italic> are type symbols then (<jats:italic>αβ</jats:italic>) is a type symbol: it is the least class of symbols which contains the symbols ı and <jats:italic>o</jats:italic> and is closed under the operation of forming the symbol (<jats:italic>αβ</jats:italic>) from the symbols <jats:italic>α</jats:italic> and <jats:italic>β</jats:italic>.</jats:p> http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of Symbolic Logic CrossRef

# A formulation of the simple theory of types

Journal of Symbolic Logic , Volume 5 (2): 56-68 – Jun 1, 1940

## A formulation of the simple theory of types

### Abstract

<jats:p>The purpose of the present paper is to give a formulation of the simple theory of types which incorporates certain features of the calculus of λ-conversion. A complete incorporation of the calculus of λ-conversion into the theory of types is impossible if we require that λ<jats:italic>x</jats:italic> and juxtaposition shall retain their respective meanings as an abstraction operator and as denoting the application of function to argument. But the present partial incorporation has certain advantages from the point of view of type theory and is offered as being of interest on this basis (whatever may be thought of the finally satisfactory character of the theory of types as a foundation for logic and mathematics).</jats:p><jats:p>For features of the formulation which are not immediately connected with the incorporation of λ-conversion, we are heavily indebted to Whitehead and Russell, Hilbert and Ackermann, Hilbert and Bernays, and to forerunners of these, as the reader familiar with the works in question will recognize.</jats:p><jats:p>The class of <jats:italic>type symbols</jats:italic> is described by the rules that ı and <jats:italic>o</jats:italic> are each type symbols and that if <jats:italic>α</jats:italic> and <jats:italic>β</jats:italic> are type symbols then (<jats:italic>αβ</jats:italic>) is a type symbol: it is the least class of symbols which contains the symbols ı and <jats:italic>o</jats:italic> and is closed under the operation of forming the symbol (<jats:italic>αβ</jats:italic>) from the symbols <jats:italic>α</jats:italic> and <jats:italic>β</jats:italic>.</jats:p>

/lp/crossref/a-formulation-of-the-simple-theory-of-types-6RSeAru9IB

# References

References for this paper are not available at this time. We will be adding them shortly, thank you for your patience.

Publisher
CrossRef
ISSN
0022-4812
DOI
10.2307/2266170
Publisher site
See Article on Publisher Site

### Abstract

<jats:p>The purpose of the present paper is to give a formulation of the simple theory of types which incorporates certain features of the calculus of λ-conversion. A complete incorporation of the calculus of λ-conversion into the theory of types is impossible if we require that λ<jats:italic>x</jats:italic> and juxtaposition shall retain their respective meanings as an abstraction operator and as denoting the application of function to argument. But the present partial incorporation has certain advantages from the point of view of type theory and is offered as being of interest on this basis (whatever may be thought of the finally satisfactory character of the theory of types as a foundation for logic and mathematics).</jats:p><jats:p>For features of the formulation which are not immediately connected with the incorporation of λ-conversion, we are heavily indebted to Whitehead and Russell, Hilbert and Ackermann, Hilbert and Bernays, and to forerunners of these, as the reader familiar with the works in question will recognize.</jats:p><jats:p>The class of <jats:italic>type symbols</jats:italic> is described by the rules that ı and <jats:italic>o</jats:italic> are each type symbols and that if <jats:italic>α</jats:italic> and <jats:italic>β</jats:italic> are type symbols then (<jats:italic>αβ</jats:italic>) is a type symbol: it is the least class of symbols which contains the symbols ı and <jats:italic>o</jats:italic> and is closed under the operation of forming the symbol (<jats:italic>αβ</jats:italic>) from the symbols <jats:italic>α</jats:italic> and <jats:italic>β</jats:italic>.</jats:p>

### Journal

Journal of Symbolic LogicCrossRef

Published: Jun 1, 1940