14 Jan 2021
This Thursday 14 January is the 3rd World Logic Day (the 2nd under the auspices of UNESCO), celebrated with events in many places throughout the world. See here: http://wld.cipsh.international In Tallinn, we will host a lecture by Prof Herman Geuvers from Nijmegen, a renowned logician/type theorist who is a good friend of ours. His talk will be at 14.00 Tallinn time (GMT+2), ie at 13.00 Central European Time (CET, GMT+1). The Zoom link will appear on the below link of the Tallinn World Logic Day on the actual day of the event: http://cs.ioc.ee/lsg/wld2021.html The title and abstract are below. Welcome to join! Niccol Veltri, Tarmo Uustalu --- Deriving Derivation Rules from Truth Tables: Classically, Constructively and Proof Reduction Herman Geuvers, Radboud University and Technical University Eindhoven Abstract: We have developed a general method for deriving natural deduction rules from the truth table for a connective. The method applies to both constructive and classical logic and it produces derivation rules of a generic form that lend themselves well to proof-theoretic investigations, abstracting from the specific choice of connectives. We have defined the notion of "detour conversion" (or "cut") and "permutation conversion" for the constructive connectives. For the well-known connectives, like 'and', 'or', 'implication', 'negation', the constructive rules we derive are equivalent to the natural deduction rules we know from Gentzen and Prawitz, both in terms of logical derivability and in terms of proof reductions. However, our rules have a different shape (closer to the "general elimination rules" by Von Plato, but more general than those). For the constructive rules, we also have completeness with respect to a Kripke semantics, which emphasizes that also for the connectives that are not known as constructive, like 'nand' and 'if-the-else', we really have constructive rules. In the talk I will give an overview of our work on this topic, by first introducing the method and relating it to standard natural deduction. Then we will analyze detour conversion and permutation conversion in general for the constructive rules. Following the Curry-Howard isomorphism, we assign proof-terms to deductions and we study conversion of derivations as term reduction. We will prove strong normalisation for the union of detour conversion and permutation conversion, for any set of constructive rules. If time permits, we will look into ongoing work on proof-reduction for deductions in the classical variant of the logic. Joint work with Tonny Hurkens and Iris van der Giessen. -- [LOGIC] mailing list http://www.dvmlg.de/mailingliste.html Archive: http://www.illc.uva.nl/LogicList/ provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam