| Line 1: | 
Line 1: | 
|   | {{DISPLAYTITLE:Propositional Equation Reasoning Systems}}  |   | {{DISPLAYTITLE:Propositional Equation Reasoning Systems}}  | 
| − | * '''Note.''' The MathJax parser is not rendering this page properly.<br>Until it can be fixed please see the [http://intersci.ss.uci.edu/wiki/index.php/Propositional_Equation_Reasoning_Systems InterSciWiki version].
  |   | 
| − | 
  |   | 
|   | '''Author: [[User:Jon Awbrey|Jon Awbrey]]'''  |   | '''Author: [[User:Jon Awbrey|Jon Awbrey]]'''  | 
|   |  |   |  | 
| Line 1,382: | 
Line 1,380: | 
|   | e_0 & = &  |   | e_0 & = &  | 
|   | {}^{\backprime\backprime}  |   | {}^{\backprime\backprime}  | 
| − | \texttt{(~)}  | + | \texttt{( )}  | 
|   | {}^{\prime\prime}  |   | {}^{\prime\prime}  | 
|   | \\[4pt]  |   | \\[4pt]  | 
|   | e_1 & = &  |   | e_1 & = &  | 
|   | {}^{\backprime\backprime}  |   | {}^{\backprime\backprime}  | 
| − | \texttt{~}  | + | \texttt{ }  | 
|   | {}^{\prime\prime}  |   | {}^{\prime\prime}  | 
|   | \\[4pt]  |   | \\[4pt]  | 
|   | e_2 & = &  |   | e_2 & = &  | 
|   | {}^{\backprime\backprime}  |   | {}^{\backprime\backprime}  | 
| − | \texttt{(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))}  | + | \texttt{(} p \texttt{ (} q \texttt{)) (} p \texttt{ (} r \texttt{))}  | 
|   | {}^{\prime\prime}  |   | {}^{\prime\prime}  | 
|   | \\[4pt]  |   | \\[4pt]  | 
|   | e_3 & = &  |   | e_3 & = &  | 
|   | {}^{\backprime\backprime}  |   | {}^{\backprime\backprime}  | 
| − | \texttt{(} p \texttt{~(} q~r \texttt{))}  | + | \texttt{(} p \texttt{ (} q r \texttt{))}  | 
|   | {}^{\prime\prime}  |   | {}^{\prime\prime}  | 
|   | \\[4pt]  |   | \\[4pt]  | 
|   | e_4 & = &  |   | e_4 & = &  | 
|   | {}^{\backprime\backprime}  |   | {}^{\backprime\backprime}  | 
| − | \texttt{(} p~q~r \texttt{~,~(} p \texttt{))}  | + | \texttt{(} p q r \texttt{ , (} p \texttt{))}  | 
|   | {}^{\prime\prime}  |   | {}^{\prime\prime}  | 
|   | \\[4pt]  |   | \\[4pt]  | 
|   | e_5 & = &  |   | e_5 & = &  | 
|   | {}^{\backprime\backprime}  |   | {}^{\backprime\backprime}  | 
| − | \texttt{((~(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))~,~(} p \texttt{~(} q~r \texttt{))~))}  | + | \texttt{(( (} p \texttt{ (} q \texttt{)) (} p \texttt{ (} r \texttt{)) , (} p \texttt{ (} q r \texttt{)) ))}  | 
|   | {}^{\prime\prime}  |   | {}^{\prime\prime}  | 
|   | \end{array}\!</math>  |   | \end{array}\!</math>  | 
| Line 1,415: | 
Line 1,413: | 
|   |  |   |  | 
|   | {| align="center" cellpadding="8" width="90%"  |   | {| align="center" cellpadding="8" width="90%"  | 
| − | | <math>e_0 = {}^{\backprime\backprime} \texttt{(~)} {}^{\prime\prime}\!</math> expresses the logical constant <math>\mathrm{false}.\!</math>  | + | | <math>e_0 = {}^{\backprime\backprime} \texttt{( )} {}^{\prime\prime}\!</math> expresses the logical constant <math>\mathrm{false}.\!</math>  | 
|   | |-  |   | |-  | 
| − | | <math>e_1 = {}^{\backprime\backprime} \texttt{~} {}^{\prime\prime}\!</math> expresses the logical constant <math>\mathrm{true}.\!</math>  | + | | <math>e_1 = {}^{\backprime\backprime} \texttt{ } {}^{\prime\prime}\!</math> expresses the logical constant <math>\mathrm{true}.\!</math>  | 
|   | |-  |   | |-  | 
| − | | <math>e_2 = {}^{\backprime\backprime} \texttt{(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))} {}^{\prime\prime}\!</math> says <math>{}^{\backprime\backprime} \mathrm{not}~ p ~\mathrm{without}~ q,\!</math> <math>\mathrm{and~not}~ p ~\mathrm{without}~ r {}^{\prime\prime}.\!</math>  | + | | <math>e_2 = {}^{\backprime\backprime} \texttt{(} p \texttt{ (} q \texttt{)) (} p \texttt{ (} r \texttt{))} {}^{\prime\prime}\!</math> says <math>{}^{\backprime\backprime} \mathrm{not}~ p ~\mathrm{without}~ q,\!</math> <math>\mathrm{and~not}~ p ~\mathrm{without}~ r {}^{\prime\prime}.\!</math>  | 
|   | |-  |   | |-  | 
| − | | <math>e_3 = {}^{\backprime\backprime} \texttt{(} p \texttt{~(} q~r \texttt{))} {}^{\prime\prime}\!</math> says <math>{}^{\backprime\backprime} \mathrm{not}~ p ~\mathrm{without}~ q ~\mathrm{and}~ r {}^{\prime\prime}.\!</math>  | + | | <math>e_3 = {}^{\backprime\backprime} \texttt{(} p \texttt{ (} q~r \texttt{))} {}^{\prime\prime}\!</math> says <math>{}^{\backprime\backprime} \mathrm{not}~ p ~\mathrm{without}~ q ~\mathrm{and}~ r {}^{\prime\prime}.\!</math>  | 
|   | |-  |   | |-  | 
| − | | <math>e_4 = {}^{\backprime\backprime} \texttt{(} p~q~r \texttt{~,~(} p \texttt{))} {}^{\prime\prime}\!</math> says <math>{}^{\backprime\backprime} p ~\mathrm{and}~ q ~\mathrm{and}~ r,\!</math> <math>~\mathrm{or~else~not}~ p{}^{\prime\prime}.\!</math>  | + | | <math>e_4 = {}^{\backprime\backprime} \texttt{(} p~q~r \texttt{ , (} p \texttt{))} {}^{\prime\prime}\!</math> says <math>{}^{\backprime\backprime} p ~\mathrm{and}~ q ~\mathrm{and}~ r,\!</math> <math>~\mathrm{or~else~not}~ p{}^{\prime\prime}.\!</math>  | 
|   | |-  |   | |-  | 
| − | | <math>e_5 = {}^{\backprime\backprime} \texttt{((~(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))~,~(} p \texttt{~(} q~r \texttt{))~))} {}^{\prime\prime}\!</math> says that <math>e_2\!</math> and <math>e_3\!</math> say the same thing.  | + | | <math>e_5 = {}^{\backprime\backprime} \texttt{(( (} p \texttt{ (} q \texttt{)) (} p \texttt{ (} r \texttt{)) , (} p \texttt{ (} q~r \texttt{)) ))} {}^{\prime\prime}\!</math> says that <math>e_2\!</math> and <math>e_3\!</math> say the same thing.  | 
|   | |}  |   | |}  | 
|   |  |   |  | 
| Line 1,431: | 
Line 1,429: | 
|   |  |   |  | 
|   | {| align="center" cellpadding="8" width="90%"  |   | {| align="center" cellpadding="8" width="90%"  | 
| − | | <math>\texttt{(} p \texttt{~(} q \texttt{))(} p \texttt{~(} r \texttt{))} = \texttt{(} p \texttt{~(} q~r \texttt{))}.\!</math>  | + | | <math>\texttt{(} p \texttt{ (} q \texttt{))(} p \texttt{ (} r \texttt{))} = \texttt{(} p \texttt{ (} q~r \texttt{))}.\!</math>  | 
|   | |}  |   | |}  | 
|   |  |   |  | 
| Line 1,442: | 
Line 1,440: | 
|   | '''Proof 1''' proceeded by the ''straightforward approach'', starting with <math>e_2\!</math> as <math>s_1\!</math> and ending with <math>e_3\!</math> as <math>s_n\!.</math>  |   | '''Proof 1''' proceeded by the ''straightforward approach'', starting with <math>e_2\!</math> as <math>s_1\!</math> and ending with <math>e_3\!</math> as <math>s_n\!.</math>  | 
|   |  |   |  | 
| − | : That is, Proof 1 commenced from the sign <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))} {}^{\prime\prime}\!</math> and ended up at the sign <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q~r \texttt{))} {}^{\prime\prime}\!</math> by legal moves.  | + | : That is, Proof 1 commenced from the sign <math>{}^{\backprime\backprime} \texttt{(} p \texttt{ (} q \texttt{)) (} p \texttt{ (} r \texttt{))} {}^{\prime\prime}\!</math> and ended up at the sign <math>{}^{\backprime\backprime} \texttt{(} p \texttt{ (} q~r \texttt{))} {}^{\prime\prime}\!</math> by legal moves.  | 
|   |  |   |  | 
|   | '''Proof 2''' lit on by ''burning the candle at both ends'', changing <math>e_2\!</math> into a normal form that reduced to <math>e_4,\!</math> and changing <math>e_3\!</math> into a normal form that also reduced to <math>e_4,\!</math> in this way tethering <math>e_2\!</math> and <math>e_3\!</math> to a common stake.  |   | '''Proof 2''' lit on by ''burning the candle at both ends'', changing <math>e_2\!</math> into a normal form that reduced to <math>e_4,\!</math> and changing <math>e_3\!</math> into a normal form that also reduced to <math>e_4,\!</math> in this way tethering <math>e_2\!</math> and <math>e_3\!</math> to a common stake.  | 
|   |  |   |  | 
| − | : Filling in the details, one route went from <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))} {}^{\prime\prime}\!</math> to <math>{}^{\backprime\backprime} \texttt{(} p~q~r \texttt{~,~(} p \texttt{))} {}^{\prime\prime},\!</math> and another went from <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q~r \texttt{))} {}^{\prime\prime}\!</math> to <math>{}^{\backprime\backprime} \texttt{(} p~q~r \texttt{~,~(} p \texttt{))} {}^{\prime\prime},\!</math> thus equating the two points of departure.  | + | : Filling in the details, one route went from <math>{}^{\backprime\backprime} \texttt{(} p \texttt{ (} q \texttt{)) (} p \texttt{ (} r \texttt{))} {}^{\prime\prime}\!</math> to <math>{}^{\backprime\backprime} \texttt{(} p~q~r \texttt{ , (} p \texttt{))} {}^{\prime\prime},\!</math> and another went from <math>{}^{\backprime\backprime} \texttt{(} p \texttt{ (} q~r \texttt{))} {}^{\prime\prime}\!</math> to <math>{}^{\backprime\backprime} \texttt{(} p~q~r \texttt{ , (} p \texttt{))} {}^{\prime\prime},\!</math> thus equating the two points of departure.  | 
|   |  |   |  | 
|   | '''Proof 3''' took the path of reflection, expressing the meta-equation between <math>e_2\!</math> and <math>e_3\!</math> in the form of the naturalized equation <math>e_5,\!</math> then taking <math>e_5\!</math> as <math>s_1\!</math> and exchanging it by dint of value preserving steps for <math>e_1\!</math> as <math>s_n.\!</math>  |   | '''Proof 3''' took the path of reflection, expressing the meta-equation between <math>e_2\!</math> and <math>e_3\!</math> in the form of the naturalized equation <math>e_5,\!</math> then taking <math>e_5\!</math> as <math>s_1\!</math> and exchanging it by dint of value preserving steps for <math>e_1\!</math> as <math>s_n.\!</math>  | 
|   |  |   |  | 
| − | : This way of proceeding went from <math>e_5 = {}^{\backprime\backprime} \texttt{((~(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))~,~(} p \texttt{~(} q~r \texttt{))~))} {}^{\prime\prime}\!</math> to the blank expression that <math>\mathrm{Ex}\!</math> recognizes as the value <math>{\mathrm{true}}.\!</math>  | + | : This way of proceeding went from <math>e_5 = {}^{\backprime\backprime} \texttt{(( (} p \texttt{ (} q \texttt{)) (} p \texttt{ (} r \texttt{)) , (} p \texttt{ (} q~r \texttt{)) ))} {}^{\prime\prime}\!</math> to the blank expression that <math>\mathrm{Ex}\!</math> recognizes as the value <math>{\mathrm{true}}.\!</math>  | 
|   |  |   |  | 
|   | ==Computation and inference as semiosis==  |   | ==Computation and inference as semiosis==  | 
| Line 1,475: | 
Line 1,473: | 
|   | ~ p  |   | ~ p  | 
|   | \\  |   | \\  | 
| − | \overline{15:22, 6 November 2016 (UTC)15:22, 6 November 2016 (UTC)15:22, 6 November 2016 (UTC)}  | + | \overline{~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~}  | 
|   | \\  |   | \\  | 
|   | ~ q  |   | ~ q  | 
| Line 1,493: | 
Line 1,491: | 
|   | ~ p  |   | ~ p  | 
|   | \\  |   | \\  | 
| − | =\!=\!=\!=\!=\!=\!=\!=
  | + | \overline{\underline{~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~}}  | 
