带否定的分配格逻辑的有限公理化
Finite axiomatizability of logics of distributive lattices with negation
摘要：
本文主要研究由各种带否定的分配格定义的保序逻辑，特别是研究这些逻辑是否可以通过有限希尔伯特演算公理化的问题。在否定结果的一面，我们提供了一个句法条件上的等式表示的品种，需要失败的有限公理化相应的逻辑。这个结果的一个应用是所有带否定的分配格的逻辑不是可公理化的;同样，我们建立了所有奥卡姆代数的簇的保序逻辑也不是可公理化的。在积极的一面，我们表明，半德摩根代数的任意子品种是公理化的有限数量的方程，当且仅当相应的保序逻辑公理化的有限希尔伯特演算。这个等价也适用于奥卡姆代数的伯曼簇的每个子簇。作为推论，我们得到了直觉主义逻辑的无蕴涵部分是可公理化的新证明，以及一个新的希尔伯特演算.我们的证明是建设性的，因为它们允许我们有效地将各种代数的等式表示转换为相应的保序逻辑的希尔伯特演算，反之亦然.我们还考虑了与上述变种相关的断言逻辑，特别表明半德摩根代数的可公理化的子变种的断言逻辑也是可公理化的。
英文摘要：
This paper focuses on order-preserving logics defined from varieties of distributive lattices with negation, and in particular on the problem of whether these can be axiomatized by means of finite Hilbert calculi. On the side of negative results, we provide a syntactic condition on the equational presentation of a variety that entails failure of finite axiomatizability for the corresponding logic. An application of this result is that the logic of all distributive lattices with negation is not finitely axiomatizable; likewise, we establish that the order-preserving logic of the variety of all Ockham algebras is also not finitely axiomatizable. On the positive side, we show that an arbitrary subvariety of semi-De Morgan algebras is axiomatized by a finite number of equations if and only if the corresponding order-preserving logic is axiomatized by a finite Hilbert calculus. This equivalence also holds for every subvariety of a Berman variety of Ockham algebras. We obtain, as a corollary, a new proof that the implication-free fragment of intuitionistic logic is finitely axiomatizable, as well as a new Hilbert calculus for it. Our proofs are constructive in that they allow us to effectively convert an equational presentation of a variety of algebras into a Hilbert calculus for the corresponding order-preserving logic, and vice versa. We also consider the assertional logics associated to the above-mentioned varieties, showing in particular that the assertional logics of finitely axiomatizable subvarieties of semi-De Morgan algebras are finitely axiomatizable as well.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
