Intuitionist type theory and foundations

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

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

Categories

Keywords

Reprint years

DOI

10.1007/bf00253914

Other Versions

No versions found

Links

PhilArchive

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

What is the world of mathematics?J. Lambek - 2004 - Annals of Pure and Applied Logic 126 (1-3):149-158.
On some peculiar aspects of the constructive theory of point-free spaces.Giovanni Curi - 2010 - Mathematical Logic Quarterly 56 (4):375-387.
An Intuitionistic Version of Cantor's Theorem.Dario Maguolo & Silvio Valentini - 1996 - Mathematical Logic Quarterly 42 (1):446-448.
Denotational semantics for intuitionistic type theory using a hierarchy of domains with totality.Geir Waagbø - 1999 - Archive for Mathematical Logic 38 (1):19-60.
An Overview of Type Theories.Nino Guallart - 2015 - Global Philosophy 25 (1):61-77.
Type-theoretical Grammar.Aarne Ranta - 1994 - Oxford, England: Oxford University Press on Demand.
Logical Foundations for Hybrid Type-Logical Grammars.Richard Moot & Symon Jory Stevens-Guille - 2022 - Journal of Logic, Language and Information 31 (1):35-76.
A Transfinite Type Theory with Type Variables.J. M. P. - 1966 - Review of Metaphysics 20 (1):144-144.
On the ordered Dedekind real numbers in toposes.Marcelo E. Coniglio & Luís A. Sbardellini - 2015 - In Edward H. Haeusler, Wagner Sanz & Bruno Lopes, Why is this a Proof? Festschrift for Luiz Carlos Pereira. College Publications. pp. 87-105.
A constructive examination of a Russell-style ramified type theory.Erik Palmgren - 2018 - Bulletin of Symbolic Logic 24 (1):90-106.

Analytics

Added to PP
2009-01-28

Downloads
143 (#302,075)

6 months
16 (#749,564)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Category theory.Jean-Pierre Marquis - 2008 - Stanford Encyclopedia of Philosophy.
New Proofs of Some Intuitionistic Principles.P. J. Scott & J. Lambek - 2006 - Mathematical Logic Quarterly 29 (10):493-504.

Add more citations

References found in this work

Introduction to Metamathematics.Stephen Cole Kleene - 1952 - Groningen: North-Holland.
Natural deduction: a proof-theoretical study.Dag Prawitz - 1965 - Mineola, N.Y.: Dover Publications.
Mathematical Logic as Based on the Theory of Types.Bertrand Russell - 1908 - American Journal of Mathematics 30 (3):222-262.
Completeness in the theory of types.Leon Henkin - 1950 - Journal of Symbolic Logic 15 (2):81-91.
Completeness in the Theory of Types.Leon Henkin - 1950 - Journal of Symbolic Logic 16 (1):72-73.

View all 10 references / Add more references