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 on 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\"of Type Theory is not able to construct non-trivial apartness relations between propositions either.
翻译：我们用海丁代数语义学来将所有分离关系都分类,用理论逻辑来定义所有分离关系,以扩展直觉逻辑。我们显示,每个包含非三角分离术语的交配代数符合被排斥中间的弱法,每个交配代数中包含紧密分离术语的交配代数事实上都是布尔伦代数。这回答了E.~Rijke关于主张分离正确概念的问题,并得出了在交配代数代数中可能发生的分离术语的简短分类。我们还表明,“类型理论”的马丁-L\\”也无法在各种主张之间建立非三角分离关系。
相关内容
微信扫码咨询专知VIP会员