We give a proof-theoretic as well as a semantic characterization of a logic in the signature with conjunction, disjunction, negation, and the universal and existential quantifiers that we suggest has a certain fundamental status. We present a Fitch-style natural deduction system for the logic that contains only the introduction and elimination rules for the logical constants. From this starting point, if one adds the rule that Fitch called Reiteration, one obtains a proof system for intuitionistic logic in the given signature; if instead of adding Reiteration, one adds the rule of Reductio ad Absurdum, one obtains a proof system for orthologic; by adding both Reiteration and Reductio, one obtains a proof system for classical logic. Arguably neither Reiteration nor Reductio is as intimately related to the meaning of the connectives as the introduction and elimination rules are, so the base logic we identify serves as a more fundamental starting point and common ground between proponents of intuitionistic logic, orthologic, and classical logic. The algebraic semantics for the logic we motivate proof-theoretically is based on bounded lattices equipped with what has been called a weak pseudocomplementation. We show that such lattice expansions are representable using a set together with a reflexive binary relation satisfying a simple first-order condition, which yields an elegant relational semantics for the logic. This builds on our previous study of representations of lattices with negations, which we extend and specialize for several types of negation in addition to weak pseudocomplementation. Finally, we discuss ways of extending these representations to lattices with a conditional or implication operation.
翻译:我们给出了一种证据理论以及语义特征, 在签名中给出了一种逻辑的逻辑特征, 包括连接、 脱钩、 否定, 以及我们所认为的普遍和存在性量化符, 并具有某种基本的地位。 我们为逻辑提供了一种Fitch式的自然推论系统, 仅包含逻辑常量的引入和删除规则。 从这个开始, 如果加上了Fitch称为“ 重新点” 的规则, 人们可以获得一种直观逻辑的验证系统; 如果在给定的签名中添加了“ 重新点 ”, 而不是增加“ 降低 ad Absurdum ” 规则, 并增加了“ 降低 ” 和“ 提高 ” ; 通过添加“ 降低” 和“ 降低 ” 等值, 我们提供了一个典型逻辑的验证系统。 重现“ 减少 ” 与“ 减少 ” 规则” 之间的关联性密切相连, 因此, 我们确定基本逻辑作为更基本的起始点和共同点, 直观逻辑的推理, 和古典逻辑的推理的推理, 。