logical graph : formal development LogicalGraphFormalDevelopment 2008-08-26 16:29:02 2008-09-03 16:05:01 Topic logical graph : introduction entitative interpretation existential interpretation % this is the default PlanetMath preamble. as your knowledge % of TeX increases, you will probably want to edit this, but % it should be fine as is for beginners. % almost certainly you want these \usepackage{amssymb} \usepackage{amsmath} \usepackage{amsfonts} \usepackage{graphicx} % used for TeXing text within eps files %\usepackage{psfrag} % need this for including graphics (\includegraphics) %\usepackage{graphicx} % for neatly defining theorems and propositions %\usepackage{amsthm} % making logically defined graphics %\usepackage{xypic} % there are many more packages, add them here as you need them % define commands here \PMlinkescapeword{ad} \PMlinkescapeword{AD} \PMlinkescapeword{complex} \PMlinkescapeword{Complex} \PMlinkescapeword{cut} \PMlinkescapeword{Cut} \PMlinkescapeword{decide} \PMlinkescapeword{Decide} \PMlinkescapeword{development} \PMlinkescapeword{Development} \PMlinkescapeword{dft} \PMlinkescapeword{DFT} \PMlinkescapeword{dominant} \PMlinkescapeword{Dominant} \PMlinkescapeword{entire} \PMlinkescapeword{Entire} \PMlinkescapeword{exact form} \PMlinkescapeword{exact forms} \PMlinkescapeword{focus} \PMlinkescapeword{Focus} \PMlinkescapeword{graph} \PMlinkescapeword{Graph} \PMlinkescapeword{graphs} \PMlinkescapeword{Graphs} \PMlinkescapeword{interpretation} \PMlinkescapeword{Interpretation} \PMlinkescapeword{ma} \PMlinkescapeword{MA} \PMlinkescapeword{meagre} \PMlinkescapeword{Meagre} \PMlinkescapeword{mean} \PMlinkescapeword{Mean} \PMlinkescapeword{means} \PMlinkescapeword{Means} \PMlinkescapeword{moment} \PMlinkescapeword{Moment} \PMlinkescapeword{moments} \PMlinkescapeword{Moments} \PMlinkescapeword{moment's} \PMlinkescapeword{Moment's} \PMlinkescapeword{project} \PMlinkescapeword{Project} \PMlinkescapeword{qed} \PMlinkescapeword{QED} \PMlinkescapeword{reflect} \PMlinkescapeword{Reflect} \PMlinkescapeword{reflection} \PMlinkescapeword{Reflection} \PMlinkescapeword{represent} \PMlinkescapeword{Represent} \PMlinkescapeword{representation} \PMlinkescapeword{Representation} \PMlinkescapeword{representations} \PMlinkescapeword{Representations} \PMlinkescapeword{scheme} \PMlinkescapeword{Scheme} \PMlinkescapeword{simple} \PMlinkescapeword{Simple} \PMlinkescapeword{spectrum} \PMlinkescapeword{Spectrum} \PMlinkescapeword{state} \PMlinkescapeword{State} \PMlinkescapeword{structure} \PMlinkescapeword{Structure} \PMlinkescapeword{system} \PMlinkescapeword{System} \PMlinkescapeword{systems} \PMlinkescapeword{Systems} \PMlinkescapeword{volume} \PMlinkescapeword{Volume} Initial discussion of \textbf{logical graphs} is given in the \PMlinkname{Topic Introduction}{LogicalGraph}. \tableofcontents \section{Formal development} The next order of business is to give the exact forms of the axioms that are used in the following more formal development, devolving from Peirce's various systems of logical graphs via Spencer-Brown's \textit{Laws of Form} (LOF). In formal proofs, a variation of the annotation scheme from LOF will be used to mark each step of the proof according to which axiom, or \textit{initial}, is being invoked to justify the corresponding step of syntactic transformation, whether it applies to graphs or to strings. \subsection{Axioms} The axioms are just four in number, divided into the \textit{arithmetic initials}, $I_1$ and $I_2,$ and the \textit{algebraic initials}, $J_1$ and $J_2.$ \begin{center}\begin{tabular}{cc} \includegraphics[scale=0.8]{LogicalGraphFigure20} & (20) \\ \\ \includegraphics[scale=0.8]{LogicalGraphFigure21} & (21) \\ \\ \includegraphics[scale=0.8]{LogicalGraphFigure22} & (22) \\ \\ \includegraphics[scale=0.8]{LogicalGraphFigure23} & (23) \\ \end{tabular}\end{center} One way of assigning logical meaning to the initial equations is known as the \textit{entitative interpretation} (EN). Under EN, the axioms read as follows: \begin{center}$\begin{array}{ccccc} I_1 & : & \operatorname{true}\ \operatorname{or}\ \operatorname{true} & = & \operatorname{true} \\ I_2 & : & \operatorname{not}\ \operatorname{true}\ & = & \operatorname{false} \\ J_1 & : & a\ \operatorname{or}\ \operatorname{not}\ a & = & \operatorname{true} \\ J_2 & : & (a\ \operatorname{or}\ b)\ \operatorname{and}\ (a\ \operatorname{or}\ c) & = & a\ \operatorname{or}\ (b\ \operatorname{and}\ c) \\ \end{array}$\end{center} Another way of assigning logical meaning to the initial equations is known as the \textit{existential interpretation} (EX). Under EX, the axioms read as follows: \begin{center}$\begin{array}{ccccc} I_1 & : & \operatorname{false}\ \operatorname{and}\ \operatorname{false} & = & \operatorname{false} \\ I_2 & : & \operatorname{not}\ \operatorname{false} & = & \operatorname{true} \\ J_1 & : & a\ \operatorname{and}\ \operatorname{not}\ a & = & \operatorname{false} \\ J_2 & : & (a\ \operatorname{and}\ b)\ \operatorname{or}\ (a\ \operatorname{and}\ c) & = & a\ \operatorname{and}\ (b\ \operatorname{or}\ c) \\ \end{array}$\end{center} All of the axioms in this set have the form of equations. This means that all of the inference steps that they allow are reversible. The proof annotation scheme employed below makes use of a double bar $^{\underline{\overline{~~~~~~}}}$ to mark this fact, although 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. \subsection{Frequently used theorems} The actual business of proof is a far more strategic affair than the simple cranking of inference rules might suggest. Part of the reason for this lies in the circumstance that the usual brands of inference rules combine the moving forward of a state of inquiry with the losing of information along the way that doesn't appear to be immediately relevant, at least, not as viewed in the local focus and the short run of the moment to moment proceedings 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 that one had strategically thought to forget in earlier stages of the proof, if ``before the proof started" can be counted as an earlier stage of the proof in view. This is just one of the reasons that it can be very instructive to study equational inference rules of the sort that 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. By way of gaining a minimal experience with how equational proofs look in the present forms of syntax, let us examine the proofs of a few essential theorems in the primary algebra. \subsubsection{$C_1$. Double negation theorem} The first theorem goes under the names of \textit{Consequence~1} $(C_1)$, the \textit{double negation theorem} (DNT), or \textit{Reflection}. \begin{center}\begin{tabular}{cc} \includegraphics[scale=0.8]{LogicalGraphFigure24} & (24) \\ \end{tabular}\end{center} The proof that follows is adapted from the one that was given by George Spencer Brown in his book \textit{Laws of Form} (LOF) and credited to two of his students, John Dawes and D.A. Utting. \begin{center}\begin{tabular}{cc} \includegraphics[scale=0.8]{LogicalGraphFigure25} & (25) \\ \end{tabular}\end{center} \begin{center}\begin{tabular}{cc} \includegraphics[scale=0.8]{LogicalGraphFigure26} & (26) \\ \end{tabular}\end{center} \subsubsection{$C_2$. Generation theorem} One theorem of frequent use goes under the nickname of the \textit{weed and seed theorem} (WAST). The proof is just an exercise in mathematical induction, once a suitable basis is laid down, and it will be left as an exercise for the reader. What the WAST says is that a label can be freely distributed or freely erased anywhere in a subtree whose root is labeled with that label. The second in our list of frequently used theorems is in fact the base case of this weed and seed theorem. In LOF, it goes by the name of \textit{Consequence~2} $(C_2)$ or \textit{Generation}. \begin{center}\begin{tabular}{cc} \includegraphics[scale=0.8]{LogicalGraphFigure27} & (27) \\ \end{tabular}\end{center} Here is a proof of the Generation Theorem. \begin{center}\begin{tabular}{cc} \includegraphics[scale=0.8]{LogicalGraphFigure28} & (28) \\ \end{tabular}\end{center} \subsubsection{$C_3$. Dominant form theorem} The third of the frequently used theorems of service to this survey is one that Spencer-Brown annotates as \textit{Consequence~3} $(C_3)$ or \textit{Integration}. A better mnemonic might be \textit{dominance and recession theorem} (DART), but perhaps the brevity of \textit{dominant form theorem} (DFT) is sufficient reminder of its double-edged role in proofs. \begin{center}\begin{tabular}{cc} \includegraphics[scale=0.8]{LogicalGraphFigure29} & (29) \\ \end{tabular}\end{center} Here is a proof of the Dominant Form Theorem. \begin{center}\begin{tabular}{cc} \includegraphics[scale=0.8]{LogicalGraphFigure30} & (30) \\ \end{tabular}\end{center} \subsection{Exemplary proofs} Using no more than the axioms and theorems recorded so far, it is already possible to prove a multitude of much more complex theorems. A couple of all-time favorites are given next. \subsubsection{Peirce's law} Peirce's law is commonly written in the following form: \[ ((p \Rightarrow q) \Rightarrow p) \Rightarrow p \] The existential graph representation of Peirce's law is shown in Figure~31. \begin{center}\begin{tabular}{cc} \includegraphics[scale=0.8]{LogicalGraphFigure31} & (31) \\ \end{tabular}\end{center} A graphical proof of Peirce's law is shown in Figure~32. \begin{center}\begin{tabular}{cc} \includegraphics[scale=0.8]{LogicalGraphFigure32} & (32) \\ \end{tabular}\end{center} \textbf{Cf.} \PMlinkname{Peirce's Law}{PeircesLaw}. \subsubsection{Praeclarum theorema} An illustrious example of a propositional theorem is the \textit{praeclarum theorema}, the \textit{admirable}, \textit{shining}, or \textit{splendid} theorem of Leibniz. \begin{quote} If $a$ is $b$ and $d$ is $c$, then $ad$ will be $bc$. This is a fine theorem, which is proved in this way: $a$ is $b$, therefore $ad$ is $bd$ (by what precedes), $d$ is $c$, therefore $bd$ is $bc$ (again by what precedes), $ad$ is $bd$, and $bd$ is $bc$, therefore $ad$ is $bc$. Q.E.D. (Leibniz, \textit{Logical Papers}, p. 41). \end{quote} Under the existential interpretation, the praeclarum theorema is represented by means of the following logical graph equation. \begin{center}\begin{tabular}{cc} \includegraphics[scale=0.8]{LogicalGraphFigure33} & (33) \\ \end{tabular}\end{center} And here's a neat proof of that nice theorem. \begin{center}\begin{tabular}{cc} \includegraphics[scale=0.8]{LogicalGraphFigure34} & (34) \\ \end{tabular}\end{center} \textbf{Cf.} \PMlinkname{Praeclarum Theorema}{PraeclarumTheorema}. \section{Bibliography} \begin{itemize} \item Leibniz, Gottfried W. (1679--1686 ?), ``Addenda to the Specimen of the Universal Calculus'', pp. 40--46 in G.H.R. Parkinson (ed., trans., 1966), \textit{Leibniz : Logical Papers}, Oxford University Press, London, UK. \item Peirce, Charles Sanders (1931--1935, 1958), \textit{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). \item Peirce, Charles Sanders (1981--), \textit{Writings of Charles S. Peirce : A Chronological Edition}, Peirce Edition Project (eds.), Indiana University Press, Bloomington and Indianopolis, IN. Cited as (CE volume, page). \item Peirce, Charles Sanders (1885), ``On the Algebra of Logic : A Contribution to the Philosophy of Notation'', \textit{American Journal of Mathematics} 7 (1885), 180--202. Reprinted as CP 3.359--403 and CE 5, 162--190. \item Peirce, Charles Sanders (c. 1886), ``Qualitative Logic'', MS 736. Published as pp. 101--115 in Carolyn Eisele (ed., 1976), \textit{The New Elements of Mathematics by Charles S. Peirce, Volume 4, Mathematical Philosophy}, Mouton, The Hague. \item Peirce, Charles Sanders (1886 a), ``Qualitative Logic'', MS 582. Published as pp. 323--371 in \textit{Writings of Charles S. Peirce : A Chronological Edition, Volume 5, 1884--1886}, Peirce Edition Project (eds.), Indiana University Press, Bloomington and Indianopolis, IN, 1993. \item Peirce, Charles Sanders (1886 b), ``The Logic of Relatives : Qualitative and Quantitative'', MS 584. Published as pp. 372--378 in \textit{Writings of Charles S. Peirce : A Chronological Edition, Volume 5, 1884--1886}, Peirce Edition Project (eds.), Indiana University Press, Bloomington and Indianopolis, IN, 1993. \item Spencer Brown, George (1969), \textit{Laws of Form}, George Allen and Unwin, London, UK. \end{itemize}