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称为“Reiteration”的规则，则可得到给定签名下直觉主义逻辑的证明系统；若不添加Reiteration，而添加归谬法（Reductio ad Absurdum）规则，则可得到正规则逻辑（orthologic）的证明系统；同时添加Reiteration和归谬法，则得到经典逻辑的证明系统。可以论证，Reiteration和归谬法都不像引入和消去规则那样与联结词的意义直接相关，因此我们所识别的基础逻辑可作为直觉主义逻辑、正规则逻辑和经典逻辑支持者之间更基础的起点与共同基础。我们在证明论上论证的这一逻辑的代数语义学基于配备所谓弱伪补（weak pseudocomplementation）的有界格。我们证明，此类格扩张可通过一个集合连同满足简单一阶条件的自反二元关系来表示，从而为该逻辑提供了优雅的关系语义学。这建立在我们先前对带否定格的表示研究之上，我们针对弱伪补之外的几种否定类型扩展并特化了该研究。最后，我们讨论了将这些表示扩展到带有条件或蕴涵运算的格的方法。