Heyting 代数

格序 $a\le b$ 表示“证据 $a$ 足以得到 $b$”。蕴涵 $a\Rightarrow b$ 收集能与 $a$ 合用而推出 $b$ 的最大证据条件。它不是先写好的一张经典真假表，而是由“与 $a$ 合取”这一步的右伴随唯一决定。

经典布尔代数要求每个元素都有真正补元；Heyting 代数只要求最大的不相容部分。一个命题与其否定可以都未达到顶元，反映当前证据既没有建立命题，也没有排除它。序结构把这种未决保留下来，而不会强行添加第三个固定真值。

取三元链 $H=\{0<a<1\}$，交与并是最小值、最大值。在任意全序 Heyting 代数中，

所以 $\mathrm{\neg }a=a\Rightarrow 0=0$，继而 $\mathrm{\neg }\mathrm{\neg }a=0\Rightarrow 0=1$。于是

同一个元素同时反驳排中律和双重否定消去的普遍有效性。计算依赖伴随定义，不能通过给 $a$ 随意命名为“未知”代替。

拓扑空间 $X$ 的全体开集也构成 Heyting 代数：

取 $X=\mathbb{R}$、$U=(0,1)$，则 $\mathrm{\neg }U=(-\mathrm{\infty },0)\cup (1,\mathrm{\infty })$，而 $\mathrm{\neg }\mathrm{\neg }U=(0,1)=U$；换成开集 $U=(0,1)\cup (1,2)$，双重否定会填回缺失点而得到 $(0,2)$。这说明双重否定一般是正则化操作，不是恒等。

Heyting 代数是布尔代数的推广。若对每个 $a$ 都有 $a\vee \mathrm{\neg }a=1$，等价地 $\mathrm{\neg }\mathrm{\neg }a=a$，则 Heyting 代数成为布尔代数；在这种额外条件下，其有效逻辑从 IPL 增强为经典命题逻辑。

Lindenbaum–Tarski 构造把证明论变成代数：可证蕴涵对应序，不同公式的可证等价类成为格元素。由此可以用同态、子代数和完备化研究中间逻辑；但某个有限 Heyting 代数给出的反值只反驳该公式的普遍有效性，不能自动证明整套逻辑具有有限模型性质。

开集代数还连接直觉主义 Kripke 语义公理库直觉主义 Kripke 语义Intuitionistic Kripke semantics · Kripke semantics for IPL在信息增长的预序世界上用持久赋值和未来量化解释直觉主义联结词的语义。与拓扑语义。前者按信息扩张解释强迫，后者按开集内部解释蕴涵；二者都让真理具有稳定性，却通过不同数学对象实现，不能把世界节点直接等同于开集元素。