Lindenbaum’s Lemma via Open Induction

Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 28)


With Raoult’s Open Induction in place of Zorn’s Lemma, we do a perhaps more perspicuous proof of Lindenbaum’s Lemma for not necessarily countable languages of first-order predicate logic. We generally work for and with classical logic, but say what can be achieved for intuitionistic logic, which prompts the natural generalizations for distributive and complete lattices.


Intuitionistic Logic Complete Lattice Strong Primality Tests Complete Consistent Theory Lindenbaum Algebra 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



The research that has led to this note was carried out within the project “Abstract Mathematics for Actual Computation: Hilbert’s Program in the 21st Century” funded by the John Templeton Foundation, and within two of the European Union’s Marie Curie projects: the Initial Training Network “MALOA: From Mathematical Logic to Applications” and the International Research Exchange Scheme project “CORCON: Correctness by Construction”. The final version of the present note was prepared when the third author was visiting the Munich Center for Mathematical Philosophy: upon kind invitation by Hannes Leitgeb and with a research fellowship “Erneuter Aufenthalt” by the Alexander-von-Humboldt Foundation. All authors wish to thank Thierry Coquand, Volker Halbach, Kentaro Fujimoto, Giovanni Sambin and the anonymous referee for useful hints and constructive critique. Last but not least, the third author would like to express his gratitude to Gerhard Jäger for now more than a decade of encouragement, support and hospitality.


  1. 1.
    U. Berger, A computational interpretation of open induction, in Proceedings of the Ninetenth Annual IEEE Symposium on Logic in Computer Science (IEEE Computer Society, 2004), pp. 326–334Google Scholar
  2. 2.
    F. Ciraulo, A constructive semantics for non-deducibility. MLQ Math. Log. Q. 54, 35–48 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    R. Constable, M. Bickford, Intuitionistic completeness of first-order logic. Ann. Pure Appl. Logic 165, 164–198 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    T. Coquand, Two applications of Boolean models. Arch. Math. Logic 37, 143–147 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    T. Coquand, Constructive topology and combinatorics, in Constructivity in Computer Science (San Antonio, TX, 1991), ed. by J.P. Myers Jr., M.J. O’Donnell. Lecture Notes in Computer Science, vol. 613 (Springer, Berlin, 1992), pp. 159–164Google Scholar
  6. 6.
    T. Coquand, H. Persson, Gröbner bases in type theory, in Types for Proofs and Programs (Irsee, 1998), ed. by T. Altenkirch, W. Naraschewski, B. Reus. Lecture Notes in Computer Science, vol. 1657 (Springer, Berlin, 1999), pp. 33–46Google Scholar
  7. 7.
    T. Coquand, J.M. Smith, An application of constructive completeness, in Types for Proofs and Programs (Torino, 1995), ed. by S. Berardi, M. Coppo. Lecture Notes in Computer Science, vol. 1158 (Springer, Berlin, 1996), pp. 76–84Google Scholar
  8. 8.
    A.G. Drágalin, A completeness theorem for higher-order intuitionistic logic: an intuitionistic proof, in Mathematical Logic and Its Applications (Druzhba, 1986), ed. by D. Skordev (Plenum, New York, 1987), pp. 107–124Google Scholar
  9. 9.
    A. Enayat, A. Visser, New constructions of satisfaction classes. Logic Group Preprint Series 303 (Utrecht University, 2013)Google Scholar
  10. 10.
    M. Hendtlass, P. Schuster, A direct proof of Wiener’s theorem, in How the World Computes. Turing Centenary Conference and Eighth Conference on Computability in Europe (Cambridge, 2012), ed. by S.B. Cooper, A. Dawar, B. Löwe. Lecture Notes in Computer Science, vol. 7318 (Springer, Berlin, 2012), pp. 294–303Google Scholar
  11. 11.
    L. Henkin, The completeness of the first-order functional calculus. J. Symb. Logic 14, 159–166 (1949)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    S. Huber, P. Schuster, Maximalprinzipien und Induktionsbeweise (Forthcoming)Google Scholar
  13. 13.
    H. Ishihara, Constructive reverse mathematics: compactness properties, in From Sets and Types to Analysis and Topology, ed. by L. Crosilla, P. Schuster. Oxford Logic Guides 48 (Oxford University Press, 2005), pp. 245–267Google Scholar
  14. 14.
    H. Kotlarski, S. Krajewski, A.H. Lachlan, Construction of satisfaction classes for nonstandard models. Can. Math. Bull. 24, 283–293 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    G.E. Leigh, Conservativity for theories of compositional truth via cut elimination. J. Symbolic Logic 80, 825–865 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    H. Perdry, Strongly Noetherian rings and constructive ideal theory. J. Symb. Comput. 37, 511–535 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    H. Persson, An application of the constructive spectrum of a ring, in Type Theory and the Integrated Logic of Programs, Ph.D. thesis (Chalmers University, University of Göteborg, 1999)Google Scholar
  18. 18.
    J.-C. Raoult, Proving open properties by induction. Inform. Process. Lett. 29(1), 19–23 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    H. Rasiowa, R. Sikorski, The Mathematics of Metamathematics. Monografie Matematyczne 41. Panstwowe Wydawnictwo Naukowe, Warszawa (1963)Google Scholar
  20. 20.
    D. Rinaldi, P. Schuster, A universal Krull-Lindenbaum theorem. J. Pure Appl. Algebra (to appear)Google Scholar
  21. 21.
    D. Rinaldi, P. Schuster, Eliminating disjunctions by disjunction elimination (Forthcoming)Google Scholar
  22. 22.
    G. Sambin, Pretopologies and completeness proofs. J. Symbolic Logic 60, 861–878 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    D. Scott, Completeness and axiomatizability in many-valued logic, in Proceedings of the Tarski Symposium (Berkeley, CA., 1971), ed. by L. Henkin et al. (American Mathematical Society, Providence, R.I., 1974), pp. 411–435Google Scholar
  24. 24.
    P. Schuster, Induction in algebra: a first case study. in 27th Annual ACM/IEEE Symposium on Logic in Computer Science (Dubrovnik, 2012) (IEEE Computer Society Publications, 2012), pp. 581–585. Journal version: Log. Methods Comput. Sci. 3(20), 9 (2013)Google Scholar
  25. 25.
    J.R. Shoenfield, Mathematical Logic (Association for Symbolic Logic, 2000)Google Scholar
  26. 26.
    A. Tarski, Fundamentale Begriffe der Methodologie der deduktiven Wissenschaften. I. Monatsh. Math. Phys. 37, 361–404 (1930)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Dipartimento di MatematicaUniversità degli Studi di PadovaPadovaItaly
  2. 2.Department of Pure MathematicsUniversity of LeedsLeeds LS2 9JTEngland
  3. 3.Dipartimento di InformaticaUniversità degli Studi di VeronaVeronaItaly

Personalised recommendations