**george.metcalfemath.unibe.ch**

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]).

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.