|   | \\  |   | \\  | 
|   | ~ p ~ q  |   | ~ p ~ q  | 
| Line 1,504: | 
Line 1,502: | 
|   | |  |   | |  | 
|   | <math>\begin{array}{l}  |   | <math>\begin{array}{l}  | 
| − | ~ \textit{Expression~1}  | + | ~ \textit{Expression 1}  | 
|   | \\  |   | \\  | 
| − | ~ \textit{Expression~2}  | + | ~ \textit{Expression 2}  | 
|   | \\  |   | \\  | 
| − | \overline{15:22, 6 November 2016 (UTC)15:22, 6 November 2016 (UTC)15:22, 6 November 2016 (UTC)15:22, 6 November 2016 (UTC)}  | + | \overline{~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~}  | 
|   | \\  |   | \\  | 
| − | ~ \textit{Expression~3}  | + | ~ \textit{Expression 3}  | 
|   | \end{array}</math>  |   | \end{array}</math>  | 
|   | |}  |   | |}  | 
| Line 1,518: | 
Line 1,516: | 
|   | {| align="center" cellpadding="8" width="90%"  |   | {| align="center" cellpadding="8" width="90%"  | 
|   | |  |   | |  | 
| − | <math>\textit{Premiss~1}, \textit{Premiss~2} ~\vdash~ \textit{Conclusion}.\!</math>  | + | <math>\textit{Premiss 1}, \textit{Premiss 2} ~\vdash~ \textit{Conclusion}.\!</math>  | 
|   | |}  |   | |}  | 
|   |  |   |  | 
| Line 1,525: | 
Line 1,523: | 
|   | {| align="center" cellpadding="8" width="90%"  |   | {| align="center" cellpadding="8" width="90%"  | 
|   | |  |   | |  | 
| − | From   <math>{\textit{Expression~1}}\!</math>   and   <math>{\textit{Expression~2}}\!</math>   infer   <math>{\textit{Expression~3}}.\!</math>  | + | From   <math>{\textit{Expression 1}}\!</math>   and   <math>{\textit{Expression 2}}\!</math>   infer   <math>{\textit{Expression 3}}.\!</math>  | 
|   | |}  |   | |}  | 
|   |  |   |  | 
| Line 1,557: | 
Line 1,555: | 
|   | ~ q \le r  |   | ~ q \le r  | 
|   | \\  |   | \\  | 
| − | \overline{15:22, 6 November 2016 (UTC)15:22, 6 November 2016 (UTC)15:22, 6 November 2016 (UTC)}  | + | \overline{~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~}  | 
|   | \\  |   | \\  | 
|   | ~ p \le r  |   | ~ p \le r  | 
| Line 1,575: | 
Line 1,573: | 
|   | ~ q \le r  |   | ~ q \le r  | 
|   | \\  |   | \\  | 
| − | =\!=\!=\!=\!=\!=\!=\!=
  | + | \overline{\underline{~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~}}  | 
