Hostname: page-component-78c5997874-t5tsf Total loading time: 0 Render date: 2024-11-07T17:31:40.401Z Has data issue: false hasContentIssue false

On the consistency of an impredicative subsystem of Quine's NF

Published online by Cambridge University Press:  12 March 2014

Marcel Crabbé*
Affiliation:
Université de Louvain (U.C.L.), Institut Supérieur de Philosophie, Louvain-La-Neuve, Belgium

Extract

NFP is the predicative fragment of NF. In this system we do not allow a set to exist if it cannot be defined without using quantifiers ranging over its type or parameters of a higher type. NFI is a less restrictive fragment located between NFP and NF.

We show that NFP is really weaker than NFI; similarly, NFI is weaker than NF. This result will be obtained in the following manner: on the one hand, we will show that NFP can be proved consistent in elementary arithmetic and that second order arithmetic is interpretable in NFI; on the other hand, we will prove the consistency of NFI in third order arithmetic, which is contained in NF.

The paper is divided in four sections. In §1, we define the concepts needed and collect a few results together in such a way that they will be ready for later use. In §2, we will present a model-theoretic (quick) proof of the consistency of NFI (and thus of NFP). The proof will be chosen (it is not the quickest!) so as to motivate in a natural manner the details of the proof-theoretical version of it that will be presented in §3. §4 will be devoted to the axiom of infinity in NFP and NFI.

Type
Research Article
Copyright
Copyright © Association for Symbolic Logic 1982

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, M., A reduction of the theory of types, Set theory and hierarchy theory, Bierutowice, Lecture Notes in Mathematics, vol. 619, Springer-Verlag, Berlin and New York, 1977, pp. 95100.CrossRefGoogle Scholar
[2]Boffa, M., The consistency problem for NF, this Journal, vol. 42 (1977), pp. 215219.Google Scholar
[3]Boffa, M. and Crabbé, M., Les théorèmes 3-stratifiés de NF3, Comptes Rendus de l'Académie des Sciences de Paris, vol. 280 (1975), pp. 16571658.Google Scholar
[4]Crabbé, M., Types ambigus, Comptes Rendus de l'Académie des Sciences de Paris, vol. 280 (1975), pp. 12.Google Scholar
[5]Crabbé, M., La prédicativité dans les théories élémentaires, Logique et Analyse, No. 74–75–76 (1976), pp. 255266.Google Scholar
[6]Crabbé, M., Ambiguity and stratification, Fundamenta Mathematicae, vol. 101 (1978), pp. 1117.CrossRefGoogle Scholar
[7]Fraenkel, A., Bar-Hillel, Y. and Levy, A., Foundations of set theory, North-Holland, Amsterdam, 1973.Google Scholar
[8]Grishin, V. N., Consistency of a fragment of Quine's NF system, Soviet Mathematics Doklady, vol. 10(1969), pp. 13871390.Google Scholar
[9]Grishin, V. N., The method of stratification in set theory, Thesis, Academy of Science of U.S.S.R., Moscow, 1973 (Russian).Google Scholar
[10]Oswald, U., Fragmente von “New-Foundations” und Typentheorie, Thesis, E.T.H., Zürich, 1976.Google Scholar
[11]Quine, W.V.O., Set theory and its logic, Harvard University Press, Cambridge, Massachusetts, 1963.CrossRefGoogle Scholar
[12]Specker, E., The axiom of choice in Quine's New Foundations for mathematical logic, Proceedings of the National Academy of Science of the United States of America, vol. 39(1953), pp. 972975.CrossRefGoogle Scholar
[13]Specker, E., Typical ambiguity, Logic, methodology and philosophy of science, Proceedings of the 1960 International Congress, Stanford, 1962, pp. 116124.Google Scholar
[14]Tait, W.W., A non constructive proof of Gentzen's Hauptsatz for second order predicate logic, Bulletin of the American Mathematical Society, vol. 72 (1966), pp. 980983.CrossRefGoogle Scholar
[15]Takeuti, G., Proof theory, North-Holland, Amsterdam, 1975.Google Scholar