A Curry-Howard Correspondence for the Minimal Fragment of {\L}ukasiewicz Logic

TL;DR

This paper introduces a new term calculus linked to a specific sub-structural logic, establishing a Curry-Howard correspondence, and proves key properties like normalization and confluence.

Contribution

It presents a novel calculus ${ m extbf B}$ for minimal { m extbf Ł}ukasiewicz logic, extending affine lambda calculus with controlled contraction, and explores its properties.

Findings

${ m extbf B}$ is strongly normalising

${ m extbf B}$ has the Church-Rosser property

Examples connect calculus to logical derivations

Abstract

In this paper we introduce a term calculus ${\cal 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 ${\cal B}$ and the sub-structural logical system which we call "minimal {\L}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 ${\cal B}$ is strongly normalising and has the Church-Rosser property. We also give examples of terms in ${\cal B}$ corresponding to some important derivations from our work and the literature. Finally, we discuss the relation between normalisation in ${\cal B}$ and cut-elimination for a Gentzen-style formulation of minimal {\L}ukasiewicz logic.