Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Bibliography
Boileau, A., Types vs topos, Thesis (Université de Montréal, 1975).
ChurchA., ‘A foundation for the simple theory of types’, J. Symbolic Logic 5 (1940), 56–68.
Coste, M., Logique d'ordre supérieur dans les topos élémentaires, Séminaire dirigé par Jean Bénabou, Novembre 1974, Université Paris-Nord.
FourmanM. P., ‘The logic of topoi’, in Handbook of Math. Logic (by Barwise), (North Holland, Amsterdam 1977), pp. 1053–1090.
Freyd, P., ‘On proving that 1 is an indecomposable projective in various free categories’, Preprint 1978.
GödelK., ‘Über formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme I’, Monatshefte für Math. und Physik 38 (1931), 173–198; English translation in ‘From Frege to Gödel’, ed. by van Heijenoort.
HatcherW. S., Foundations of Mathematics (Saunders, Philadelphia, 1968).
HenkinL., ‘Completeness in the theory of types’, J. Symbolic Logic 15 (1950), 81–91.
HenkinL., ‘A theory of propositional types’, Fundamenta Math. 52 (1963), 323–333.
JohnstoneP. T., Topos Theory (Academic Press, London, 1977).
KleeneS. C., Introduction to Metamathematics (Van Nostrand, New York and Toronto, 1952).
LambekJ., ‘Deductive system and categories III’, Lecture Notes in Mathematics 274 (Springer, Berlin, 1972), 57–82.
LambekJ., ‘Functional completeness of cartesian categories’, Annals of Math. Logic 6 (1974) 259–292.
LambekJ., ‘From types to sets’, Advances in Mathematics 36 (1980), 113–164.
Lambek, J. and Scott, P. J., ‘Intuitionist type theory and the free topos’, J. Pure and Applied Algebra (forthcoming).
LawvereF. W., ‘An elementary theory of the category of sets’, Proc. Nat. Acad. Sci. 52 (1964), 1506–1511.
LawvereF. W., ‘Introduction, in “Toposes, Algebraic Geometry and Logic”’, Lecture Notes in Mathematics 274 (Springer, Berlin, 1972), 1–12.
MulveyC., ‘Intuitionist algebra and representations of rings’, Memoirs Amer. Math. Soc. 148 (1974), 3–57.
PrawitzD., Natural Deduction (Almqvist and Wiskell, Stockholm, 1965).
RussellB., ‘Mathematical logic based on the theory of types’, Amer. J. Math. 30 (1908), 222–262 (reprinted in van Heijenoort).
TierneyM. ‘Sheaf theory and the continuum hypothesis’, Lecture Notes in Mathematics 274 (Springer, Berlin, 1972), 13–42.
TroelstraA. S., ‘Notes on second order arthmetic’, Lecture Notes in Mathematics 337 (Springer, Berlin, 1973), 171–205.
VanHeijenoortJ., From Frege to Gödel (Harvard University Press, Cambridge, Mass. 1967).
VolgerH., ‘Logical and semantical categories and topoi’, Lecture Notes in Mathematics 445 (Springer, Berlin, 1975), 87–100.
Rights and permissions
About this article
Cite this article
Lambek, J., Scott, P.J. Intuitionist type theory and foundations. J Philos Logic 10, 101–115 (1981). https://doi.org/10.1007/BF00253914
Issue Date:
DOI: https://doi.org/10.1007/BF00253914