George Metcalfe

Mathematisches Institut Universität Bern (Switzerland)

Proof Theory

Proof Surgery for Ordered Structures

Proof surgery — the manipulation of formal proofs to obtain new proofs of a certain form — is a favourite tool of proof theorists. Most famously, eliminations of cut rules in sequent calculi are used to establish consistency, conservativity, decidability, and interpolation results for logical theories. In this talk, I will describe some further quite surprising uses of proof surgery to establish algebraic properties for ordered structures. First, I will explain how eliminating the Takeuti-Titani density rule from proofs in hypersequent calculi leads to “standard completeness” results for many-valued logics, or, equivalently, that certain varieties of residuated lattices are generated by their linearly and densely ordered members (see [4, 1]). Second, I will explain how eliminating a resolution-like rule can be used to prove that the variety of lattice-ordered groups is generated by the automorphism lattice-ordered group over the real numbers, and that free groups are orderable (see [3, 2]).

  • [1] A. Ciabattoni and G. Metcalfe, Density elimination, Theoretical Com- puter Science, vol. 403, (2008), no. 2-3, pp. 328–346.
  • [2] A. Colacito and G. Metcalfe, Proof theory and ordered groups, Submitted, 2017.
  • [3] N. Galatos and G. Metcalfe, Proof theory for lattice-ordered groups, Annals of Pure and Applied Logic, vol. 167 (2016), no. 8, pp. 707–724.
  • [4] G. Metcalfe and F. Montagna, Substructural fuzzy logics, Journal of Sym- bolic Logic, vol. 72 (2007), no. 3, pp. 834–864.


George Metcalfe is a professor at the Mathematical Institute of the University of Bern, Switzerland. He received his PhD in Computer Science in 2004 from King's College London, having previously studied Mathematics and Philosophy at St. Anne's College, Oxford, and Artificial Intelligence at the University of Edinburgh.

He held postdoctoral positions at the Technical University of Vienna and Vanderbilt University, Nashville, before moving to Bern in 2009. His research interests include proof theory, universal algebra, and non-classical logics.