Logic seminar

Hyper Natural Deduction

We introduce Hyper Natural Deduction as an extension of Gentzen's Natural Deduction system by communication like rules. The motivation is to obtain a natural deduction like system which is equivalent to Avron's Hypersequent Calculus for Goedel-Dummett Logic, and which permits natural conversion rules for normalisation as an extension of the well-known conversion rules for Natural Deduction. The ultimate goal of this project is to establish a Curry-Howard correspondence to some (yet to be found) model of parallel computation. An additional aim is to shed further light on Avron's suggestion [in A. Avron: Hypersequents, Logical Consequence and Intermediate Logics for Concurrency. Annals of Mathematics and Artificial Intelligence, 4(1991), 225-248] that a hypersequent can be thought of as a multiprocess.

This is joint work with Norbert Preining, supported by a Royal Society Daiwa Anglo-Japanese Foundation International Exchanges Award #IE130639.