Gödel Logic: from Natural Deduction to Parallel Computation

Abstract

Propositional Gödel logic extends intuitionistic logic with the non-constructive principle of linearity $A\to B\vee B\to A$. We introduce a Curry-Howard correspondence for this logic and show that a particularly simple natural deduction calculus can be used as a typing system. The resulting functional language enriches the simply typed lambda calculus with a synchronous communication mechanism between parallel processes. Our normalization proof employs original termination arguments and sophisticated proof transformations with a meaningful computational reading. Our results provide a computational interpretation of Gödel logic as a logic of communicating parallel processes, thus proving Avron's 1991 conjecture.