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}$的保上确界函数代数$USC(\mathcal{L})$（在直觉主义情形中，$\mathcal{L}$为局部格）。我们在连续逻辑语言中给出AC-代数的代数公理化，并利用Macneille完备化证明每个阿基米德模型均可嵌入某个AC-代数。我们还证明：(i) 当且仅当$\mathcal{L}$为局部格时，$USC(\mathcal{L})$满足$v \dot + v = 2v$；(ii) $USC(\mathcal{L})$中否定的对合性对应于$\mathcal{L}$中的对合性；(iii) 添加这些条件可恢复经典连续逻辑。针对仿射、直觉主义、对合、经典四种变体，我们分别给出序列式演绎系统，并证明完备性与切割可接纳性。这首次实现了具有切割可接纳性的经典连续逻辑序列式形式化系统。