Dzierzgowski, D.
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 win not be satisfied for some non-stratified sentences.
- Teoria, IV, 3 (1984)
- Comptes Rendus de l’ Académie des Sciences de Paris, Série A, 280, 1657 (1975)
- Intuitionistic logic model theory and forcing (1969)
- Bulletin de la Société Mathématique de Belgique, série B, 44, 207 (1992)
- Set theory with a universal set. Exploiting an untyped universe, 20 (1992)
- Körner Friederike, Cofinal Indiscernibles and some Applications to New Foundations, 10.1002/malq.19940400305
- Lavendhomme R., Lucas T., A note on intuitionistic models of ${\rm ZF}$., 10.1305/ndjfl/1093870220
- Axiomatic set theory, XIII, 267 (1971)
- Myhill John, Some properties of intuitionistic zermelo-frankel set theory, Cambridge Summer School in Mathematical Logic (1973) ISBN:9783540055693 p.206-231, 10.1007/bfb0066775
- Axiomatic set theory, XIII, 185 (1974)
- Extending Gödel's negative interpretation to ZF, 40, 221 (1975)
- Logic, methodology and philosophy of science, 111 (1962)
Bibliographic reference |
Dzierzgowski, D.. Models of Intuitionistic Tt and Nf. In: The Journal of Symbolic Logic, Vol. 60, no. 2, p. 640-653 (1995) |
Permanent URL |
http://hdl.handle.net/2078.1/48010 |