  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.
