Proof Surgery for Ordered StructuresGeorge Metcalfe (Universität Bern)
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.
Who is attending?
No one has said they will attend yet.
Will you attend this event?