Hostname: page-component-78c5997874-mlc7c Total loading time: 0 Render date: 2024-11-19T02:10:36.116Z Has data issue: false hasContentIssue false
  • English
  • Français

Stratification and cut-elimination

Published online by Cambridge University Press:  12 March 2014

Marcel Crabbé
Marcel Crabbé*
Affiliation:
Département de Philosophie, Université de Louvain, B-1348 Louvain-la-Neuve, Belgium
Get access Rights & Permissions [Opens in a new window]

Extract

In this paper, we show the normalization of proofs of NF (Quine's New Foundations; see [15]) minus extensionality. This system, called SF (Stratified Foundations) differs in many respects from the associated system of simple type theory. It is written in a first order language and not in a multi-sorted one, and the formulas need not be stratifiable, except in the instances of the comprehension scheme. There is a universal set, but, for a similar reason as in type theory, the paradoxical sets cannot be formed.

It is not immediately apparent, however, that SF is essentially richer than type theory. But it follows from Specker's celebrated result (see [16] and [4]) that the stratifiable formula (extensionality → the universe is not well-orderable) is a theorem of SF.

It is known (see [11]) that this set theory is consistent, though the consistency of NF is still an open problem.

The connections between consistency and cut-elimination are rather loose. Cut-elimination generally implies consistency. But the converse is not true. In the case of set theory, for example, ZF-like systems, though consistent, cannot be freed of cuts because the separation axioms allow the formation of sets from unstratifiable formulas. There are nevertheless interesting partial results obtained when restrictions are imposed on the removable cuts (see [1] and [9]). The systems with stratifiable comprehension are the only known set-theoretic systems that enjoy full cut-elimination.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 56 , Issue 1 , March 1991 , pp. 213 - 226
Copyright
Copyright © Association for Symbolic Logic 1991

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]Bailin, S. C., A normalization theorem for set theory, this Journal, vol. 53 (1988), pp. 673–695.Google Scholar
[2]Bourbaki, N., Éléments de mathématique. Livre I: Théorie des ensembles, 3rd ed., Hermann, Paris, 1958.Google Scholar
[3]Crabbé, M., Ambiguity and stratification, Fundamenta Mathematicae, vol. 101 (1978), pp. 11–17.CrossRefGoogle Scholar
[4]Crabbé, M., Typical ambiguity and the axiom of choice, this Journal, vol. 49 (1984), pp. 1074–1078.Google Scholar
[5]Curry, H. B. and Feys, R., Combinatory logic, North-Holland, Amsterdam, 1968.Google Scholar
[6]de Bruijn, N. G., Lambda calculus notation with nameless dummies, a tool for automatic manipulation, with application to the Church-Rosser theorem, Indagationes Mathematicae, vol. 34 (1972), pp. 391–392.Google Scholar
[7]Girard, J. Y., Une extension de l'interprétation de Gödel à l'analyse, et son application á l'élimination des coupures dans l'analyse et la théorie des types, Proceedings of the second Scandinavian logic symposium (Fenstad, J. E., editor), North-Holland, Amsterdam, 1971, pp. 63–92.CrossRefGoogle Scholar
[8]Girard, J. Y., Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, Thèse, Université Paris-VII, Paris, 1972.Google Scholar
[9]Hallnäs, L., On normalization of proofs in set theory, Ph.D. thesis, University of Stockholm, Stockholm, 1983.Google Scholar
[10]Howard, W., The formulae-as-types notion of construction, To H. B. Curry: essays on combinatory logic, lambda calculus and formalism (Seldin, J. R. and Hindley, J. R., editors), Academic Press, New York, 1980, pp. 479–490.Google Scholar
[11]Jensen, R. B., On the consistency of a slight (?) modification of NF, Synthese, vol. 19 (1968–1969), pp. 250–263.CrossRefGoogle Scholar
[12]Martin-Löf, P., Hauptsatz for the theory of species, Proceedings of the second Scandinavian logic symposium (Fenstad, J. E., editor), North-Holland, Amsterdam, 1971, pp. 217–233.CrossRefGoogle Scholar
[13]Prawitz, D., Natural deduction, Almqvist & Wiksell, Stockholm, 1965.Google Scholar
[14]Prawitz, D., Ideas and results in proof theory, Proceedings of the second Scandinavian logic symposium (Fenstad, J. E., editor), North-Holland, Amsterdam, 1971, pp. 235–307.CrossRefGoogle Scholar
[15]Quine, W. V. O., New foundations for mathematical logic, American Mathematical Monthly, vol. 40 (1937), pp. 70–80; reprinted in From a logical point of view, Harvard University Press, Cambridge, Massachusetts, 1953, pp. 80–101; rev. ed., Harper & Row, New York, 1961, pp. 80–101.CrossRefGoogle Scholar
[16]Specker, E., The axiom of choice in Quine's “New foundations for mathematical logic”, Proceedings of the National Academy of Sciences of the United States of America, vol. 39 (1953), pp. 972–975.CrossRefGoogle Scholar
[17]Specker, E., Typical ambiguity, Logic, methodology and the philosophy of science (Nagel, E.et al., editors), Stanford University Press, Stanford, California, 1962, pp. 117–124.Google Scholar
[18]Tait, W. W., Intensional interpretation of functionals of finite type, this Journal, vol. 32 (1967), pp. 198–212.Google Scholar
[19]Tait, W. W., A realizability interpretation of the theory of species, Logic Colloquium (Boston, Massachusetts, 1972/73), Lecture Notes in Mathematics, vol. 453, Springer-Verlag, Berlin, 1975, pp. 240–251.CrossRefGoogle Scholar