Practical forms of type theory

Publisher Website
Google Scholar
Abstract
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.

This publication has 1 reference indexed in Scilit: