A Natural Proof System for Herbrand’s Theorem

  • Benjamin RalphEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10703)


The reduction of undecidable first-order logic to decidable propositional logic via Herbrand’s theorem has long been of interest to theoretical computer science, with the notion of a Herbrand proof motivating the definition of expansion proofs. The problem of building a natural proof system around expansion proofs, with composition of proofs and cut-free completeness, has been approached from a variety of different angles. In this paper we construct a simple deep inference system for first-order logic, Open image in new window , based around the notion of expansion proofs, as a starting point to developing a rich proof theory around this foundation. Translations between proofs in this system and expansion proofs are given, retaining much of the structure in each direction.


Structural proof theory First-order logic Deep inference Herbrand’s theorem Expansion proofs 


  1. 1.
    Alcolei, A., Clairambault, P., Hyland, M., Winskel, G.: The true concurrency of Herbrand’s theorem (2017, submitted)Google Scholar
  2. 2.
    Aler Tubella, A.: A study of normalisation through subatomic logic. University of Bath (2016)Google Scholar
  3. 3.
    Aler Tubella, A., Guglielmi, A.: Subatomic proof systems: splittable systems. arXiv preprint arXiv:1703.10258 (2017)
  4. 4.
    Aler Tubella, A., Guglielmi, A., Ralph, B.: Removing cycles from proofs. In: Goranko, V., Dam, M. (eds.) 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Stockholm, Sweden 2017. Leibniz International Proceedings in Informatics (LIPIcs), pp. 9:1–9:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017)Google Scholar
  5. 5.
    Brünnler, K.: Deep inference and symmetry in classical proofs. Logos Verlag (2003)Google Scholar
  6. 6.
    Brünnler, K.: Two restrictions on contraction. Logic J. IGPL 11(5), 525–529 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Brünnler, K.: Cut elimination inside a deep inference system for classical predicate logic. Stud. Logica. 82(1), 51–71 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Buss, S.R.: On Herbrand’s theorem. In: Leivant, D. (ed.) LCC 1994. LNCS, vol. 960, pp. 195–209. Springer, Heidelberg (1995). CrossRefGoogle Scholar
  9. 9.
    Chaudhuri, K., Hetzl, S., Miller, D.: A multi-focused proof system isomorphic to expansion proofs. J. Logic Comput. 26(2), 577–603 (2016). MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Guglielmi, A., Gundersen, T., Parigot, M.: A proof calculus which reduces syntactic bureaucracy. In: Proceedings of the 21st International Conference on Rewriting Techniques and Applications (Rta 2010), vol. 6, pp. 135–150 (2010).
  11. 11.
    Gundersen, T.E.: A general view of normalisation through atomic flows. University of Bath (2009)Google Scholar
  12. 12.
    Heijltjes, W.: Classical proof forestry. Ann. Pure Appl. Logic 161(11), 1346–1366 (2010). MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Herbrand, J., Goldfarb, W.D.: Logical Writings. Springer, Dordrecht (1971). CrossRefGoogle Scholar
  14. 14.
    Hetzl, S., Weller, D.: Expansion trees with cut. arXiv preprint arXiv:1308.0428 (2013)
  15. 15.
    McKinley, R.: A sequent calculus demonstration of Herbrand’s theorem. arXiv preprint arXiv:1007.3414 (2010)
  16. 16.
    McKinley, R.: Proof nets for Herbrand’s theorem. ACM Trans. Comput. Logic (TOCL) 14(1), 1–31 (2013). MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Miller, D.A.: A compact representation of proofs. Stud. Logica. 46(4), 347–370 (1987). MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Straßburger, L.: Some observations on the proof theory of second order propositional multiplicative linear logic. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 309–324. Springer, Heidelberg (2009). CrossRefGoogle Scholar
  19. 19.
    Straßburger, L.: Deep inference, expansion trees, and proof graphs for second order propositional multiplicative linear logic, vol. RR-9071, p. 38. Inria Saclay Ile de France (2017)Google Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.University of BathBathUK

Personalised recommendations