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

arXiv: https://arxiv.org/abs/1607.05120 · HTML: https://mlsanity.com/paper/1607.05120/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Jul 2016.

## Built on by (most cited first, 1 of 1)

- [G"odel-Dummett linear temporal logic](https://mlsanity.com/paper/2306.15805/) (2023)

## Abstract (arXiv)

Propositional G"odel logic extends intuitionistic logic with the non-constructive principle of linearity Arightarrow B lor Brightarrow 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.