Date
1  6 of 6
Double Negation
All,
In my article on Logical Graphs, š https://oeis.org/wiki/Logical_Graphs I give the following discussion of Double Negation, š https://oeis.org/wiki/Logical_Graphs#C1._Double_negation Spencer Brown called this āConsequence 1ā (Cā). It's also known as the āDouble Negation Theoremā (DNT) or āReflectionā. Here's a picture of the theorem ā Figure 1. Double Negation Theorem (see also attached image) š https://oeis.org/w/images/2/27/Double_Negation_3.0.png Next time I'll give a proof adapted from the one Spencer Brown gave in his āLaws of Formā and credited to two of his students, John Dawes and D.A. Utting. For anyone who wants to read ahead, the axioms (or āinitialsā) used in the proof can be found in the following section of the Logical Graphs article. š https://oeis.org/wiki/Logical_Graphs#Axioms Regards, Jon


Cf: Double Negation ā¢ 1
http://inquiryintoinquiry.com/2021/02/14/doublenegation1/ All, I rewrote my last post a little more clearly, for ease of reference including the exact set of axioms or initials to be used in the proof of double negation to follow next time. The article and section linked below introduces the Double Negation Theorem (DNT) in the manner described as Consequence 1 (Cā) or Reflection by Spencer Brown. ā¢ Logical Graphs ( https://oeis.org/wiki/Logical_Graphs ) ā¢ Double Negation ( https://oeis.org/wiki/Logical_Graphs#C1._Double_negation ) Converting the planar figures used by Peirce and Spencer Brown to the graphtheoretic structures commonly used in mathematics and computer science, the double negation theorem takes the following form. Figure. Double Negation Theorem (see also attached) https://inquiryintoinquiry.files.wordpress.com/2021/02/doublenegation3.0.png The formal system of logical graphs is defined by a foursome of formal equations, called āinitialsā when regarded purely formally, in abstraction from potential interpretations, and called āaxiomsā when interpreted as logical equivalences. There are two arithmetic initials and two algebraic initials, as shown below. Arithmetic Initials =================== Axiom Iā https://inquiryintoinquiry.files.wordpress.com/2020/09/axiomi1.png Axiom Iā https://inquiryintoinquiry.files.wordpress.com/2020/09/axiomi2.png Algebraic Initials ================== Axiom Jā https://inquiryintoinquiry.files.wordpress.com/2020/09/axiomj1.png Axiom Jā https://inquiryintoinquiry.files.wordpress.com/2020/09/axiomj2.png Using these equations as transformation rules permits the development of formal consequences which may be interpreted as logical theorems. The double negation theorem is one such consequence. The proof of the double negation theorem I give next time is adapted from the one Spencer Brown presents in his Laws of Form and credits to two of his students, John Dawes and D.A. Utting. Resource ======== ā¢ Logic Syllabus ( https://inquiryintoinquiry.com/logicsyllabus/ ) Regards, Jon


