The Interpretation Existence Lemma

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)CrossRefMATHGoogle Scholar
  2. 2.
    Buss, S.R.: Bounded Arithmetic. Bibliopolis, Napoli (1986)MATHGoogle 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)MathSciNetMATHGoogle 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)MathSciNetCrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle Scholar
  10. 10.
    Gödel, K.: Die Vollständigkeit der Axiome des logischen Funktionenkalküls. Monatshefte für Mathematik 37(1), 349–360 (1930)MathSciNetCrossRefMATHGoogle Scholar
  11. 11.
    Hájek, P.: On interpretability in set theories I. Comm. Math. Univ. Carolinae 12, 73–79 (1971)MathSciNetMATHGoogle Scholar
  12. 12.
    Hájek, P.: On interpretability in set theories II. Comm. Math. Univ. Carolinae 13, 445–455 (1972)MathSciNetMATHGoogle Scholar
  13. 13.
    Hilbert, D., Bernays, P.: Grundlagen der Mathematik II. Springer, Berlin (1939). Second edition: 1970MATHGoogle Scholar
  14. 14.
    Henkin, L.: The completeness of the first-order functional calculus. J. Symb. Log. 14(03), 159–166 (1949)MathSciNetCrossRefMATHGoogle Scholar
  15. 15.
    Hájková, M., Hájek, P.: On interpretability in theories containing arithmetic. Fund. Math. 76(2), 131–137 (1972)MathSciNetCrossRefMATHGoogle Scholar
  16. 16.
    Hájek, P., Pudlák, P.: Metamathematics of First-Order Arithmetic. Perspectives in Mathematical Logic. Springer, Berlin (1993)CrossRefMATHGoogle Scholar
  17. 17.
    Jeřábek, E.: Sequence encoding without induction. Math. Log. Q. 58(3), 244–248 (2012)MathSciNetCrossRefMATHGoogle Scholar
  18. 18.
    Kaye, R.: Models of Peano Arithmetic. Oxford Logic Guides. Oxford University Press, Oxford (1991)MATHGoogle Scholar
  19. 19.
    Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)MATHGoogle Scholar
  20. 20.
    Krajíček, J.: A note on proofs of falsehood. Archiv für Mathematische Logik und Grundlagenforschung 26(1), 169–176 (1987)MathSciNetCrossRefMATHGoogle Scholar
  21. 21.
    Kossak, R., Schmerl, J.: The Structure of Models of Peano Arithmetic. Clarendon Press, Oxford (2006)CrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle 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)CrossRefMATHGoogle Scholar
  26. 26.
    Orey, S.: Relative interpretations. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 7, 146–153 (1961)MathSciNetCrossRefMATHGoogle Scholar
  27. 27.
    Pudlák, P.: Some prime elements in the lattice of interpretability types. Trans. Am. Math. Soc. 280, 255–275 (1983)MathSciNetCrossRefMATHGoogle Scholar
  28. 28.
    Pudlák, P.: Cuts, consistency statements and interpretations. J. Symb. Log. 50(2), 423–441 (1985)MathSciNetCrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle Scholar
  30. 30.
    Schmerl, J.H.: End extensions of models of arithmetic. Notre Dame J. Form. Log. 33(2), 216–219 (1992)MathSciNetCrossRefMATHGoogle 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)CrossRefMATHGoogle 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)CrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle Scholar
  38. 38.
    Visser, A.: The unprovability of small inconsistency. Arch. Math. Log. 32(4), 275–298 (1993)MathSciNetCrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle Scholar
  50. 50.
    Wang, H.: Arithmetic translations of axiom systems. Trans. Am. Math. Soc. 71, 283–293 (1951)MathSciNetCrossRefMATHGoogle 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)MathSciNetCrossRefMATHGoogle 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