2025/10/30 by Guillaume Geoffroy, Geoffroy, Guillaume
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2510.26849
openalex publication_date 2025/10/30 · openalex created_date 2025/11/05 · openalex updated_date 2026/07/28
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(L) of sup-preserving functions from [0,1] to an integral commutative residuated complete lattice L (in the intuitionistic case, 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(L) satisfies v + v = 2v exactly when L is a locale, (ii) involutiveness of negation in USC(L) corresponds to that in 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.