Skip to main content
Log in

The inconsistency of higher order extensions of Martin-Löf's type theory

  • Published:
Journal of Philosophical Logic Aims and scope Submit manuscript

Abstract

Martin-Löf's constructive type theory forms the basis of this paper. His central notions of category and set, and their relations with Russell's type theories, are discussed. It is shown that addition of an axiom — treating the category of propositions as a set and thereby enabling higher order quantification — leads to inconsistency. This theorem is a variant of Girard's paradox, which is a translation into type theory of Mirimanoff's paradox (concerning the set of all well-founded sets). The occurrence of the contradiction is explained in set theoretical terms. Crucial here is the way a proof-object of an existential proposition is understood. It is shown that also Russell's paradox can be translated into type theory. The type theory extended with the axiom mentioned above contains constructive higher order logic, but even if one only adds constructive second order logic to type theory the contradictions arise.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  • Barendregt, H. P., Typed Lambda Calculi, in: Abramski, S. (ed.), Handbook of Logic in Computer Science, Oxford University Press, to appear.

  • Beeson, M. J., 1985, Foundations of Constructive Mathematics, Springer Verlag.

  • CopiI. M., 1958, The Burali-Forti Paradox, Philosophy of Science 25, pp. 281–286.

    Google Scholar 

  • CopiI. M., 1971, The Theory of Logical Types, Routledge & Kegan Paul, London.

    Google Scholar 

  • Coquand, TH, 1985, Une théorie des constructions, Thèse de troisième cycle, Paris VII. The first chapter circulates under the title Mathematical Investigation of a Calculus of Constructions.

  • CoquandTH, 1986, An Analysis of Girard's Paradox, in: Proceedings of the First Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, Washington, pp. 227–236.

    Google Scholar 

  • Coquand, TH., and Huet, G., 1988, The Calculus of Constructions, in: Information and Computation 76, p. 95–120.

  • Van Dalen, D., 1983, Logic and Structure (second edition), Springer Verlag.

  • Frege, G., 1891, Funktion und Begriff, from: Patzig, G. (ed.), Gottlob Frege. Funktion, Begiff, Bedeutung, Göttingen, 1980, pp. 18–39.

  • Gödel, K., 1944, Russell's Mathematical Logic, in: Schilpp, P. A., The Philosophy of Bertrand Russell, Tudor, New York, Reprinted in: Benacerraf, P. and Putnam, H., Philosophy of Mathematics. Selected Readings, Prentice Hall, 1964 (to which the pagenumbers refer).

  • Girard, J. Y., 1972, Interprétation fonctionelle et élimination des coupures de l'aritmétique d'ordre supérieur, Thèse d'État, Paris VII

  • HaoWang, 1974, From Mathematics to Philosophy, Routledge and Kegan Paul, London.

    Google Scholar 

  • HowardW., 1980, The formulae-as-types notion of construction, in: HindleyJ. R. and SeldinJ. P. (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism. (Academic Press, New York and London), pp. 479–490.

    Google Scholar 

  • Martin-Löf, P., 1971a, Hauptsatz for the Theory of Species, in: Fenstad, J. E. (ed.), Proceedings of the Second Scandinavian Logic Symposium, North Holland.

  • Martin-Löf, P., 1971b, A Theory of Types. Unpublished.

  • Martin-Löf, P., 1972, An Intuitionistic Theory of Types. Unpublished.

  • Martin-Löf, P., Constructive Mathematics and Computer Programming, in: Cohen, L. J. et al. (eds.), Logic, Methodology and Philosophy of Science VI, North Holland, pp. 153–175.

  • Martin-Löf, P., 1984, Intuitionistic Type Theory, Studies in Proof Theory, Lecture Notes, Bibliopolis, Napoli.

  • Martin-Löf, P., 1985, On the Meanings of the Logical Constants and the Justifications of the Logical Laws, in: Atti degli incontri di logica matematica Vol. 2, Scuola di Specializazione in Logica Matematica, Dipartimento di Matematica, Università di Siena, pp. 203–281.

  • Martin-Löf, P., 1986, The Category Structure of Intuitionistic Type Theory. Unpublished notes of a lecture held for the Société Belge de Logique et de Philosophie des Sciences, 26 April.

  • Martin-Löf, P., 1987, Truth of a Proposition, Evidence of a Judgement, Validity of Proof, in: Synthese 73, pp. 407–420.

  • MirimanoffD., 1917, Les antinomies de Russell et de Burali-Forti et le problème fondamental de la théorie des ensembles, L'Einseignement Mathematique 19, pp. 37–52.

    Google Scholar 

  • MooreG. H. and GarciadiegoA., 1981, Burali-Forti's Paradox: A Repraisal of Its Origins, Historia Mathematica 8, pp. 319–350.

    Google Scholar 

  • Montague, R., 1955, On the Paradox of Grounded Classes, Journal of Symbolic Logic 20(2), p. 140.

    Google Scholar 

  • Passmore, J., 1957, A Hundred Years of Philosophy. (The citation is from the 1984 Penguin edition).

  • Quine, W. V. O., 1963, Set Theory and Its Logics, Cambridge, Mass.

  • Ramsey, F. P., 1926, The Foundations of Mathematics, in: Proceedings of the London Mathematical Society, pp. 338–384. Reprinted in: Braithwaite, R. B. (ed.), The Foundations of Mathematics and Other Logical Essays, 1931, pp. 1–61.

  • Russell, B., 1903, The Principles of Mathematics, Cambridge, England.

  • Russell, B., 1908, Mathematical Logic as Based on the Theory of Types, Am. J. Math. 30, pp. 222–262. Reprinted in: Marsh, R. Ch. (ed.), Bertrand Russell, Logic and Knowledge, Essays 1901–1950. London, 1971, pp. 57–102. (The citations are from this reprint.)

Download references

Author information

Authors and Affiliations

Authors

Rights and permissions

Reprints and permissions

About this article

Cite this article

Jacobs, B. The inconsistency of higher order extensions of Martin-Löf's type theory. J Philos Logic 18, 399–422 (1989). https://doi.org/10.1007/BF00262943

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00262943

Keywords

Navigation