Skip to main content
SpringerLink
Log in
Book cover

Feferman on Foundations pp 101–144Cite as

The Interpretation Existence Lemma

  • Chapter
  • First Online:

Part of the book series: Outstanding Contributions to Logic ((OCTR,volume 13))

Abstract

The present paper contains a fairly detailed verification of a reasonably general form of the Interpretation Existence Lemma. In first approximation, this lemma tells us that if a theory U proves the consistency of V then U interprets V. What are theories here? What is proving the consistency of V in this context? The paper will explain how the lemma works, providing rather general answers to these questions. We apply the Interpretation Existence Lemma to verify well-known characterization theorems for interpretability: the Friedman Characterization and the Orey–Hájek Characterization. Finally, we provide three randomly chosen examples of application of the Interpretation Existence Lemma.

I am grateful to Ali Enayat, Paula Henk and Volodya Shavrukov for helpful comments, references and scholarly support. I thank the anonymous referee for his/her suggestions.

This is a preview of subscription content, log in via an institution.

Notes

  1. 1.

    My most extensive earlier attempt to give a presentation of the proof was in [37]. However, the present one gives more detail and isolates the special features of the construction in a better way.

  2. 2.

    One-dimensional means that the formula representing the object domain of the interpretation just has one free variable, apart from variables serving as parameters. See Sect. 2.2.

  3. 3.

    Alternatively, we could start from the theory \(\mathsf{PA}^-\).

  4. 4.

    The verification of the equivalence between axioms-interpretability and theorems-interpretability demands \(\Sigma _1\)-collection. See [37] for more details.

  5. 5.

    Here we restrict ourselves to the case without parameters. We can add parameters to the definition in different ways, either by employing a parameter domain or by stipulating parameters locally for each model. These ways are more closely connected than one would think thanks to the Omitting Types Theorem. One can find examples of theories U and V, where V model-interprets U with parameters but does not do so without parameters.

  6. 6.

    In my forthcoming paper Restricted Theories, I will treat the various properties of the complexity measure in more detail.

  7. 7.

    We note that in the case of many sorted theories, we need to use a standard translation into a one-sorted theory to apply the definition.

  8. 8.

    Our Sect. 4.2 contains a bit more detail on the construction of satisfaction predicates.

  9. 9.

    The induction axioms are only for the original language of arithmetic.

  10. 10.

    For the notion of synonymity of theories, see e.g. [40].

  11. 11.

    I choose for this representation of \(P_\eta \) since it contains no ambiguities. One would like to say that \(P_\tau (x_0,\cdots ,x_{n-1})\) is \(P (c_0,\cdots ,c_{n-1}) \in \Delta ^\star \), were the \(c_i\) are the \(x_i\).

  12. 12.

    We are a bit sloppy, since the finite set need not have a unique code. The insight works for every code of the displayed set.

  13. 13.

    We allow the domain D to be empty. We consider the the empty relation to be an equivalence relation on the empty set.

  14. 14.

    In \(\mathsf{S}^1_2\), the supremum of the elements of a sequence always exists. However, we do not need that insight for the present definition to be meaningful.

  15. 15.

    We remind the reader that we allow axiomatizations of any complexity.

  16. 16.

    We treat the A in the subscript of \( \Diamond _{\alpha ,A,n}\) as the number bounding the axiom of the theory A, which is par abus de langage, again A.

  17. 17.

    It would be more natural to work with the theory \(\mathsf{FC}_\infty \) with class-variables for any arity. However, this would not fit with our policy to only consider finite signatures.

  18. 18.

    Regrettably, I do not have a reference for the argument in full generality. It is proven for the case of \(\mathsf{ACA}_0\) in [32, pp. 311–312]. However, the argument there does not easily lift to the general case.

  19. 19.

    We do have, by a direct application of the Interpretation Existence Lemma, that there is a large class of models \(\mathcal M\) that have a parametric internal strict end-extension \(\mathcal N\) that is elementarily equivalent to \(\mathcal M\). In fact, the recursively saturated models are in this class. So, the difference between elementary extension and extension that is elementarily equivalent is essential in the extended Feferman-Scott result. An open end in our story is that it is unclear whether there is a model \(\mathcal M\) with a parameter-free internal model \(\mathcal N\) that is a strict end-extension and elementarily equivalent to \(\mathcal M\).

