The Explanatory Power of a New Proof: Henkin’s Completeness Proof

  • John BaldwinEmail author
Part of the Boston Studies in the Philosophy and History of Science book series (BSPS, volume 334)


Mancosu writes But explanations in mathematics do not only come in the form of proofs. In some cases explanations are sought in a major recasting of an entire discipline. (Mancosu 2008, 142) This paper takes up both halves of that statement. On the one hand we provide a case study of the explanatory value of a particular milestone proof. In the process we examine how it began the recasting of a discipline.


  1. Ackerman, W. 1950. Reviewed: The completeness of the first-order functional calculus by Leon Henkin. Journal of Symbolic Logic 15: 68. German.Google Scholar
  2. Addison, J.W., L. Henkin, and A. Tarski, eds. 1965. The theory of models. Amsterdam: North-Holland.Google Scholar
  3. Avigad, J., and R. Morris. 2014. The concept of ‘character’ in Dirichlet’s theorem on primes in an arithmetic progression. Archive for History of Exact Sciences 68: 265–326.CrossRefGoogle Scholar
  4. Baldwin, J. 2016. Foundations of mathematics: Reliability and clarity, the explanatory role of mathematical induction. In Proceedings of the Logic, Language, Information, and Computation, 23rd International Workshop, Wollics 2016, Puebla Mexico, 16–19 Aug 2016, ed. J. Väänänen, Å. Hirvonen, and R. de Queiroz, 68–82.CrossRefGoogle Scholar
  5. Baldwin, J.T. 2017. Axiomatizing changing conceptions of the geometric continuum I: Euclid and Hilbert. Philosophia Mathematica 32. Scholar
  6. Baldwin, J. 2018. Model theory and the philosophy of mathematical practice: Formalization without Foundationalism. Cambridge: Cambridge University Press.CrossRefGoogle Scholar
  7. Baldwin, J., and A. Lachlan. 1971. On strongly minimal sets. Journal of Symbolic Logic 36: 79–96.CrossRefGoogle Scholar
  8. Baldwin, J., and C. Laskowski. 2018. Henkin constructions of models with size continuum. To appear: Bulletin of Symbolic Logic.Google Scholar
  9. Barwise, J., and S. Feferman, eds. 1985. Model-theoretic logics. New York: Springer.Google Scholar
  10. Beth, E. 1959. The foundations of mathematics. Amsterdam: North Holland.Google Scholar
  11. Birkhoff, Garrett. 1935. On the structure of abstract algebras. Proceedings of the Cambridge Philosophical Society 31: 433–454.CrossRefGoogle Scholar
  12. Chang, C., and H. Keisler. 1973. Model theory. Amsterdam: North-Holland. 3rd edition, 1990.Google Scholar
  13. Cintula, P., and C. Noguera. 2015. A Henkin-style proof of completeness for first-order algebraizable logics. Journal of Symbolic Logic 80: 341–358.CrossRefGoogle Scholar
  14. Dawson, J.W. 1993. The compactness of first-order logic: From Gödel to Lindstrom. History and Philosophy of Logic 14: 15–37.CrossRefGoogle Scholar
  15. Detlefsen, M. 2014. Completeness and the ends of axiomatization. In Interpreting Gödel, ed. J. Kennedy, 59–77. Cambridge: Cambridge University Press.CrossRefGoogle Scholar
  16. Dickmann, M. 1985. Larger infinitary logics. In Model-theoretic logics, ed. J. Barwise, and S. Feferman, 317–363. New York: Springer.Google Scholar
  17. Farah, I., B. Hart, M. Lupini, L. Robert, A. Tikuisis, A. Vignati, and A. Winter. 2016. Model theory of C*-algebras. Math arXiv:1602.08072v3.Google Scholar
  18. Franks, C. 2010. Cut as consequence. History and Philosophy of Logic 31: 349–379.CrossRefGoogle Scholar
  19. Franks, C. 2014. Logical completeness, form, and content: An archaeology. In Interpreting Gödel: Critical essays, ed. J. Kennedy, 78–106. Cambridge: Cambridge University Press.CrossRefGoogle Scholar
  20. Gentzen, G. 1932. Üuber die existenz unabhängiger axiomensysteme zu unendlichen satzsystemen. Mathematische Annalen 107: 329–350. Translated in Szabo, The Collected Papers of Gerhard Gentzen North Holland, London (1969) as On the existence of independent axioms systems for infinite sentence systems, 29–52.Google Scholar
  21. Gödel, K. 1929. Über die Vollständigkeit des Logikkalküls. In Kurt Gödel: Collected works, vol. 1, ed. S. Feferman, et al., 60–101. New York: Oxford University Press. 1929 Ph.D. thesis reprinted.Google Scholar
  22. Gödel, K. 1930. The completeness of the axioms of the functional calculus of logic. In Kurt Gödel, collected works, vol. I, ed. S. Feferman, et al., 103–123. New York: Oxford University Press. Under the auspices of Association for Symbolic Logic: Providence, Rhode Island;1930c in collected works; first appeared: Monatshefte für Mathematik und Physik.Google Scholar
  23. Goodstein, R.L. 1953. On the metamathematics of algebra by A. Robinson. The Mathematical Gazette 37(321): 224–226.CrossRefGoogle Scholar
  24. Hafner, J., and P. Mancosu. 2005. The varieties of mathematical explanation. In Visualization, explanation, and reasoning styles in mathematics, ed. P. Mancosu, K. Jørgensen, and S. Pedersen, 251–249. Dordrecht: Springer.Google Scholar
  25. Hafner, J., and P. Mancosu. 2008. Beyond unification. In The philosophy of mathematical practice, ed. P. Mancosu, 151–178. Oxford: Oxford University Press.CrossRefGoogle Scholar
  26. Henkin, L. 1949. The completeness of the first-order functional calculus. Journal of Symbolic Logic 14: 159–166.CrossRefGoogle Scholar
  27. Henkin, L. 1953. Some interconnections between modern algebra and mathematical logic. Transactions of the American Mathematical Society 74: 410–427.CrossRefGoogle Scholar
  28. Henkin, L. 1996. The discovery of my completeness proofs. The Bulletin of Symbolic Logic 2: 127–158.CrossRefGoogle Scholar
  29. Hilbert, D., and W. Ackermann. 1938. Grundzüge der Theoretischen Logik, 2nd ed. Berlin: Springer. First edition, 1928.CrossRefGoogle Scholar
  30. Hintikka, J. 1955. Form and content in quantification theory. Acta Philosophica Fennica 8: 7–55.Google Scholar
  31. Hodges, W. 1985. Building models by games. London Mathematical Society, Student Texts. Cambridge: Cambridge University Press.Google Scholar
  32. Karp, C. 1959. Languages with expressions of infinite length. Ph.D. thesis, University of Southern California. Advisor, Leon Henkin:
  33. Keisler, H. 1971. Model theory for infinitary logic. Amsterdam: North-Holland.Google Scholar
  34. Kreisel, G., and J. Krivine. 1967. Elements of mathematical logic (Model Theory). Amsterdam: North Holland.Google Scholar
  35. Lakatos, D. 1976. Proofs and refutations. Cambridge: Cambridge University Press.CrossRefGoogle Scholar
  36. Makkai, M. 1969. On the model theory of denumerably long formulas with finite strings of quantifiers. Journal of Symbolic Logic 34: 437–459.CrossRefGoogle Scholar
  37. Mancosu, P. 2008. Mathematical explanation: Why it matters. In The philosophy of mathematical practice, ed. P. Mancosu, 134–150. Oxford: Oxford University Press.CrossRefGoogle Scholar
  38. Marker, D. (2002). Model theory: An introduction. New York: Springer.Google Scholar
  39. Resnik, M., and D. Kushner. 1987. Explanation, independence, and realism in mathematics. The British Journal for the Philosophy of Science 38: 141–158.CrossRefGoogle Scholar
  40. Robinson, A. 1951. Introduction to model theory and to the metamathematics of algebra. Studies in logic and the foundations of mathematics. Amsterdam: North Holland. 1st edition 1951; 2nd edition 1965.Google Scholar
  41. Robinson, A. 1952. On the application of symbolic logic to algebra. In Proceedings of the International Congress of Mathematicians, Cambridge, Aug 30–Sept 6 1950, vol. 1, 686–694. Providence: American Mathematical Society.Google Scholar
  42. Robinson, A. 1970. Forcing in model theory. In Actes du Congrès international des mathématiciens, vol. 1, 245–250. Providence: American Mathematical Society.Google Scholar
  43. Skolem, T. 1967. Some remarks on axiomatic set theory. In From Frege to Godel: A sourcebook in mathematical logic, 1879–1931, ed. J. Van Heijenoort, 290–301. Harvard University Press. German original published in 1923; address delivered in 1922.Google Scholar
  44. Smullyan, R.M. 1963. A unifying principle in quantification theory. Proceedings of the National Academy of Science 49: 828–832.CrossRefGoogle Scholar
  45. Smullyan, R.M. 1966. Trees and nest structures. Journal of Symbolic Logic 31: 828–832.Google Scholar
  46. Steiner, M. 1978. Mathematical explanation. Philosophical Studies 34: 135–151.CrossRefGoogle Scholar
  47. Tarski, A. 1935. Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philosophica 1: 261–405. Translated as: The concept of truth in formalized languages in Logic, Tarski (1956).Google Scholar
  48. Tarski, A. 1946. A remark on functionally free algebras. Annals of Mathematics 47: 163–165.CrossRefGoogle Scholar
  49. Tarski, A. 1954. Contributions to the theory of models, I and II. Indagationes Mathematicae 16: 572–582.CrossRefGoogle Scholar
  50. Tarski, A. 1956. Logic, semantics and metamathematics: Papers from 1923–1938. Oxford: Clarendon Press. Translated by J.H. Woodger.Google Scholar
  51. Tarski, A., and R. Vaught. 1956. Arithmetical extensions of relational systems. Compositio Mathematica 13: 81–102.Google Scholar
  52. Werndl, C. 2009. Justifying definitions in mathematics: Going beyond Lakatos. Philosophia Mathematica 3: 313–340.CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Department of Mathematics, Statistics, and Computer ScienceUniversity of Illinois at ChicagoChicagoUSA

Personalised recommendations