Cut-free Deductive System for Continuous Intuitionistic Logic

TL;DR

This paper develops a new cut-free deductive system for continuous intuitionistic logic using algebraic semantics based on AC-algebras, enabling a deeper understanding and formalization of continuous logic variants.

Contribution

It introduces AC-algebras and provides a sequent calculus for continuous intuitionistic and affine logic, establishing completeness and cut admissibility.

Findings

AC-algebras provide a complete algebraic semantics for continuous logic.

The sequent calculus is complete and admits cut elimination.

Classical continuous logic is recovered with additional conditions.

Abstract

We introduce and develop propositional continuous intuitionistic logic and propositional continuous affine logic via complete algebraic semantics. Our approach centres on AC-algebras, which are algebras $USC(\mathcal{L})$ of sup-preserving functions from $[0,1]$ to an integral commutative residuated complete lattice $\mathcal{L}$ (in the intuitionistic case, $\mathcal{L}$ is a locale). We give an algebraic axiomatisation of AC-algebras in the language of continuous logic and prove, using the Macneille completion, that every Archimedean model embeds into some AC-algebra. We also show that (i) $USC(\mathcal{L})$ satisfies $v \dot + v = 2v$ exactly when $\mathcal{L}$ is a locale, (ii) involutiveness of negation in $USC(\mathcal{L})$ corresponds to that in $\mathcal{L} $, and that (iii) adding those conditions recovers classical continuous logic. For each variant -affine, intuitionistic, involutive, classical -we provide a sequent style deductive system and prove completeness and cut admissibility. This yields the first sequent style formulation of classical continuous logic enjoying cut admissibility.