The Interpretation Existence Lemma

  • Albert Visser
Part of the Outstanding Contributions to Logic book series (OCTR, volume 13)


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.


Interpretations Degrees Sequential theories 

2000 Mathematics Subject Classification:

03A05 03B25 03F45 


  1. 1.
    Boolos, G.S., Burgess, J.P., Jeffrey, R.C.: Computability and Logic, 4th edn. Cambridge University Press, Cambridge (2002)CrossRefzbMATHGoogle Scholar
  2. 2.
    Buss, S.R.: Bounded Arithmetic. Bibliopolis, Napoli (1986)zbMATHGoogle Scholar
  3. 3.
    Buss, S.: Cut elimination in situ. In: Kahle, R., Rathjen, M. (eds.) Gentzen’s Centenary, pp. 245–277. Springer International Publishing, Berlin (2015)CrossRefGoogle Scholar
  4. 4.
    Ebbs, G.: Satisfying predicates: Kleene’s proof of the Hilbert–Bernays theorem. Hist. Philos. Log. 36(4), 1–21 (2014)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Feferman, S.: Arithmetically definable models of formalized arithmetic. Notices of the American Mathematical Society 5, 679–680 (1958)Google Scholar
  6. 6.
    Feferman, S.: Arithmetization of metamathematics in a general setting. Fund. Math. 49, 35–92 (1960)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Feferman, S.: My route to arithmetization. Theoria 63(3), 168–181 (1997)MathSciNetCrossRefGoogle Scholar
  8. 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. 9.
    Gerhardy, P.: The role of quantifier alternations in cut elimination. Notre Dame J. Form. Log. 46(2), 165–171 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Gödel, K.: Die Vollständigkeit der Axiome des logischen Funktionenkalküls. Monatshefte für Mathematik 37(1), 349–360 (1930)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Hájek, P.: On interpretability in set theories I. Comm. Math. Univ. Carolinae 12, 73–79 (1971)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Hájek, P.: On interpretability in set theories II. Comm. Math. Univ. Carolinae 13, 445–455 (1972)MathSciNetzbMATHGoogle Scholar
  13. 13.
    Hilbert, D., Bernays, P.: Grundlagen der Mathematik II. Springer, Berlin (1939). Second edition: 1970zbMATHGoogle Scholar
  14. 14.
    Henkin, L.: The completeness of the first-order functional calculus. J. Symb. Log. 14(03), 159–166 (1949)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Hájková, M., Hájek, P.: On interpretability in theories containing arithmetic. Fund. Math. 76(2), 131–137 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Hájek, P., Pudlák, P.: Metamathematics of First-Order Arithmetic. Perspectives in Mathematical Logic. Springer, Berlin (1993)CrossRefzbMATHGoogle Scholar
  17. 17.
    Jeřábek, E.: Sequence encoding without induction. Math. Log. Q. 58(3), 244–248 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Kaye, R.: Models of Peano Arithmetic. Oxford Logic Guides. Oxford University Press, Oxford (1991)zbMATHGoogle Scholar
  19. 19.
    Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)zbMATHGoogle Scholar
  20. 20.
    Krajíček, J.: A note on proofs of falsehood. Archiv für Mathematische Logik und Grundlagenforschung 26(1), 169–176 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Kossak, R., Schmerl, J.: The Structure of Models of Peano Arithmetic. Clarendon Press, Oxford (2006)CrossRefzbMATHGoogle Scholar
  22. 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. 23.
    Löwenheim, L.: Über möglichkeiten im Relativkalkül. Math. Ann. 76(4), 447–470 (1915)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 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. 25.
    Nelson, E.: Predicative Arithmetic. Princeton University Press, Princeton (1986)CrossRefzbMATHGoogle Scholar
  26. 26.
    Orey, S.: Relative interpretations. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 7, 146–153 (1961)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Pudlák, P.: Some prime elements in the lattice of interpretability types. Trans. Am. Math. Soc. 280, 255–275 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Pudlák, P.: Cuts, consistency statements and interpretations. J. Symb. Log. 50(2), 423–441 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Putnam, H.: Trial and error predicates and a solution to a problem of Mostowski. J. Symb. Log. 30(1), 146–153 (1965)MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Schmerl, J.H.: End extensions of models of arithmetic. Notre Dame J. Form. Log. 33(2), 216–219 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Scott, D.: On a theorem of Rabin. Indagationes Mathematicae (Proceedings) 63, 481–484 (1960)Google Scholar
  32. 32.
    Simpson, S.G.: Subsystems of Second Order Arithmetic. Perspectives in Logic: Association for Symbolic Logic, 2nd edn. Cambridge University Press, Cambridge (2009)CrossRefzbMATHGoogle Scholar
  33. 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)CrossRefGoogle Scholar
  34. 34.
    Solovay, R.M.: Interpretability in set theories. Unpublished letter to P. Hájek. (1976)
  35. 35.
    Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press, Cambridge (2000)CrossRefzbMATHGoogle Scholar
  36. 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. 37.
    Visser, A.: The formalization of interpretability. Stud. Log. 51(1), 81–105 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  38. 38.
    Visser, A.: The unprovability of small inconsistency. Arch. Math. Log. 32(4), 275–298 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  39. 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)CrossRefGoogle Scholar
  40. 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. 41.
    Visser, A.: Pairs, sets and sequences in first order theories. Arch. Math. Log. 47(4), 299–326 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  42. 42.
    Visser, A.: Cardinal arithmetic in the style of Baron von Münchhausen. Review of Symbolic Logic 2(3), 570–589 (2009).
  43. 43.
    Visser, A.: Hume’s principle, beginnings. Rev. Symb. Log. 4(1), 114–129 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  44. 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. 45.
    Visser, A.: Interpretability degrees of finitely axiomatized sequential theories. Arch. Math. Log. 53(1–2), 23–42 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  46. 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. (2014)
  47. 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.
  48. 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. 49.
    Visser, A.: Transductions in arithmetic. Ann. Pure Appl. Log. 167(3), 211–234 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  50. 50.
    Wang, H.: Arithmetic translations of axiom systems. Trans. Am. Math. Soc. 71, 283–293 (1951)MathSciNetCrossRefzbMATHGoogle Scholar
  51. 51.
    Wang, H.: Arithmetical models for formal systems. Methodos 3, 217–232 (1951)MathSciNetGoogle Scholar
  52. 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)CrossRefGoogle Scholar
  53. 53.
    Wilkie, A.J., Paris, J.B.: On the scheme of induction for bounded arithmetic formulas. Ann. Pure Appl. Log. 35, 261–302 (1987)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2017

Authors and Affiliations

  1. 1.Philosophy, Faculty of HumanitiesUtrecht UniversityUtrechtThe Netherlands

Personalised recommendations