Changes

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.

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, 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, I will lay out the proofs of a few essential theorems in the primary algebra.

==Double negation theorem==

====Double negation theorem====

The first theorem goes under the names of ''Consequence&nbsp;1'' <math>(C_1)\!</math>, the ''double negation theorem'' (DNT), or ''Reflection''.

The first theorem goes under the names of ''Consequence&nbsp;1'' <math>(C_1)\!</math>, the ''double negation theorem'' (DNT), or ''Reflection''.

|}

|}

==Weed and seed theorem==

===Weed and seed 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 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 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''.

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

o=============================< QED >=======================o

o=============================< QED >=======================o

</pre>

</pre>

Now to take up a more interesting example, here is the statement and a proof of the ''Splendid Theorem'' from Leibniz that was brought to my attention by John Sowa.

Now to take up a more interesting example, here is the statement and a proof of the ''Splendid Theorem'' from Leibniz that was brought to my attention by John Sowa.