Hostname: page-component-586b7cd67f-rcrh6 Total loading time: 0 Render date: 2024-11-25T10:17:21.498Z Has data issue: false hasContentIssue false
  • English
  • Français

Models of intuitionistic TT and NF

Published online by Cambridge University Press:  12 March 2014

Daniel Dzierzgowski
Daniel Dzierzgowski*
Affiliation:
Université Catholique de Louvain, Département de Mathématique, Chemin du Cyclotron 2, B-1348 Louvain-la-Neuve (Belgium), E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Let us define the intuitionistic part of a classical theory T as the intuitionistic theory whose proper axioms are identical with the proper axioms of T. For example, Heyting arithmetic HA is the intuitionistic part of classical Peano arithmetic PA.

It's a well-known fact, proved by Heyting and Myhill, that ZF is identical with its intuitionistic part.

In this paper, we mainly prove that TT, Russell's Simple Theory of Types, and NF, Quine's “New Foundations,” are not equal to their intuitionistic part. So, an intuitionistic version of TT or NF seems more naturally definable than an intuitionistic version of ZF.

In the first section, we present a simple technique to build Kripke models of the intuitionistic part of TT (with short examples showing bad properties of finite sets if they are defined in the usual classical way).

In the remaining sections, we show how models of intuitionistic NF2 and NF can be obtained from well-chosen classical ones. In these models, the excluded middle will not be satisfied for some non-stratified sentences.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 60 , Issue 2 , June 1995 , pp. 640 - 653
Copyright
Copyright © Association for Symbolic Logic 1995

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Boffa, Maurice, The point on Quine's NF (with a bibliography), Teoria, vol. IV/2 (1984), pp. 3–13.Google Scholar
[2] Boffa, Maurice and Crabbé, Marcel, Les théorèmes 3-stratifiés de NF3, Comptes Rendus de l’ Académie des Sciences de Paris, Série A, vol. 280 (1975), pp. 1657–1658.Google Scholar
[3] Fitting, Melvin Chris, Intuitionistic logic model theory and forcing, Studies in Logic, North Holland, Amsterdam, London, 1969.Google Scholar
[4] Forster, Thomas E., On a problem of Dzierzgowski, Bulletin de la Société Mathématique de Belgique, série B, vol. 44 (1992), no. 2, pp. 207–214.Google Scholar
[5] Forster, Thomas E., Set theory with a universal set. Exploiting an untyped universe, Oxford Logic Guides, vol. 20, Clarendon Press. Oxford University Press, 1992.Google Scholar
[6] Körner, Friederike, Cofinal indiscernibles and their application to New Foundations, Mathematical Logic Quaterly, vol. 40 (1994), no. 3, pp. 347–356.CrossRefGoogle Scholar
[7] Lavendhomme, René and Lucas, Thierry, A note on intuitionistic models of ZF, Notre Dame Journal of Formal Logic, vol. 24 (1983), no. 1, pp. 54–66.CrossRefGoogle Scholar
[8] Myhill, John, Embedding classical type theory in “intuitionistic” type theory, Axiomatic set theory (Scott, Dana S., editor), Proceedings of Symposia in Pure Mathematics, vol. XIII, Part I, American Mathematical Society, Providence, R.I., 1971, Proceedings of the Summer Institute in Set Theory, University of California, Los Angeles, 1967, pp. 267–270.CrossRefGoogle Scholar
[9] Myhill, John, Some properties of intuitionistic Zermelo-Fraenkel set theory, Cambridge summer school in mathematical logic, Lecture Notes in Mathematics, vol. 337, Springer-Verlag, 1973, pp. 206–231.CrossRefGoogle Scholar
[10] Myhill, John, Embedding classical type theory in “intuitionistic” type theory: a correction, Axiomatic set theory (Jech, Thomas, editor), Proceedings of Symposia in Pura Mathematics, vol. XIII, Part II, American Mathematical Society, Providence, R.I., 1974, Proceedings of the Summer Institute in Set Theory, University of California, Los Angeles, 1967, pp. 185–188.CrossRefGoogle Scholar
[11] Powell, William C., Extending Gödel's negative interpretation to ZF, this Journal, vol. 40 (1975), pp. 221–229.Google Scholar
[12] Scott, Dana, Quine's individuals, Logic, methodology and philosophy of science (Stanford, California) (Nagel, Suppes, and Tarski, editors), Stanford University Press, 1962, Proceedings of the International Congress, Stanford, California, 1960, pp. 111–115.Google Scholar