Intuitionist type theory and foundations

Journal of Philosophical Logic 10 (1):101 - 115 (1981)

A version of intuitionistic type theory is presented here in which all logical symbols are defined in terms of equality. This language is used to construct the so-called free topos with natural number object. It is argued that the free topos may be regarded as the universe of mathematics from an intuitionist's point of view
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1007/BF00253914
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 47,201
Through your library

References found in this work BETA

Foundations of Mathematics.William S. Hatcher - 1968 - Philadelphia: W. B. Saunders Co..
Topos Theory.P. T. Johnstone - 1982 - Journal of Symbolic Logic 47 (2):448-450.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles


Added to PP index

Total views
49 ( #183,156 of 2,289,671 )

Recent downloads (6 months)
5 ( #236,884 of 2,289,671 )

How can I increase my downloads?


My notes

Sign in to use this feature