Changes

{{DISPLAYTITLE:Propositional Equation Reasoning Systems}}

{{DISPLAYTITLE:Propositional Equation Reasoning Systems}}

This article develops elementary facts about the formal calculi that we describe as '''propositional equation reasoning systems''' ('''PERS''').  This work follows up on the ''[[alpha graphs]]'' that [[Charles Sanders Peirce]] devised as a graphical syntax for [[propositional calculus]] and also on the ''calculus of indications'' that [[George Spencer Brown]] presented in his ''[[Laws of Form]]''.

This article develops elementary facts about a family of formal calculi called '''propositional equation reasoning systems''' ('''PERS''').  This work follows on the ''alpha graphs'' that [[Charles Sanders Peirce]] devised as a graphical syntax for [[propositional calculus]] and also on the ''calculus of indications'' that George Spencer Brown presented in his ''Laws of Form''.

==Formal development==

==Formal development==

The first order of business is to give the exact forms of the axioms that we use, devolving from Peirce's "[[Logical Graphs]]" via Spencer-Brown's ''[[Laws of Form]]'' (LOF).  In formal proofs, we use a variation of the annotation scheme from LOF to mark each step of the proof according to which axiom, or ''initial'', is being invoked to justify the corresponding step of syntactic transformation, whether it applies to graphs or to strings.

The first order of business is to give the exact forms of the axioms that we use, devolving from Peirce's "[[Logical Graphs]]" via Spencer-Brown's ''Laws of Form'' (LOF).  In formal proofs, we use a variation of the annotation scheme from LOF to mark each step of the proof according to which axiom, or ''initial'', is being invoked to justify the corresponding step of syntactic transformation, whether it applies to graphs or to strings.

===Axioms===

===Axioms===