References

  1. Boolos, G.S., Burgess, J.P., Jeffrey, R.C.: Computability and Logic, 4th edn. Cambridge University Press, Cambridge (2002)

    Book  MATH  Google Scholar 

  2. Buss, S.R.: Bounded Arithmetic. Bibliopolis, Napoli (1986)

    MATH  Google Scholar 

  3. Buss, S.: Cut elimination in situ. In: Kahle, R., Rathjen, M. (eds.) Gentzen’s Centenary, pp. 245–277. Springer International Publishing, Berlin (2015)

    Chapter  Google Scholar 

  4. Ebbs, G.: Satisfying predicates: Kleene’s proof of the Hilbert–Bernays theorem. Hist. Philos. Log. 36(4), 1–21 (2014)

    MathSciNet  MATH  Google Scholar 

  5. Feferman, S.: Arithmetically definable models of formalized arithmetic. Notices of the American Mathematical Society 5, 679–680 (1958)

    Google Scholar 

  6. Feferman, S.: Arithmetization of metamathematics in a general setting. Fund. Math. 49, 35–92 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  7. Feferman, S.: My route to arithmetization. Theoria 63(3), 168–181 (1997)

    Article  MathSciNet  Google Scholar 

  8. Gerhardy, P.: Refined complexity analysis of cut elimination. In: Baaz, M., Makowsky, J. (eds.) Proceedings of the 17th International Workshop CSL 2003. LNCS, vol. 2803, pp. 212–225. Springer, Berlin (2003)

    Google Scholar 

  9. Gerhardy, P.: The role of quantifier alternations in cut elimination. Notre Dame J. Form. Log. 46(2), 165–171 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  10. Gödel, K.: Die Vollständigkeit der Axiome des logischen Funktionenkalküls. Monatshefte für Mathematik 37(1), 349–360 (1930)

    Article  MathSciNet  MATH  Google Scholar 

  11. Hájek, P.: On interpretability in set theories I. Comm. Math. Univ. Carolinae 12, 73–79 (1971)

    MathSciNet  MATH  Google Scholar 

  12. Hájek, P.: On interpretability in set theories II. Comm. Math. Univ. Carolinae 13, 445–455 (1972)

    MathSciNet  MATH  Google Scholar 

  13. Hilbert, D., Bernays, P.: Grundlagen der Mathematik II. Springer, Berlin (1939). Second edition: 1970

    MATH  Google Scholar 

  14. Henkin, L.: The completeness of the first-order functional calculus. J. Symb. Log. 14(03), 159–166 (1949)

    Article  MathSciNet  MATH  Google Scholar 

  15. Hájková, M., Hájek, P.: On interpretability in theories containing arithmetic. Fund. Math. 76(2), 131–137 (1972)

    Article  MathSciNet  MATH  Google Scholar 

  16. Hájek, P., Pudlák, P.: Metamathematics of First-Order Arithmetic. Perspectives in Mathematical Logic. Springer, Berlin (1993)

    Book  MATH  Google Scholar 

  17. Jeřábek, E.: Sequence encoding without induction. Math. Log. Q. 58(3), 244–248 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  18. Kaye, R.: Models of Peano Arithmetic. Oxford Logic Guides. Oxford University Press, Oxford (1991)

    MATH  Google Scholar 

  19. Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)

    MATH  Google Scholar 

  20. Krajíček, J.: A note on proofs of falsehood. Archiv für Mathematische Logik und Grundlagenforschung 26(1), 169–176 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  21. Kossak, R., Schmerl, J.: The Structure of Models of Peano Arithmetic. Clarendon Press, Oxford (2006)

    Book  MATH  Google Scholar 

  22. Lindström, P.: Some results on interpretability. In: Jensen, F.V., Mayoh, B.H., Møller, K.K. (eds.) Proceedings of the 5th Scandinavian Logic Symposium 1979, pp. 329–361. Aalborg University Press, Aalborg (1979)

    Google Scholar 

  23. Löwenheim, L.: Über möglichkeiten im Relativkalkül. Math. Ann. 76(4), 447–470 (1915)

    Article  MathSciNet  MATH  Google Scholar 

  24. Mycielski, J., Pudlák, P., Stern, A.S.: A lattice of chapters of mathematics (interpretations between theorems). Memoirs of the American Mathematical Society, vol. 84. AMS, Providence (1990)

    Google Scholar 

  25. Nelson, E.: Predicative Arithmetic. Princeton University Press, Princeton (1986)

    Book  MATH  Google Scholar 

  26. Orey, S.: Relative interpretations. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 7, 146–153 (1961)

    Article  MathSciNet  MATH  Google Scholar 

  27. Pudlák, P.: Some prime elements in the lattice of interpretability types. Trans. Am. Math. Soc. 280, 255–275 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  28. Pudlák, P.: Cuts, consistency statements and interpretations. J. Symb. Log. 50(2), 423–441 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  29. Putnam, H.: Trial and error predicates and a solution to a problem of Mostowski. J. Symb. Log. 30(1), 146–153 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  30. Schmerl, J.H.: End extensions of models of arithmetic. Notre Dame J. Form. Log. 33(2), 216–219 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  31. Scott, D.: On a theorem of Rabin. Indagationes Mathematicae (Proceedings) 63, 481–484 (1960)

    Google Scholar 

  32. Simpson, S.G.: Subsystems of Second Order Arithmetic. Perspectives in Logic: Association for Symbolic Logic, 2nd edn. Cambridge University Press, Cambridge (2009)

    Book  MATH  Google Scholar 

  33. Smoryński, C.: Nonstandard models and related developments. In: Harrington, L.A., Morley, M.D., Scedrov, A., Simpson, S.G. (eds.) Harvey Friedman’s Research on the Foundations of Mathematics, pp. 179–229. North Holland, Amsterdam (1985)

    Chapter  Google Scholar 

  34. Solovay, R.M.: Interpretability in set theories. Unpublished letter to P. Hájek. http://www.cs.cas.cz/hajek/RSolovayZFGB.pdf (1976)

  35. Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press, Cambridge (2000)

    Book  MATH  Google Scholar 

  36. Visser, A.: Interpretability logic. In: Petkov, P.P. (ed.) Mathematical logic. Proceedings of the Heyting 1988 Summer School in Varna, Bulgaria, pp. 175–209. Plenum Press, Boston (1990)

    Google Scholar 

  37. Visser, A.: The formalization of interpretability. Stud. Log. 51(1), 81–105 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  38. Visser, A.: The unprovability of small inconsistency. Arch. Math. Log. 32(4), 275–298 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  39. Visser, A.: Faith & Falsity: a study of faithful interpretations and false \({\Sigma }^0_1\)-sentences. Ann. Pure Appl. Log. 131(1–3), 103–131 (2005)

    Article  Google Scholar 

  40. Visser, A.: Categories of theories and interpretations. In: Enayat, A., Kalantari, I., Moniri, M. (eds.) Logic in Tehran. Proceedings of the Workshop and Conference on Logic, Algebra and Arithmetic, held 18–22 October 2003. Lecture Notes in Logic, vol. 26, pp. 284–341. ASL, A.K. Peters Ltd., Wellesley, Mass (2006)

    Google Scholar 

  41. Visser, A.: Pairs, sets and sequences in first order theories. Arch. Math. Log. 47(4), 299–326 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  42. Visser, A.: Cardinal arithmetic in the style of Baron von Münchhausen. Review of Symbolic Logic 2(3), 570–589 (2009). https://doi.org/10.1017/S1755020309090261

  43. Visser, A.: Hume’s principle, beginnings. Rev. Symb. Log. 4(1), 114–129 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  44. Visser, A.: What is sequentiality? In: Cégielski, P., Cornaros, Ch., Dimitracopoulos, C. (eds.) New Studies in Weak Arithmetics. CSLI Lecture Notes, vol. 211, pp. 229–269. CSLI Publications and Presses Universitaires du Pôle de Recherche et d’Enseingement Supérieur Paris-est, Stanford (2013)

    Google Scholar 

  45. Visser, A.: Interpretability degrees of finitely axiomatized sequential theories. Arch. Math. Log. 53(1–2), 23–42 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  46. Visser, A.: The interpretability of inconsistency, Feferman’s theorem and related results. Logic Group Preprint Series 318, Faculty of Humanities, Philosophy, Utrecht University, Janskerkhof 13, 3512 BL Utrecht. http://www.phil.uu.nl/preprints/lgps/ (2014)

  47. Visser, A.: Why the theory R is special. In: Tennant, N. (ed.) Foundational Adventures. Essays in honour of Harvey Friedman, pp. 7–23. College Publications, UK (2014). Originally published online by Templeton Press in 2012. http://foundationaladventures.com/

  48. Visser, A.: On Q. Soft Comput. 1–18 (2016). Special issue in memoriam Franco Montagna (A. Di Nola, D. Mundici, C. Toffalori, A. Ursini, eds.)

    Google Scholar 

  49. Visser, A.: Transductions in arithmetic. Ann. Pure Appl. Log. 167(3), 211–234 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  50. Wang, H.: Arithmetic translations of axiom systems. Trans. Am. Math. Soc. 71, 283–293 (1951)

    Article  MathSciNet  MATH  Google Scholar 

  51. Wang, H.: Arithmetical models for formal systems. Methodos 3, 217–232 (1951)

    MathSciNet  Google Scholar 

  52. Wilkie, A.J.: On the theories of end-extensions of models of arithmetic. Set Theory and Hierarchy Theory V, pp. 305–310. Springer, Berlin (1977)

    Chapter  Google Scholar 

  53. Wilkie, A.J., Paris, J.B.: On the scheme of induction for bounded arithmetic formulas. Ann. Pure Appl. Log. 35, 261–302 (1987)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Philosophy, Faculty of Humanities, Utrecht University, Janskerkhof 13, 3512BL, Utrecht, The Netherlands

    Albert Visser

Authors
  1. Albert Visser
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Albert Visser .

Editor information

Editors and Affiliations

  1. Institut für Informatik, Universität Bern, Bern, Switzerland

    Gerhard Jäger

  2. Department of Philosophy, Carnegie Mellon University Dept. Philosophy, Pittsburgh, Pennsylvania, USA

    Wilfried Sieg

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Visser, A. (2017). The Interpretation Existence Lemma. In: Jäger, G., Sieg, W. (eds) Feferman on Foundations. Outstanding Contributions to Logic, vol 13. Springer, Cham. https://doi.org/10.1007/978-3-319-63334-3_5

Download citation

Publish with us

Policies and ethics

Search

Navigation