|   | \\  |   | \\  | 
|   | ~ p \le q \le r  |   | ~ p \le q \le r  | 
| Line 1,656: | 
Line 1,654: | 
|   | |  |   | |  | 
|   | <math>\begin{matrix}  |   | <math>\begin{matrix}  | 
| − | \texttt{(} p \texttt{~(} q \texttt{))}  | + | \texttt{(} p \texttt{ (} q \texttt{))}  | 
|   | \\[4pt]  |   | \\[4pt]  | 
| − | \texttt{(} q \texttt{~(} r \texttt{))}  | + | \texttt{(} q \texttt{ (} r \texttt{))}  | 
|   | \\[4pt]  |   | \\[4pt]  | 
| − | \texttt{(} p \texttt{~(} r \texttt{))}  | + | \texttt{(} p \texttt{ (} r \texttt{))}  | 
|   | \\[4pt]  |   | \\[4pt]  | 
| − | \texttt{(} p \texttt{~(} q \texttt{))~(} q \texttt{~(} r \texttt{))}  | + | \texttt{(} p \texttt{ (} q \texttt{)) (} q \texttt{ (} r \texttt{))}  | 
|   | \end{matrix}</math>  |   | \end{matrix}</math>  | 
|   | |  |   | |  | 
| Line 1,683: | 
Line 1,681: | 
|   | | [[Image:Venn Diagram (P (Q)).jpg|500px]] || (52)  |   | | [[Image:Venn Diagram (P (Q)).jpg|500px]] || (52)  | 
|   | |-  |   | |-  | 
| − | | <math>f_{207}(p, q, r) ~=~ \texttt{(} p \texttt{~(} q \texttt{))}\!</math>  | + | | <math>f_{207}(p, q, r) ~=~ \texttt{(} p \texttt{ (} q \texttt{))}\!</math>  | 
|   | |-  |   | |-  | 
|   | |    |   | |    | 
| Line 1,689: | 
Line 1,687: | 
|   | | [[Image:Venn Diagram (Q (R)).jpg|500px]] || (53)  |   | | [[Image:Venn Diagram (Q (R)).jpg|500px]] || (53)  | 
|   | |-  |   | |-  | 
| − | | <math>f_{187}(p, q, r) ~=~ \texttt{(} q \texttt{~(} r \texttt{))}\!</math>  | + | | <math>f_{187}(p, q, r) ~=~ \texttt{(} q \texttt{ (} r \texttt{))}\!</math>  | 
|   | |-  |   | |-  | 
|   | |    |   | |    | 
| Line 1,695: | 
Line 1,693: | 
|   | | [[Image:Venn Diagram (P (R)).jpg|500px]] || (54)  |   | | [[Image:Venn Diagram (P (R)).jpg|500px]] || (54)  | 
|   | |-  |   | |-  | 
| − | | <math>f_{175}(p, q, r) ~=~ \texttt{(} p \texttt{~(} r \texttt{))}\!</math>  | + | | <math>f_{175}(p, q, r) ~=~ \texttt{(} p \texttt{ (} r \texttt{))}\!</math>  | 
|   | |-  |   | |-  | 
|   | |    |   | |    | 
| Line 1,701: | 
Line 1,699: | 
|   | | [[Image:Venn Diagram (P (Q)) (Q (R)).jpg|500px]] || (55)  |   | | [[Image:Venn Diagram (P (Q)) (Q (R)).jpg|500px]] || (55)  | 
|   | |-  |   | |-  | 
| − | | <math>f_{139}(p, q, r) ~=~ \texttt{(} p \texttt{~(} q \texttt{))~(} q \texttt{~(} r \texttt{))}\!</math>  | + | | <math>f_{139}(p, q, r) ~=~ \texttt{(} p \texttt{ (} q \texttt{)) (} q \texttt{ (} r \texttt{))}\!</math>  | 
|   | |}  |   | |}  | 
|   |  |   |  | 
| Line 1,824: | 
Line 1,822: | 
|   | ~ q \le r  |   | ~ q \le r  | 
|   | \\  |   | \\  | 
| − | \overline{15:22, 6 November 2016 (UTC)15:22, 6 November 2016 (UTC)15:22, 6 November 2016 (UTC)}  | + | \overline{~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~}  | 
|   | \\  |   | \\  | 
|   | ~ p \le r  |   | ~ p \le r  | 
| Line 1,853: | 
Line 1,851: | 
|   | ~ q \le r  |   | ~ q \le r  | 
|   | \\  |   | \\  | 
| − | =\!=\!=\!=\!=\!=\!=\!=
  | + | \overline{\underline{~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~}}  | 
