Hyper Natural Deduction

After quite some years of research, my colleague Arnold Beckmann and my paper on Hyper Natural Deduction has finally been published in the Journal of Logic and Computation. This paper was the difficult but necessary first step in our program to develop a Curry-Howard style correspondence between standard Gödel logic (and its Hypersequent calculus) and some kind of parallel computations.

The results of this article were first announced at the LICS (Logic in Computer Science) Conference in 2015, but the current version is much more intuitive due to a switch to inductive definition, usage of graph representation for proofs, and finally due to a fix of a serious error. The abstract of the current article read:

We introduce a system of Hyper Natural Deduction for Gödel Logic as an extension of Gentzen’s system of Natural Deduction. A deduction in this system consists of a finite set of derivations which uses the typical rules of Natural Deduction, plus additional rules providing means for communication between derivations. We show that our system is sound and complete for infinite-valued propositional Gödel Logic, by giving translations to and from Avron’s Hypersequent Calculus. We provide conversions for normalization extending usual conversions for Natural Deduction and prove the existence of normal forms for Hyper Natural Deduction for Gödel Logic. We show that normal deductions satisfy the subformula property.

The article (preprint version) by itself is rather long (around 70 pages including the technical appendix), but for those interested, the first 20 pages give a nice introduction and the inductive definition of our system, which suffices for building upon this work. The rest of the paper is dedicated to an extensional definition – not and inductive definition but one via clearly defined properties on the final object – and the proof of normalization.

Starting point of our investigations was Arnon Avron‘s comments on parallel computations and communication when he introduced the Hypersequent calculus (Hypersequents, Logical Consequence and Intermediate Logics for Concurrency, Ann.Math.Art.Int. 4 (1991) 225-248):

The second, deeper objective of this paper is to contribute towards a better understanding of the notion of logical consequence in general, and especially its possible relations with parallel computations.

We believe that these logics […] could serve as bases for parallel λ-calculi.

The name “communication rule” hints, of course, at a certain intuitive interpretation that we have of it as corresponding to the idea of exchanging information between two multiprocesses: […]

In working towards a Curry-Howard (CH) correspondence between Gödel logics and some kind of process calculus, we are guided by the original path, as laid out in the above graphics: Starting from Intuitionistic Logic (IL) and its sequent calculus (LJ) a natural dudcution system (ND) provided the link to the λ-calculus. We started from Gödel logics (GL) and its Hypersequent calculus (HLK) and in this article developed a Hyper Natural Deduction with similar properties as the original Natural Deduction system.

Curry-Howard correspondences provide deep conceptual links between formal proofs and computational programs. A whole range of such CH correspondences have been identified and explored. The most fundamental one is between the natural deduction proof formalism for intuitionistic logic, and a foundational programming language called lambda calculus. This CH correspondence interprets formulas in proofs as types in programs, proof transformations like cut-reduction to computation steps like beta-reduction in lambda calculus. These insights have led to applications of logical tools to programming language technology, and the development of programming languages like CAML and of proof assistants like Coq.

CH correspondences are well established for sequential programming, but are far less clear for parallel programming. Current approaches to establish such links for parallel programming always start from established models of parallel programming like process algebra (CSP, CCS, pi-calculus) and define a related logical formalism. For example the linear logic proof formalism is inspired by the pi-calculus process algebra. Although some links between linear logic and pi-calculus have been established, a deep, inspiring connection is missing. Another problem is that logical formalisms established in this way often lack a clear semantics which is independent of the related computational model on which they are based. Thus, despite years of intense research on this topic, we are far from having a clear and useful answer which leads to strong applications in programming language technology as we have seen for the fundamental CH correspondence for sequential programming.

Although it was a long and tiring path to the current status, it is only the beginning.