12,080
edits
Changes
Directory:Jon Awbrey/Papers/Futures Of Logical Graphs (view source)
Revision as of 14:23, 29 July 2009
, 14:23, 29 July 2009convert graphics + other revisions
Notice that all of the axioms in this set have the form of equations. This means that all of the inference steps they allow are reversible. In the proof annotation scheme below, I will use a double bar "=====" to mark this fact, but I may at times leave it to the reader to pick which direction is the one required for applying the indicated axiom.
Notice that all of the axioms in this set have the form of equations. This means that all of the inference steps they allow are reversible. In the proof annotation scheme below, I will use a double bar "=====" to mark this fact, but I may at times leave it to the reader to pick which direction is the one required for applying the indicated axiom.
==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.
For this reason, among others, it is 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 conventional 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, I will lay out the proofs of a few essential theorems in the primary algebra.
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.
====Double negation theorem====
===C<sub>1</sub>. Double negation theorem===
The first theorem goes under the names of ''Consequence 1'' <math>(C_1)\!</math>, the ''double negation theorem'' (DNT), or ''Reflection''.
The first theorem goes under the names of ''Consequence 1'' <math>(C_1)\!</math>, the ''double negation theorem'' (DNT), or ''Reflection''.
|}
|}
===Weed and seed theorem===
===C<sub>2</sub>. Generation theorem===
One theorem of frequent use is what I like to call the ''Weed and Seed Theorem''. The proof is just an inductive exercise, so I will let it go till later, but it says that a label can be freely distributed or freely erased (retracted or withdrawn) anywhere in a subtree whose root is labeled with that label. The second theorem on the list to be shown here is actually the base case of this Weed and Seed theorem. I talk about it under the LOF name of ''Generation''.
One theorem of frequent use goes under the nickname of the ''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 names of ''Consequence 2'' <math>(C_2)\!</math> or ''Generation''.
{| align="center" cellpadding="10"
| [[Image:Logical_Graph_Figure_27.jpg|500px]]
|}
| ` ` ` ` ` ` ` ` b o ` ` ` ` ` ` ` ` a o b ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
Here is a proof of the Generation Theorem.
Here is a proof of the Generation Theorem.
{| align="center" cellpadding="10"
| [[Image:Logical_Graph_Figure_28.jpg|500px]]
|}
| ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
Now that we've seen a few — very simple but still non-trivial — examples of semiotic processes, namely, ones which fall under the headings of logical computation, evaluation, and proof, there are a number of questions that typically arise with respect to the relationship between sign relations and sign processes.
Now that we've seen a few — very simple but still non-trivial — examples of semiotic processes, namely, ones which fall under the headings of logical computation, evaluation, and proof, there are a number of questions that typically arise with respect to the relationship between sign relations and sign processes.
For concreteness, let's consider the example of logical evaluation that we looked at in Note 15.
For concreteness, let's consider the example of logical evaluation that we looked at in Note 15.
Cf: FOLG 15. http://stderr.org/pipermail/inquiry/2005-October/003134.html
: Cf: [http://stderr.org/pipermail/inquiry/2005-October/003134.html FOLG 15]
In: FOLG. http://stderr.org/pipermail/inquiry/2005-October/thread.html#3104
: In: [http://stderr.org/pipermail/inquiry/2005-October/thread.html#3104 FOLG]
<pre>
<pre>
One of the things that makes this sign sequence so special, amidst the generations of other sign sequences that can be generated from the sign relation of the primary arithmetic, is that it goes from a relatively obscure and verbose sign to an optimally clear and succinct sign for the same thing. For all its simplicity, then, it possesses a property that is characteristic of a semiotic process known as ''inquiry''.
One of the things that makes this sign sequence so special, amidst the generations of other sign sequences that can be generated from the sign relation of the primary arithmetic, is that it goes from a relatively obscure and verbose sign to an optimally clear and succinct sign for the same thing. For all its simplicity, then, it possesses a property that is characteristic of a semiotic process known as ''inquiry''.
===Dominant form theorem===
===C<sub>3</sub>. Dominant form theorem===
The third theorem that we will have need of here is one that GSB annotates as ''Integration'', but I tend to count it as being more a question of ''Dominance and Recession'' among formal expressions.
The third of the frequently used theorems of service to this survey is one that Spencer-Brown annotates as ''Consequence 3'' <math>(C_3)\!</math> or ''Integration''. A better mnemonic might be ''dominance and recession theorem'' (DART), but perhaps the brevity of ''dominant form theorem'' (DFT) is sufficient reminder of its double-edged role in proofs.
{| align="center" cellpadding="10"
| [[Image:Logical_Graph_Figure_29.jpg|500px]]
|}
| ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
Here is a proof of the ''Dominant Form Theorem''.
Here is a proof of the Dominant Form Theorem.
{| align="center" cellpadding="10"
| [[Image:Logical_Graph_Figure_30.jpg|500px]]
|}
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
==Exemplary proofs==
==Exemplary proofs==