A Curry-Howard Correspondence for the Minimal Fragment of Łukasiewicz Logic

Abstract

In this paper we introduce a term calculus $\mathcal{B}$ which adds to the affine $\lambda$-calculus with pairing a new construct allowing for a restricted form of contraction. We obtain a Curry-Howard correspondence between $\mathcal{B}$ and the sub-structural logical system which we call "minimal Łukasiewicz logic", also known in the literature as the logic of hoops (a generalisation of MV-algebras). This logic lies strictly in between affine minimal logic and standard minimal logic. We prove that $\mathcal{B}$ is strongly normalising and has the Church-Rosser property. We also give examples of terms in $\mathcal{B}$ corresponding to some important derivations from our work and the literature. Finally, we discuss the relation between normalisation in $\mathcal{B}$ and cut-elimination for a Gentzen-style formulation of minimal Łukasiewicz logic.

arXiv comment17 pages

References in corpus (1)

• On Pocrims and Hoops