Equational Inference

All the initials have the form of equations.  This means the inference steps they license are reversible.  The proof annotation scheme employed below makes use of double bars to mark this fact, though it will often be left to the reader to decide which of the two possible directions is the one required for applying the indicated axiom.

The actual business of proof is a far more strategic affair than the routine cranking of inference rules might suggest.  Part of the reason for this lies in the circumstance that the customary types of inference rules combine the moving forward of a state of inquiry with the losing of information along the way that doesn’t appear immediately relevant, at least, not as viewed in the local focus and short run of the proof in question.  Over the long haul, this has the pernicious side‑effect that one is forever strategically required to reconstruct much of the information one had strategically thought to forget at earlier stages of proof, where “before the proof started” can be counted as an earlier stage of the proof in view.

This is just one of the reasons it can be very instructive to study equational inference rules of the sort our axioms have just provided.  Although equational forms of reasoning are paramount in mathematics, they are less familiar to the student of the usual logic textbooks, who may find a few surprises here.

cc: FB | Logical Graphs • Laws of Form • Mathstodon • Academia.edu
cc: Conceptual Graphs • Cybernetics • Structural Modeling • Systems Science