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.

翻译：我们通过完备代数语义引入并发展了命题连续直觉主义逻辑与命题连续仿射逻辑。我们的方法以AC-代数为核心，即从$[0,1]$到整交换剩余完备格$\mathcal{L}$（直觉主义情形下$\mathcal{L}$为locale）的保上确界函数代数$USC(\mathcal{L})$。我们在连续逻辑的语言中给出AC-代数的代数公理化，并利用Macneille完备化证明：每个Archimedean模型均可嵌入某个AC-代数。我们还证明：(i) 当且仅当$\mathcal{L}$为locale时$USC(\mathcal{L})$满足$v \dot + v = 2v$；(ii) $USC(\mathcal{L})$中否定的对合性对应于$\mathcal{L}$中的对合性；(iii) 添加这些条件可恢复经典连续逻辑。针对每种变体——仿射、直觉主义、对合、经典——我们提供了矢列式演绎系统，并证明了完备性与割消可容许性。由此得到了首个具有割消可容许性的经典连续逻辑矢列式形式系统。