|   | \\  |   | \\  | 
|   | ~ p \le q \le r  |   | ~ p \le q \le r  | 
| Line 1,921: | 
Line 1,919: | 
|   | |- style="height:40px; background:#f0f0ff"  |   | |- style="height:40px; background:#f0f0ff"  | 
|   | | <math>p \le q \le r\!</math>  |   | | <math>p \le q \le r\!</math>  | 
| − | | <math>\texttt{(} p \texttt{~(} q \texttt{))}\!</math>  | + | | <math>\texttt{(} p \texttt{ (} q \texttt{))}\!</math>  | 
| − | | <math>\texttt{(} p \texttt{~(} r \texttt{))}\!</math>  | + | | <math>\texttt{(} p \texttt{ (} r \texttt{))}\!</math>  | 
| − | | <math>\texttt{(} q \texttt{~(} r \texttt{))}\!</math>  | + | | <math>\texttt{(} q \texttt{ (} r \texttt{))}\!</math>  | 
|   | |}  |   | |}  | 
|   |  |   |  | 
| Line 2,431: | 
Line 2,429: | 
|   | In accord with my experimental way, I will stick with the case of transitive inference until I have pinned it down thoroughly, but of course the real interest is much more general than that.  |   | In accord with my experimental way, I will stick with the case of transitive inference until I have pinned it down thoroughly, but of course the real interest is much more general than that.  | 
|   |  |   |  | 
| − | At first sight, the relationships seem easy enough to write out.  Figure 75 shows how the various logical expressions are related to each other:  The expressions <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q \texttt{))} {}^{\prime\prime}\!</math> and <math>{}^{\backprime\backprime} \texttt{(} q \texttt{~(} r \texttt{))} {}^{\prime\prime}\!</math> are conjoined in a purely syntactic fashion — much in the way that one might compile a theory from axioms without knowing what either the theory or the axioms were about — and the best way to sum up the state of information implicit in taking them together is just the expression <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} q \texttt{))~(} q \texttt{~(} r \texttt{))}{}^{\prime\prime}\!</math> that would the canonical result of an equational or reversible rule of inference.  From that equational inference, one might arrive at the implicational inference <math>{}^{\backprime\backprime} \texttt{(} p \texttt{~(} r \texttt{))} {}^{\prime\prime}\!</math> by the most conventional implication.  | + | At first sight, the relationships seem easy enough to write out.  Figure 75 shows how the various logical expressions are related to each other:  The expressions <math>{}^{\backprime\backprime} \texttt{(} p \texttt{ (} q \texttt{))} {}^{\prime\prime}\!</math> and <math>{}^{\backprime\backprime} \texttt{(} q \texttt{ (} r \texttt{))} {}^{\prime\prime}\!</math> are conjoined in a purely syntactic fashion — much in the way that one might compile a theory from axioms without knowing what either the theory or the axioms were about — and the best way to sum up the state of information implicit in taking them together is just the expression <math>{}^{\backprime\backprime} \texttt{(} p \texttt{ (} q \texttt{)) (} q \texttt{ (} r \texttt{))}{}^{\prime\prime}\!</math> that would the canonical result of an equational or reversible rule of inference.  From that equational inference, one might arrive at the implicational inference <math>{}^{\backprime\backprime} \texttt{(} p \texttt{ (} r \texttt{))} {}^{\prime\prime}\!</math> by the most conventional implication.  | 
|   |  |   |  | 
|   | {| align="center" border="0" cellpadding="10"  |   | {| align="center" border="0" cellpadding="10"  | 
| Line 2,682: | 
Line 2,680: | 
|   | ==References==  |   | ==References==  | 
|   |  |   |  | 
| − | * [[Gottfried Leibniz|Leibniz, G.W.]] (1679–1686 ?), "Addenda to the Specimen of the Universal Calculus", pp. 40–46 in Parkinson, G.H.R. (ed.), ''Leibniz : Logical Papers'', Oxford University Press, London, UK, 1966.  (Cf. Gerhardt, 7, p. 223).  | + | * Leibniz, G.W. (1679–1686 ?), “Addenda to the Specimen of the Universal Calculus”, pp. 40–46 in Parkinson, G.H.R. (ed.), ''Leibniz : Logical Papers'', Oxford University Press, London, UK, 1966.  (Cf. Gerhardt, 7, p. 223).  | 
|   |  |   |  | 
| − | * [[Charles Peirce (Bibliography)|Peirce, C.S., Bibliography]].  | + | * [[Charles Sanders Peirce (Bibliography)|Peirce, C.S., Bibliography]].  | 
|   |  |   |  | 
| − | * [[Charles Peirce|Peirce, C.S.]] (1931–1935, 1958), ''Collected Papers of Charles Sanders Peirce'', vols. 1–6, [[Charles Hartshorne]] and [[Paul Weiss (philosopher)|Paul Weiss]] (eds.), vols. 7–8, [[Arthur W. Burks]] (ed.), Harvard University Press, Cambridge, MA.  Cited as CP volume.paragraph.  | + | * [[Charles Sanders Peirce|Peirce, C.S.]] (1931–1935, 1958), ''Collected Papers of Charles Sanders Peirce'', vols. 1–6, Charles Hartshorne and Paul Weiss (eds.), vols. 7–8, Arthur W. Burks (ed.), Harvard University Press, Cambridge, MA.  Cited as CP volume.paragraph.  | 
|   |  |   |  | 
| − | * Peirce, C.S. (1981–), ''Writings of Charles S. Peirce:  A Chronological Edition'', [[Peirce Edition Project]] (eds.), Indiana University Press, Bloomington and Indianoplis, IN.  Cited as CE volume, page.  | + | * Peirce, C.S. (1981–), ''Writings of Charles S. Peirce : A Chronological Edition'', Peirce Edition Project (eds.), Indiana University Press, Bloomington and Indianoplis, IN.  Cited as CE volume, page.  | 
|   |  |   |  | 
| − | * Peirce, C.S. (1885), "On the Algebra of Logic:  A Contribution to the Philosophy of Notation", ''American Journal of Mathematics'' 7 (1885), 180–202.  Reprinted as CP 3.359–403 and CE 5, 162–190.  | + | * Peirce, C.S. (1885), “On the Algebra of Logic : A Contribution to the Philosophy of Notation”, ''American Journal of Mathematics'' 7 (1885), 180–202.  Reprinted as CP 3.359–403 and CE 5, 162–190.  | 
|   |  |   |  | 
| − | * Peirce, C.S. (c. 1886), "Qualitative Logic", MS 736.  Published as pp. 101–115 in Carolyn Eisele (ed., 1976), ''The New Elements of Mathematics by Charles S. Peirce, Volume 4, Mathematical Philosophy'', Mouton, The Hague.  | + | * Peirce, C.S. (c. 1886), “Qualitative Logic”, MS 736.  Published as pp. 101–115 in Carolyn Eisele (ed., 1976), ''The New Elements of Mathematics by Charles S. Peirce, Volume 4, Mathematical Philosophy'', Mouton, The Hague.  | 
|   |  |   |  | 
| − | * Peirce, C.S. (1886 a), "Qualitative Logic", MS 582.  Published as pp. 323–371 in ''Writings of Charles S. Peirce:  A Chronological Edition, Volume 5, 1884–1886'', Peirce Edition Project (eds.), Indiana University Press, Bloomington, IN, 1993.  | + | * Peirce, C.S. (1886 a), “Qualitative Logic”, MS 582.  Published as pp. 323–371 in ''Writings of Charles S. Peirce : A Chronological Edition, Volume 5, 1884–1886'', Peirce Edition Project (eds.), Indiana University Press, Bloomington, IN, 1993.  | 
|   |  |   |  | 
| − | * Peirce, C.S. (1886 b), "The Logic of Relatives: Qualitative and Quantitative", MS 584.  Published as pp. 372–378 in ''Writings of Charles S. Peirce:  A Chronological Edition, Volume 5, 1884–1886'', Peirce Edition Project (eds.), Indiana University Press, Bloomington, IN, 1993.  | + | * Peirce, C.S. (1886 b), “The Logic of Relatives : Qualitative and Quantitative”, MS 584.  Published as pp. 372–378 in ''Writings of Charles S. Peirce : A Chronological Edition, Volume 5, 1884–1886'', Peirce Edition Project (eds.), Indiana University Press, Bloomington, IN, 1993.  | 
|   |  |   |  | 
| − | * [[George Spencer Brown|Spencer Brown, George]] (1969), ''[[Laws of Form]]'', George Allen and Unwin, London, UK.  | + | * Spencer Brown, George (1969), ''[[Laws of Form]]'', George Allen and Unwin, London, UK.  | 
|   |  |   |  | 
|   | ==See also==  |   | ==See also==  | 
|   | + |  | 
|   | ===Related essays and projects===  |   | ===Related essays and projects===  | 
|   |  |   |  |