Armahedi Mahzar
Dear Jon. We only need algebraic axioms, because cancelation (())= is the consequence of reflexion ((x))=x and condensation ()() = () is the consequence of iteration xx=x. But, if we don't need independence for the basis, it is OK. Best regards Arma
On Monday, February 15, 2021, 12:34:29 AM GMT+7, Jon Awbrey <jawbrey@...> wrote: Cf: Double Negation ā¢ 1 All, I rewrote my last post a little more clearly, for ease of reference including the exact set of axioms or initials to be used in the proof of double negation to follow next time. The article and section linked below introduces the Double Negation Theorem (DNT) in the manner described as Consequence 1 (Cā) or Reflection by Spencer Brown. ā¢ Logical Graphs ( https://oeis.org/wiki/Logical_Graphs ) ā¢ Double Negation ( https://oeis.org/wiki/Logical_Graphs#C1._Double_negation ) Converting the planar figures used by Peirce and Spencer Brown to the graphtheoretic structures commonly used in mathematics and computer science, the double negation theorem takes the following form. Figure.Ā Double Negation Theorem (see also attached) The formal system of logical graphs is defined by a foursome of formal equations, called āinitialsā when regarded purely formally, in abstraction from potential interpretations, and called āaxiomsā when interpreted as logical equivalences.Ā There are two arithmetic initials and two algebraic initials, as shown below. Arithmetic Initials =================== Axiom Iā Axiom Iā Algebraic Initials ================== Axiom Jā Axiom Jā Using these equations as transformation rules permits the development of formal consequences which may be interpreted as logical theorems. The double negation theorem is one such consequence.Ā The proof of the double negation theorem I give next time is adapted from the one Spencer Brown presents in his Laws of Form and credits to two of his students, John Dawes and D.A. Utting. Resource ======== ā¢ Logic Syllabus ( https://inquiryintoinquiry.com/logicsyllabus/ ) Regards, Jon


Cf: Double Negation ā¢ 2
http://inquiryintoinquiry.com/2021/02/18/doublenegation2/  If we stand back for a moment to regard the structure of  an implicational logic, such as Whitehead and Russell's,  we see that it is fully contained in that of an equivalence  logic. The difference is in the kind of step used. In one  case expressions are detached at the point of implication,  in the other they are detached at the point of equivalence.   G. Spencer Brown ā¢ Laws of Form All, We have been exploring the properties of a simple but elegant formal system exhibiting useful applications to logic. This very simplicity helps us focus on core features of formal systems and logical reasoning in a far less cluttered environment than the general run of logical systems. Earlier we touched on the theme of duality sourcing the radiation of mathematical form into logical subject matter, a theme we'll touch on again. But while we have the simple but critical example of Double Negation in our sights let's use it to illustrate another central feature of logical graphs bearing on the mathematical infrastructure of logic. This is the power of using equational inference over and above implicational inference in proofs. Here again is the formal equation corresponding to the principle of double negation, shown below in graphtheoretic and traversalstring forms. Figure. Double Negation Theorem https://inquiryintoinquiry.files.wordpress.com/2021/02/doublenegation3.0.png Whether any principle is taken for an axiom or has to be proven as a theorem depends on the formal system at hand. In the present system double negation is a consequence of the following set of axioms. Axioms ====== The formal system of logical graphs is defined by a foursome of formal equations, called āinitialsā when regarded purely formally, in abstraction from potential interpretations, and called āaxiomsā when interpreted as logical equivalences. There are two arithmetic initials and two algebraic initials, as shown below. Arithmetic Initials =================== Axiom Iā https://inquiryintoinquiry.files.wordpress.com/2020/09/axiomi1.png Axiom Iā https://inquiryintoinquiry.files.wordpress.com/2020/09/axiomi2.png Algebraic Initials ================== Axiom Jā https://inquiryintoinquiry.files.wordpress.com/2020/09/axiomj1.png Axiom Jā https://inquiryintoinquiry.files.wordpress.com/2020/09/axiomj2.png Logical Interpretation ====================== One way of assigning logical meaning to the initial equations is known as the entitative interpretation (En). Under En, the axioms read as follows. Iā : true or true = true Iā : not true = false Jā : a or not a = true Jā : (a or b) and (a or c) = a or (b and c) Another way of assigning logical meaning to the initial equations is known as the existential interpretation (Ex). Under Ex, the axioms read as follows. Iā : false and false = false Iā : not false = true Jā : a and not a = false Jā : (a and b) or (a and c) = a and (b or c) Equational Inference ==================== Formal proofs in what follows employ a variation on Spencer Brown's annotation scheme to mark each step of proof according to which axiom is called to license the corresponding step of syntactic transformation, whether it applies to graphs or to strings. All the axioms in the above set have the form of equations. This means the inference steps they license are all reversible. The proof annotation scheme employs a double bar ====== to mark this fact, though 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. Here is the proof of Double Negation. Figure. Double Negation Theorem ā¢ Proof https://inquiryintoinquiry.files.wordpress.com/2021/02/doublenegationproof3.0.png 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 implicational inference rules combine the moving forward of a state of inquiry with the losing of whatever information along the way one did not think immediately relevant, at least, not as viewed in the local focus and short hauls of moment to moment progress of the proof in question. Over the long haul, this has the pernicious sideeffect of one being strategically forced to reconstruct much of the information one had strategically thought to forget in earlier stages of the proof, where ābefore the proof startedā may be counted as an earlier stage of the proof in view. This is one of the reasons it is instructive to study equational inference rules. Equational forms of reasoning are paramount in mathematics but they are less familiar to the student of conventional logic textbooks, who may find a few surprises here. Reference ========= ā¢ Spencer Brown, G. (1969), Laws of Form, George Allen and Unwin, London, UK, p. 118. Regards, Jon


Lyle Anderson
All,
Not sure if this is an Archenemies level Eureka, but after reading Jon's latest letter, it occurred toĀ me that the "equals" sign '=", should be read as "is indistinguishable in value from" because that is what it means.Ā 73, Lyle


Cf: Double Negation ā¢ 3
http://inquiryintoinquiry.com/2021/02/19/doublenegation3/ Re: Double Negation https://oeis.org/wiki/Logical_Graphs#C1._Double_negation 1. https://inquiryintoinquiry.com/2021/02/14/doublenegation1/ 2. https://inquiryintoinquiry.com/2021/02/18/doublenegation2/ The steps of the proof of double negation are replayed in the following animation. Double Negation Theorem ā¢ Animation (see also attached) https://inquiryintoinquiry.files.wordpress.com/2021/02/doublenegation2.0animation.gif Resource ======== ā¢ Logic Syllabus ( https://oeis.org/wiki/Logic_Syllabus ) ( https://inquiryintoinquiry.com/logicsyllabus/ ) Reference ========= ā¢ Spencer Brown, G. (1969), Laws of Form, George Allen and Unwin, London, UK. Regards, Jon

