12,089
edits
Changes
→Formal development: ASCII → JPEG
===Frequently used theorems===
===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 also be counted as an earlier stage of the proof in view.
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.
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.
The first theorem goes under the names of ''Consequence 1'' (C<sub>1</sub>), the ''double negation theorem'' (DNT), or ''Reflection''.
The first theorem goes under the names of ''Consequence 1'' (C<sub>1</sub>), the ''double negation theorem'' (DNT), or ''Reflection''.
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:Logical_Graph_Figure_24.jpg|500px]] || (24)
| C_1. Double Negation Theorem |
|}
| |
| |
| ((a)) = a |
The proof that follows is adapted from the one that was given by [[George Spencer Brown]] in his book ''Laws of Form'' (LOF), and credited to two of his students, John Dawes and D.A. Utting.
The proof that follows is adapted from the one that was given by [[George Spencer Brown]] in his book ''Laws of Form'' (LOF), and credited to two of his students, John Dawes and D.A. Utting.