George Metcalfe

Mathematisches Institut Universität Bern (Suiza)

Teoría de Prueba

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 es profesor del Instituto de Matemáticas de la Universidad de Berna, Suiza. Recibió su doctorado en Ciencias de la Computación en 2004 del King's College de Londres, después de haber estudiado Matemáticas y Filosofía en el St. Anne's College de Oxford y en Inteligencia Artificial en la Universidad de Edimburgo.

Realizó estudios postdoctorales en la Universidad Técnica de Viena y en la Universidad de Vanderbilt, en Nashville, antes de trasladarse a Berna en 2009. Sus intereses de investigación incluyen la teoría de la prueba, el álgebra universal y las lógicas no clásicas.