Proof Surgery for Ordered Structures
George Metcalfe (Universität Bern)

March 10, 2017, 6:00am - 8:00am
Logic Group, The University of Melbourne

Old Quad
Parkville 3010


Shawn Standefer
University of Melbourne

Topic areas


George Metcalfe (Bern) will present "Proof Surgery for Ordered Structures" at 11 in Old Quad G09. 

Abstract: 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 applications 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 applications of the Takeuti-Titani density rule from proofs in hypersequent calculi leads to “standard completeness” results for certain many-valued logics, or, equivalently, that certain varieties of residuated lattices are generated by their linearly and densely ordered members. Second, I will explain how eliminating applications of 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 number line, and that free groups are orderable.

Supporting material

Add supporting material (slides, programs, etc.)




Who is attending?

No one has said they will attend yet.

Will you attend this event?

Let us know so we can notify you of any change of plan.