Changes

==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===

The axioms are just four in number, divided into the ''arithmetic initials'', <math>I_1\!</math> and <math>I_2,\!</math> and the ''algebraic initials'', <math>J_1\!</math> and <math>J_2.\!</math>

The axioms are just four in number, divided into the ''arithmetic initials'', <math>I_1\!</math> and <math>I_2\!</math>, and the ''algebraic initials'', <math>J_1\!</math> and <math>J_2\!</math>.

{| align="center" cellpadding="10"

{| align="center" cellpadding="10"

|}

|}

One way of assigning logical meaning to the initial equations is known as the ''entitative interpretation'' (<math>\operatorname{En}</math>).  Under <math>\operatorname{En},</math> the axioms read as follows:

One way of assigning logical meaning to the initial equations is known as the ''entitative interpretation'' (<math>\operatorname{En}</math>).  Under <math>\operatorname{En}</math>, the axioms read as follows:

{| align="center" cellpadding="10"

{| align="center" cellpadding="10"

|}

|}

Another way of assigning logical meaning to the initial equations is known as the ''existential interpretation'' (<math>\operatorname{Ex}</math>).  Under <math>\operatorname{Ex},</math> the axioms read as follows:

Another way of assigning logical meaning to the initial equations is known as the ''existential interpretation'' (<math>\operatorname{Ex}</math>).  Under <math>\operatorname{Ex}</math>, the axioms read as follows:

{| align="center" cellpadding="10"

{| align="center" cellpadding="10"

All of the axioms in this set have the form of equations.  This means that all of the inference licensed by them are reversible.  The proof annotation scheme employed below makes use of a double bar <math>\overline{\underline{~~~~~~}}</math> to mark this fact, but it will often be left to the reader to decide which of the two possible ways of applying the axiom is the one that is called for in a particular case.

All of the axioms in this set have the form of equations.  This means that all of the inference licensed by them are reversible.  The proof annotation scheme employed below makes use of a double bar <math>\overline{\underline{~~~~~~}}</math> to mark this fact, but it will often be left to the reader to decide which of the two possible ways of applying the axiom is the one that is called for in a particular case.

Peirce introduced these formal equations at a level of abstraction that is one step higher than their customary interpretations as propositional calculi, which two readings he called the ''Entitative'' and the ''Existential'' interpretations, here referred to as <math>\operatorname{En}</math> and <math>\operatorname{Ex},</math> respectively.  The early CSP, as in his essay on "Qualitative Logic", and also GSB, emphasized the <math>\operatorname{En}</math> interpretation, while the later CSP developed mostly the <math>\operatorname{Ex}</math> interpretation.

Peirce introduced these formal equations at a level of abstraction that is one step higher than their customary interpretations as propositional calculi, which two readings he called the ''Entitative'' and the ''Existential'' interpretations, here referred to as <math>\operatorname{En}</math> and <math>\operatorname{Ex}</math>, respectively.  The early CSP, as in his essay on &rdquo;Qualitative Logic&rdquo;, and also GSB, emphasized the <math>\operatorname{En}</math> interpretation, while the later CSP developed mostly the <math>\operatorname{Ex}</math> interpretation.

===Frequently used theorems===

===Frequently used theorems===