# The Interpretation Existence Lemma

• Albert Visser
Chapter
Part of the Outstanding Contributions to Logic book series (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.

## Keywords

Interpretations Degrees Sequential theories

## 2000 Mathematics Subject Classification:

03A05 03B25 03F45

## References

1. 1.
Boolos, G.S., Burgess, J.P., Jeffrey, R.C.: Computability and Logic, 4th edn. Cambridge University Press, Cambridge (2002)
2. 2.
Buss, S.R.: Bounded Arithmetic. Bibliopolis, Napoli (1986)
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)
4. 4.
Ebbs, G.: Satisfying predicates: Kleene’s proof of the Hilbert–Bernays theorem. Hist. Philos. Log. 36(4), 1–21 (2014)
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)
7. 7.
Feferman, S.: My route to arithmetization. Theoria 63(3), 168–181 (1997)
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)
10. 10.
Gödel, K.: Die Vollständigkeit der Axiome des logischen Funktionenkalküls. Monatshefte für Mathematik 37(1), 349–360 (1930)
11. 11.
Hájek, P.: On interpretability in set theories I. Comm. Math. Univ. Carolinae 12, 73–79 (1971)
12. 12.
Hájek, P.: On interpretability in set theories II. Comm. Math. Univ. Carolinae 13, 445–455 (1972)
13. 13.
Hilbert, D., Bernays, P.: Grundlagen der Mathematik II. Springer, Berlin (1939). Second edition: 1970
14. 14.
Henkin, L.: The completeness of the first-order functional calculus. J. Symb. Log. 14(03), 159–166 (1949)
15. 15.
Hájková, M., Hájek, P.: On interpretability in theories containing arithmetic. Fund. Math. 76(2), 131–137 (1972)
16. 16.
Hájek, P., Pudlák, P.: Metamathematics of First-Order Arithmetic. Perspectives in Mathematical Logic. Springer, Berlin (1993)
17. 17.
Jeřábek, E.: Sequence encoding without induction. Math. Log. Q. 58(3), 244–248 (2012)
18. 18.
Kaye, R.: Models of Peano Arithmetic. Oxford Logic Guides. Oxford University Press, Oxford (1991)
19. 19.
Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)
20. 20.
Krajíček, J.: A note on proofs of falsehood. Archiv für Mathematische Logik und Grundlagenforschung 26(1), 169–176 (1987)
21. 21.
Kossak, R., Schmerl, J.: The Structure of Models of Peano Arithmetic. Clarendon Press, Oxford (2006)
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)
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)
26. 26.
Orey, S.: Relative interpretations. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 7, 146–153 (1961)
27. 27.
Pudlák, P.: Some prime elements in the lattice of interpretability types. Trans. Am. Math. Soc. 280, 255–275 (1983)
28. 28.
Pudlák, P.: Cuts, consistency statements and interpretations. J. Symb. Log. 50(2), 423–441 (1985)
29. 29.
Putnam, H.: Trial and error predicates and a solution to a problem of Mostowski. J. Symb. Log. 30(1), 146–153 (1965)
30. 30.
Schmerl, J.H.: End extensions of models of arithmetic. Notre Dame J. Form. Log. 33(2), 216–219 (1992)
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)
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)
34. 34.
Solovay, R.M.: Interpretability in set theories. Unpublished letter to P. Hájek. http://www.cs.cas.cz/hajek/RSolovayZFGB.pdf (1976)
35. 35.
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press, Cambridge (2000)
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)
38. 38.
Visser, A.: The unprovability of small inconsistency. Arch. Math. Log. 32(4), 275–298 (1993)
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)
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)
42. 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. 43.
Visser, A.: Hume’s principle, beginnings. Rev. Symb. Log. 4(1), 114–129 (2011)
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)
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. http://www.phil.uu.nl/preprints/lgps/ (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. http://foundationaladventures.com/
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)
50. 50.
Wang, H.: Arithmetic translations of axiom systems. Trans. Am. Math. Soc. 71, 283–293 (1951)
51. 51.
Wang, H.: Arithmetical models for formal systems. Methodos 3, 217–232 (1951)
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)
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)