Cut-free Deductive System for Continuous Intuitionistic Logic

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.