AI 中文总结
本文利用 Simmons 的无点 Cantor-Bendixson 余导数算子，简化了 Xu-Ye 关于自由 Heyting 代数不可嵌入基本拓扑的证明，并证明了直觉主义二阶命题逻辑的 Heyting 代数语义不具强完备性。
AI 中文摘要
我们给出了 Simmons 的无点 Cantor-Bendixson 余导数算子在直觉主义逻辑中的两个新应用。首先，我们用该算子简化了 Xu 和 Ye 最近结果的证明，即两个生成元上的自由 Heyting 代数不会作为任何基本拓扑中的次终对象之 Heyting 代数出现。然后，我们用该算子证明：对于直觉主义二阶命题逻辑，完全的 Heyting 代数语义并不具有强完备性：从任意假设集合出发的语义后承与通常的句法后承并不一致。
英文摘要
We present two new applications of Simmons' point-free Cantor-Bendixson coderivative operator in intuitionistic logic. First, we use it to give a simplified proof of the recent result of Xu and Ye that the free Heyting algebra on two generators does not occur as the Heyting algebra of subterminal objects in any elementary topos. Then we use it to prove that complete Heyting algebra semantics is not strongly complete for intuitionistic second-order propositional logic: semantic consequence from an arbitrary set of assumptions does not coincide with ordinary syntactic consequence.
Comments23 pages, 1 figure
