12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Friday April 19, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Propositional Equation Reasoning Systems (view source)
Revision as of 03:44, 10 November 2016
, 03:44, 10 November 2016format
{{DISPLAYTITLE:Propositional Equation Reasoning Systems}}
{{DISPLAYTITLE:Propositional Equation Reasoning Systems}}
'''Author: [[User:Jon Awbrey|Jon Awbrey]]'''
'''Author: [[User:Jon Awbrey|Jon Awbrey]]'''
==Logic as sign transformation==
==Logic as sign transformation==
We have been looking at various ways of transforming propositional expressions, expressed in the parallel formats of character strings and graphical structures, all the while preserving certain aspects of their "meaning" — and here I risk using that vaguest of all possible words, but only as a promissory note, hopefully to be cached out in a more meaningful species of currency as the discussion develops.
We have been looking at various ways of transforming propositional expressions, expressed in the parallel formats of character strings and graphical structures, all the while preserving certain aspects of their “meaning” — and here I risk using that vaguest of all possible words, but only as a promissory note, hopefully to be cached out in a more meaningful species of currency as the discussion develops.
I cannot pretend to be acquainted with or to comprehend every form of intension that others might find of interest in a given form of expression, nor can I speak for every form of meaning that another might find in a given form of syntax. The best that I can hope to do is to specify what my object is in using these expressions, and to say what aspects of their syntax are meant to serve this object, lending these properties the interest I have in preserving them as I put the expressions through the paces of their transformations.
I cannot pretend to be acquainted with or to comprehend every form of intension that others might find of interest in a given form of expression, nor can I speak for every form of meaning that another might find in a given form of syntax. The best that I can hope to do is to specify what my object is in using these expressions, and to say what aspects of their syntax are meant to serve this object, lending these properties the interest I have in preserving them as I put the expressions through the paces of their transformations.
My broader interest lies in the theory of inquiry as a special application or a special case of the theory of signs. Another name for the theory of inquiry is ''logic'' and another name for the theory of signs is ''semiotics''. So I might as well have said that I am interested in logic as a special application or a special case of semiotics. But what sort of a special application? What sort of a special case? Well, I think of logic as ''formal semiotics'' — though, of course, I am not the first to have said such a thing — and by ''formal'' we say, in our etymological way, that logic is concerned with the ''form'', indeed, with the ''animate beauty'' and the very ''life force'' of signs and sign actions. Yes, perhaps that is far too Latin a way of understanding logic, but it's all I've got.
My broader interest lies in the theory of inquiry as a special application or a special case of the theory of signs. Another name for the theory of inquiry is ''logic'' and another name for the theory of signs is ''semiotics''. So I might as well have said that I am interested in logic as a special application or a special case of semiotics. But what sort of a special application? What sort of a special case? Well, I think of logic as ''formal semiotics'' — though, of course, I am not the first to have said such a thing — and by ''formal'' we say, in our etymological way, that logic is concerned with the ''form'', indeed, with the ''animate beauty'' and the very ''life force'' of signs and sign actions. Yes, perhaps that is far too Latin a way of understanding logic, but it's all I've got.
Now, if you think about these things just a little more, I know that you will find them just a little suspicious, for what besides logic would I use to do this theory of signs that I would apply to this theory of inquiry that I'm also calling ''logic''? But that is precisely one of the things signified by the word ''formal'', for what I'd be required to use would have to be some brand of logic, that is, some sort of innate or inured skill at inquiry, but a style of logic that is casual, catch-as-catch-can, formative, incipient, inchoate, unformalized, a work in progress, partially built into our natural language and partially more primitive than our most artless language. In so far as I use it more than mention it, mention it more than describe it, and describe it more than fully formalize it, then to that extent it must be consigned to the realm of unformalized and unreflective logic, where some say "there be oracles", but I don't know.
Now, if you think about these things just a little more, I know that you will find them just a little suspicious, for what besides logic would I use to do this theory of signs that I would apply to this theory of inquiry that I'm also calling ''logic''? But that is precisely one of the things signified by the word ''formal'', for what I'd be required to use would have to be some brand of logic, that is, some sort of innate or inured skill at inquiry, but a style of logic that is casual, catch-as-catch-can, formative, incipient, inchoate, unformalized, a work in progress, partially built into our natural language and partially more primitive than our most artless language. In so far as I use it more than mention it, mention it more than describe it, and describe it more than fully formalize it, then to that extent it must be consigned to the realm of unformalized and unreflective logic, where some say “there be oracles”, but I don't know.
Still, one of the aims of formalizing what acts of reasoning that we can is to draw them into an arena where we can examine them more carefully, perhaps to get better at their performance than we can unreflectively, and thus to live, to formalize again another day. Formalization is not the be-all end-all of human life, not by a long shot, but it has its uses on that behalf.
Still, one of the aims of formalizing what acts of reasoning that we can is to draw them into an arena where we can examine them more carefully, perhaps to get better at their performance than we can unreflectively, and thus to live, to formalize again another day. Formalization is not the be-all end-all of human life, not by a long shot, but it has its uses on that behalf.
| [[Image:Venn Diagram (P (Q)) (P (R)).jpg|500px]] || (36)
| [[Image:Venn Diagram (P (Q)) (P (R)).jpg|500px]] || (36)
|-
|-
| <math>\text{Venn Diagram for}~ \texttt{(} p \texttt{~(} q \texttt{))~(} p \texttt{~(} r \texttt{))}\!</math>
| <math>\text{Venn Diagram for}~ \texttt{(} p \texttt{ (} q \texttt{)) (} p \texttt{ (} r \texttt{))}\!</math>
|}
|}
|}
|}
This is not only a logically equivalent DNF but exactly the same DNF expression that we obtained before, so we have established the given equation <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))} = \texttt{(} p \texttt{(} q r \texttt{))}.\!</math> Incidentally, one may wish to note that this DNF expression quickly folds into the following form:
This is not only a logically equivalent DNF but exactly the same DNF expression that we obtained before, so we have established the given equation <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))} = \texttt{(} p \texttt{(} q r \texttt{))}.\!</math> Incidentally, one may wish to note that this DNF expression quickly folds into the following form:
{| align="center" cellpadding="8"
{| align="center" cellpadding="8"
In other words, <math>{}^{\backprime\backprime} p ~\mathrm{is~equivalent~to}~ p ~\mathrm{and}~ q ~\mathrm{and}~ r {}^{\prime\prime}.\!</math>
In other words, <math>{}^{\backprime\backprime} p ~\mathrm{is~equivalent~to}~ p ~\mathrm{and}~ q ~\mathrm{and}~ r {}^{\prime\prime}.\!</math>
One lemma that suggests itself at this point is a principle that may be canonized as the ''Emptiness Rule''. It says that a bare lobe expression like <math>\texttt{( \_, \_, \ldots )},\!</math> with any number of places for arguments but nothing but blanks as filler, is logically tantamount to the proto-typical expression of its type, namely, the constant expression <math>\texttt{(~)}\!</math> that <math>\mathrm{Ex}\!</math> interprets as denoting the logical value <math>\mathrm{false}.\!</math> To depict the rule in graphical form, we have the continuing sequence of equations:
One lemma that suggests itself at this point is a principle that may be canonized as the ''Emptiness Rule''. It says that a bare lobe expression like <math>\texttt{(} \_ \texttt{,} \_ \texttt{,} \ldots \texttt{)},\!</math> with any number of places for arguments but nothing but blanks as filler, is logically tantamount to the proto-typical expression of its type, namely, the constant expression <math>\texttt{(} ~ \texttt{)}\!</math> that <math>\mathrm{Ex}~\!</math> interprets as denoting the logical value <math>\mathrm{false}.~\!</math> To depict the rule in graphical form, we have the continuing sequence of equations:
{| align="center" border="0" cellpadding="10"
{| align="center" border="0" cellpadding="10"
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>
{| 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.
|}
|}
{| 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>
|}
|}
'''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==
~ p
~ p
\\
\\
\overline{15:22, 6 November 2016 (UTC)15:22, 6 November 2016 (UTC)15:22, 6 November 2016 (UTC)}
\overline{~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~}
\\
\\
~ q
~ q
~ p
~ p
\\
\\
\overline{\underline{~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~}}
\\
\\
~ p ~ q
~ p ~ q
|
|
<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>
|}
|}
{| 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>
|}
|}
{| 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>
|}
|}
~ 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
~ q \le r
~ q \le r
\\
\\
\overline{\underline{~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~}}
\\
\\
~ p \le q \le r
~ p \le q \le r
|
|
<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>
|
|
| [[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>
|-
|-
|
|
| [[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>
|-
|-
|
|
| [[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>
|-
|-
|
|
| [[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>
|}
|}
~ 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
~ q \le r
~ q \le r
\\
\\
\overline{\underline{~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~}}
\\
\\
~ p \le q \le r
~ p \le q \le r
|- 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>
|}
|}
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"
==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===
