论文标题
命题之间的公平关系
Apartness relations between propositions
论文作者
论文摘要
我们对使用Heyting代数语义扩展直觉逻辑的命题逻辑中可以定义的所有公寓关系分类。我们表明，每个包含一个非平凡的公寓术语的热烈代数都满足了被排除的中间的薄弱法律，每个包含紧密分离术语的嘿代数实际上都是布尔式代数。这回答了E. Rijke关于命题的正确概念的问题，并得出了在Heyting代数中可能发生的分离术语的简短分类。我们还表明，马丁 - 洛夫类型理论无法在命题之间构建非平凡的分离关系。
We classify all apartness relations definable in propositional logics extending intuitionistic logic using Heyting algebra semantics. We show that every Heyting algebra which contains a non-trivial apartness term satisfies the weak law of excluded middle, and every Heyting algebra which contains a tight apartness term is in fact a Boolean algebra. This answers a question of E. Rijke regarding the correct notion of apartness for propositions, and yields a short classification of apartness terms that can occur in a Heyting algebra. We also show that Martin-Löf Type Theory is not able to construct non-trivial apartness relations between propositions.
