Kurt Gödel Research Center

2015 seminar talk: Eliminating Disjunctions by Disjunction Elimination

Talk held by Peter Schuster (University of Verona, Italy, currently Humboldt returning fellow at the Munich Center for Mathematical Philosophy, Germany) at the KGRC seminar on 2015-06-25.

Abstract

Joint work with Davide Rinaldi (University of Leeds, England)

If a Scott-style multi-conclusion entailment relation E extends a Tarskian single-conclusion consequence relation C, then E is conservative over C precisely when the appropriate rule of disjunction elimination can be proved for C. This readily follows from a sandwich criterion due to Scott, but can also be fleshed out into a proof-theoretical reduction. The principal application is to turn transfinite methods into admissible rules. For instance, contrapositive forms of Zorn's Lemma are often applied in concrete contexts in which–at least for definite Horn clauses–the corresponding conservation theorems would suffice. We now have at hand a syntactical, uniform approach to many of those conservation theorems, e.g. of the ones related to the theorems by Krull-Lindenbaum, Artin-Schreier, Szpilrajn and Hahn-Banach. Related work can be found e.g. in locale theory (Mulvey-Pelletier 1991), dynamical algebra (Coste-Lombardi-Roy 2001, Lombardi 1997-8), formal topology (Cederquist-Coquand-Negri 1998) and proof theory (Coquand-Negri-von Plato 2004, Negri-von Plato 2011).