Hostname: page-component-cd9895bd7-fscjk Total loading time: 0 Render date: 2024-12-22T14:53:41.922Z Has data issue: false hasContentIssue false
  • English
  • Français

Cuts, consistency statements and interpretations

Published online by Cambridge University Press:  12 March 2014

Pavel Pudlák
Pavel Pudlák*
Affiliation:
Mathematical Institute, Czechoslovak Academy of Sciences, 115 67 Prague 1, Czechoslovakia
Get access Rights & Permissions [Opens in a new window]

Extract

Interpretability in reflexive theories, especially in PA, has been studied in many papers; see e.g. [3], [6], [7], [10], [11], [15], [26]. It has been shown that reflexive theories exhibit many nice properties, e.g. (1) if T, S are recursively enumerable reflexive, then T is interpretable in S iff every Π1 sentence provable in T is provable in S; and (2) if S is reflexive, T is recursively enumerable and locally interpretable in S (i.e. every finite part of T is interpretable in S), then T is globally interpretable in S (Orey's theorem, cf. [3]).

In this paper we want to study such statements for nonreflexive theories, especially for finitely axiomatizable theories (which are never reflexive). These theories behave differently, although they may be quite close to reflexive theories, as e.g. GB to ZF. An important fact is that in such theories one can define proper cuts. By a cut we mean a formula with one free variable which defines a nonempty initial segment of natural numbers closed under the successor function. The importance of cuts for interpretations in GB was realized already by Vopěnka and Hájek in [30]. Pioneering work was done by Solovay in [24]. There he developed the method of “shortening of cuts”. Using this method it is possible to replace any cut by a cut which is contained in it and has some desirable additional properties; in particular it can be closed under + and ·. This introduces ambiguity in the concept of arithmetic in theories which admit proper cuts, namely, which cut (closed under + and ·) should be called the arithmetic of the theory? Cuts played the crucial role also in [20].

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 50 , Issue 2 , June 1985 , pp. 423 - 441
Copyright
Copyright © Association for Symbolic Logic 1985

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]Bezboruah, A. and Shepherdson, J. C., Gödel's second incompleteness theorem for Q, this Journal, vol. 41 (1976), pp. 503–512.Google Scholar
[2]Dimitracopoulos, C., Matijasevič's theorem andfragments of arithmetic, Ph.D. Thesis, University of Manchester, Manchester, 1980.Google Scholar
[3]Feferman, S., Arithmetization of metamathematics in a general setting, Fundamenta Mathematicae, vol. 49 (1960), pp. 35–92.CrossRefGoogle Scholar
[4]Gaifman, H. and Dimitracopoulos, C., Fragments of Peano's arithmetic and the MRDP theorem, Logic and algorithmic (Zürich, 1980), Monographies de l'Enseignement Mathématique, no. 30, Université de Genève, Geneva, 1982, pp. 187–206.Google Scholar
[5]Hájek, P., On a new notion of partial consevativity, Logic Colloquium '83, North-Holland, Amsterdam (to appear).Google Scholar
[6]Hájková, M. and Hájek, P., On interpretability in theories containing arithmetic, Fundamenta Mathematicae, vol. 76 (1972), pp. 131–137.CrossRefGoogle Scholar
[7]Jeroslow, R. G., Consistency statements in formal theories, Fundamenta Mathematicae, vol. 72 (1971), pp. 17–40.CrossRefGoogle Scholar
[8]Jeroslow, R. G., Redundancies in the Hilbert-Bernays derivability conditions for Gödel's second incompleteness theorem, this Journal, vol. 38 (1973), pp. 359–367.Google Scholar
[9]Kleene, S. C., Mathematical logic, Wiley, New York, 1967.Google Scholar
[10]Lindström, P., Some results on interpretability, Proceedings of the Fifth Scandinavian Logic Symposium (Jensen, F. V., Mayoh, B. H. and Møller, K. K., editors), Aalborg University Press, Aalborg, 1979, pp. 329–361.Google Scholar
[11]Lindström, P., On certain lattices of degrees of interpretability, Notre Dame Journal of Formal Logic, vol. 25 (1984), pp. 127–140.CrossRefGoogle Scholar
[12]Mycielski, J., A lattice of interpretability types of theories, this Journal, vol. 42 (1977), pp. 297–305.Google Scholar
[13]Mycielski, J., Finitistic intuitions supporting the consistency of ZF and ZF + AD, this Journal (to appear).Google Scholar
[14]Orévkov, V. P., Lower bounds for lengthening of proofs after cut elimination, Zapiski Naučnyh Séminarov LOMI, vol. 88 (1979), pp. 137–162; English translation, Journal of Soviet Mathematics, vol. 20 (1982), pp. 2337–2350.Google Scholar
[15]Orey, S., Relative interpretations, Zeitschrift für Mathematische Logic und Grundlagen der Mathematik, vol. 7 (1961), pp. 146–153.CrossRefGoogle Scholar
[16]Parikh, R., Existence and feasibility in arithmetic, this Journal, vol. 36 (1971), pp. 494–508.Google Scholar
[17]Paris, J. B. and Dimitracopoulos, C., A note on the undefinability of cuts, this Journal, vol. 48 (1983), pp. 564–569.Google Scholar
[18]Paris, J. B. and Wilkie, A., ⊿00 sets and induction, preprint.Google Scholar
[19]Pudlák, P., A definition of exponentiation by a bounded arithmetical formula, Commentationes Mathematicae Universitatis Carolinae, vol. 24 (1983), pp. 667–671.Google Scholar
[20]Pudlák, P., Some prime elements in the lattice of interpretability types, Transactions of the American Mathematical Society, vol. 280 (1983), pp. 255–275.CrossRefGoogle Scholar
[21]Schwichtenberg, H., Some applications of cut-elimination, Handbook of mathematical Logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 867–895.CrossRefGoogle Scholar
[22]Shoenfield, J. R., Mathematical logic, Addison-Wesley, Reading, Massachusetts, 1967.Google Scholar
[23]Smoryński, C., The incompleteness theorem, Handbook of mathematical logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 821–865.CrossRefGoogle Scholar
[24]Solovay, R., Letter to P. Hájek, August, 1976. (A proof that there exists a Π 10 sentence Φ such that ZF + Φ is not interpretable in ZF, yet GB + Φ is interpretable in GB. See Hájek, P., On interpretability of theories containing arithmetic. II, Commentationes Mathematicae Universitatis Carolinae, vol. 22 (1981), pp. 667–688.)Google Scholar
[25]Statman, R., Bounds for proof search and speed-up in the predicate calculus, Annals of Mathematical Logic, vol. 15 (1978), pp. 225–287.CrossRefGoogle Scholar
[26]Švejdar, V., Degrees of interpretability, Commentationes Mathematicae Universitatis Carolinae, vol. 19 (1978), pp. 789–813.Google Scholar
[27]Švejdar, V., Modal analysis of generalized Rosser sentences, this Journal, vol. 48 (1983), pp. 986–999.Google Scholar
[28]Tarski, A., Mostowski, A. and Robinson, R. M., Undecidable theories, North-Holland, Amsterdam, 1953.Google Scholar
[29]Vaught, R., Axiomatizability by a schema, this Journal, vol. 32 (1967), pp. 473–479.Google Scholar
[30]Vopěnka, P. and Hájek, P., Existence of a generalized semantic model of Gödel-Bernays set theory, Bulletin de l'Académie Polonaise des Sciences, Série des Sciences Mathématiques, Astronomiques et Physiques, vol. 12 (1973), pp. 1079–1086.Google Scholar