G\"odel Logic: from Natural Deduction to Parallel Computation

TL;DR

This paper establishes a Curry-Howard correspondence for G"odel logic, resulting in a functional language with parallel communication, and provides a normalization proof that interprets G"odel logic as a system of communicating parallel processes.

Contribution

It introduces a simple natural deduction calculus for G"odel logic and demonstrates its computational interpretation as a language of communicating parallel processes.

Findings

Provides a Curry-Howard correspondence for G"odel logic

Enriches lambda calculus with synchronous communication

Proves G"odel logic as a logic of parallel processes

Abstract

Propositional G\"odel logic extends intuitionistic logic with the non-constructive principle of linearity $A\rightarrow B\ \lor\ B\rightarrow 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\"odel logic as a logic of communicating parallel processes, thus proving Avron's 1991 conjecture.