
arXiv: 2207.06993
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.
representation of lattices, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, orthologic, classical logic, lattices with negation, Mathematics - Logic, intuitionistic logic, Logic in Computer Science (cs.LO), FOS: Mathematics, lattices with implication, F.4.1, natural deduction, Logic (math.LO), introduction and elimination rules, 03B20, 03G10, 06B15, 06B23, 06C15, 06D15, 06D20
representation of lattices, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, orthologic, classical logic, lattices with negation, Mathematics - Logic, intuitionistic logic, Logic in Computer Science (cs.LO), FOS: Mathematics, lattices with implication, F.4.1, natural deduction, Logic (math.LO), introduction and elimination rules, 03B20, 03G10, 06B15, 06B23, 06C15, 06D15, 06D20
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 9 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
