Double Negation

[Jon Awbrey]

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

[Jon Awbrey]

Cf: Double Negation • 1
http://inquiryintoinquiry.com/2021/02/14/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 graph-theoretic 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/double-negation-3.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/axiom-i1.png

Axiom I₂
https://inquiryintoinquiry.files.wordpress.com/2020/09/axiom-i2.png

Algebraic Initials
==================

Axiom J₁
https://inquiryintoinquiry.files.wordpress.com/2020/09/axiom-j1.png

Axiom J₂
https://inquiryintoinquiry.files.wordpress.com/2020/09/axiom-j2.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/logic-syllabus/ )

Regards,

Jon

[Jon Awbrey]

Cf: Double Negation • 2
http://inquiryintoinquiry.com/2021/02/18/double-negation-2/

| 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
graph-theoretic and traversal-string forms.

Figure. Double Negation Theorem
https://inquiryintoinquiry.files.wordpress.com/2021/02/double-negation-3.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/axiom-i1.png

Axiom I₂
https://inquiryintoinquiry.files.wordpress.com/2020/09/axiom-i2.png

Algebraic Initials
==================

Axiom J₁
https://inquiryintoinquiry.files.wordpress.com/2020/09/axiom-j1.png

Axiom J₂
https://inquiryintoinquiry.files.wordpress.com/2020/09/axiom-j2.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/double-negation-proof-3.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 side-effect 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

[Jon Awbrey]

Cf: Double Negation • 3
http://inquiryintoinquiry.com/2021/02/19/double-negation-3/

Re: Double Negation
https://oeis.org/wiki/Logical_Graphs#C1._Double_negation
1. https://inquiryintoinquiry.com/2021/02/14/double-negation-1/
2. https://inquiryintoinquiry.com/2021/02/18/double-negation-2/

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/double-negation-2.0-animation.gif

Resource
========

• Logic Syllabus
( https://oeis.org/wiki/Logic_Syllabus )
( https://inquiryintoinquiry.com/logic-syllabus/ )

Reference
=========

• Spencer Brown, G. (1969), Laws of Form, George Allen and Unwin, London, UK.

Regards,

Jon