Logical Graphs • Formal Development

[Jon Awbrey]

Logical Graphs • Formal Development 1
• https://inquiryintoinquiry.com/2024/09/12/logical-graphs-formal-development-1-a/

Recap —

A first approach to logical graphs was outlined in the article linked below.

Logical Graphs • First Impressions
• https://inquiryintoinquiry.com/2024/08/26/logical-graphs-first-impressions-a/

That introduced the initial elements of logical graphs and hopefully supplied
the reader with an intuitive sense of their motivation and rationale.

Formal Development —

Logical graphs are next presented as a formal system by going back to the
initial elements and developing their consequences in a systematic manner.

The next order of business is to give the precise axioms used to
develop the formal system of logical graphs. The axioms derive
from C.S. Peirce's various systems of graphical syntax via the
“calculus of indications” described in Spencer Brown's “Laws
of Form”.

The formal proofs to follow will use a variation of Spencer Brown's
annotation scheme to mark each step of the proof according to which
axiom is called to license the corresponding step of syntactic
transformation, whether it applies to graphs or to strings.

Resources —

Survey of Animated Logical Graphs
• https://inquiryintoinquiry.com/2024/03/18/survey-of-animated-logical-graphs-7/

Regards,

Jon

cc: https://www.academia.edu/community/ld361R
cc: https://mathstodon.xyz/@Inquiry/113129787112676868

[Jon Awbrey]

Logical Graphs • Formal Development 2
• https://inquiryintoinquiry.com/2024/09/13/logical-graphs-formal-development-2-a/

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/2023/09/logical-graph-axiom-i1-2.0.png

Axiom I₂
• https://inquiryintoinquiry.files.wordpress.com/2023/09/logical-graph-axiom-i2-2.0.png

Algebraic Initials —

Axiom J₁
• https://inquiryintoinquiry.files.wordpress.com/2023/09/logical-graph-axiom-j1-2.0.png

Axiom J₂
• https://inquiryintoinquiry.files.wordpress.com/2023/09/logical-graph-axiom-j2-2.0.png

Resources —

Survey of Animated Logical Graphs
• https://inquiryintoinquiry.com/2024/03/18/survey-of-animated-logical-graphs-7/

Regards,

Jon

cc: https://www.academia.edu/community/LbXK4D
cc: https://mathstodon.xyz/@Inquiry/113129787112676868

[Jon Awbrey]

Logical Graphs • Formal Development 3
• https://inquiryintoinquiry.com/2024/09/14/logical-graphs-formal-development-3-a/

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.

Logical Graphs • Entitative Interpretation
• https://inquiryintoinquiry.files.wordpress.com/2023/09/logical-graphs-e280a2-entitative-interpretation.png

Another way of assigning logical meaning to the initial equations
is known as the “existential interpretation” (Ex). Under Ex,
the axioms read as follows.

Logical Graphs • Existential Interpretation
• https://inquiryintoinquiry.files.wordpress.com/2023/09/logical-graphs-e280a2-existential-interpretation.png

Resources —

Survey of Animated Logical Graphs
• https://inquiryintoinquiry.com/2024/03/18/survey-of-animated-logical-graphs-7/

Regards,

Jon

cc: https://www.academia.edu/community/V91Rmw
cc: https://mathstodon.xyz/@Inquiry/113129787112676868

[Jon Awbrey]

Logical Graphs • Formal Development 4
• https://inquiryintoinquiry.com/2024/09/14/logical-graphs-formal-development-4-a/

Equational Inference —

All the initials I₁, I₂, J₁, J₂ have the form of equations.
This means the inference steps they license are reversible.
The proof annotation scheme employed below makes use of
double bars “══════” 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.

The actual business of proof is a far more strategic affair than the
routine cranking of inference rules might suggest. Part of the reason
for this lies in the circumstance that the customary types of inference
rules combine the moving forward of a state of inquiry with the losing
of information along the way that doesn't appear immediately relevant,
at least, not as viewed in the local focus and short run 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 one had strategically thought to forget at earlier stages
of proof, where “before the proof started” can be counted as an earlier
stage of the proof in view.

This is just one of the reasons it can be very instructive to study
equational inference rules of the sort 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.

Resources —

Survey of Animated Logical Graphs
• https://inquiryintoinquiry.com/2024/03/18/survey-of-animated-logical-graphs-7/

Regards,

Jon

cc: https://www.academia.edu/community/VBYW33
cc: https://mathstodon.xyz/@Inquiry/113129787112676868

[Jon Awbrey]

Logical Graphs • Formal Development 5
• https://inquiryintoinquiry.com/2024/09/14/logical-graphs-formal-development-5-a/

Frequently Used Theorems —

To familiarize ourselves with equational proofs
in logical graphs let's run though the proofs
of a few basic theorems in the primary algebra.

C₁. Double Negation Theorem —

The first theorem goes under the names of Consequence 1 (C₁),
the double negation theorem (DNT), or Reflection.

Double Negation Theorem
• https://inquiryintoinquiry.files.wordpress.com/2021/02/double-negation-3.0.png

The proof that follows is adapted from the one George Spencer Brown
gave in his book “Laws of Form” and credited to two of his students,
John Dawes and D.A. Utting.

Double Negation Theorem • Proof
• https://inquiryintoinquiry.files.wordpress.com/2021/02/double-negation-proof-3.0.png

Resources —

Survey of Animated Logical Graphs
• https://inquiryintoinquiry.com/2024/03/18/survey-of-animated-logical-graphs-7/

Regards,

Jon

cc: https://www.academia.edu/community/V0YXb0
cc: https://mathstodon.xyz/@Inquiry/113129787112676868

[Jon Awbrey]

Logical Graphs • Formal Development 6
• https://inquiryintoinquiry.com/2024/09/15/logical-graphs-formal-development-6-a/

Frequently Used Theorems (cont.) —

C₂. Generation Theorem —

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 the weed and seed theorem. In Laws of Form
it goes by the names of Consequence 2 (C₂) or Generation.

Generation Theorem
• https://inquiryintoinquiry.com/wp-content/uploads/2024/09/generation-theorem-1.0.jpg

Here is a proof of the Generation Theorem.

Generation Theorem • Proof
• https://inquiryintoinquiry.com/wp-content/uploads/2024/09/generation-theorem-proof-1.0.jpg

Resources —

Survey of Animated Logical Graphs
• https://inquiryintoinquiry.com/2024/03/18/survey-of-animated-logical-graphs-7/

Regards,

Jon

cc: https://www.academia.edu/community/l7ednb
cc: https://mathstodon.xyz/@Inquiry/113129787112676868

[Jon Awbrey]

Logical Graphs • Formal Development 7
• https://inquiryintoinquiry.com/2024/09/15/logical-graphs-formal-development-7-a/

Frequently Used Theorems (concl.) —

C₃. Dominant Form Theorem —

The third of the frequently used theorems of service to this survey
is one Spencer Brown annotates as Consequence 3 (C₃) 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.

Dominant Form Theorem
• https://inquiryintoinquiry.com/wp-content/uploads/2024/09/dominant-form-theorem-1.0.jpg

Here is a proof of the Dominant Form Theorem.

Dominant Form Theorem • Proof
• https://inquiryintoinquiry.com/wp-content/uploads/2024/09/dominant-form-theorem-proof-1.0.jpg

Resources —

Survey of Animated Logical Graphs
• https://inquiryintoinquiry.com/2024/03/18/survey-of-animated-logical-graphs-7/

Regards,

Jon

cc: https://www.academia.edu/community/VowE60
cc: https://mathstodon.xyz/@Inquiry/113129787112676868

[Jon Awbrey]

Logical Graphs • Formal Development 8
• https://inquiryintoinquiry.com/2024/09/16/logical-graphs-formal-development-8-a/

Exemplary Proofs —

Using no more than the axioms and theorems recorded so far,
it is possible to prove a multitude of much more complex
theorems. A number of all‑time favorites are linked below.

Peirce's Law
• https://inquiryintoinquiry.com/2023/10/18/peirces-law-a/
Blog Series
1. https://inquiryintoinquiry.com/2023/10/19/peirces-law-1/
2. https://inquiryintoinquiry.com/2023/10/20/peirces-law-2/
3. https://inquiryintoinquiry.com/2023/10/21/peirces-law-3/
4. https://inquiryintoinquiry.com/2023/10/22/peirces-law-4/
5. https://inquiryintoinquiry.com/2023/10/23/peirces-law-5/
6. https://inquiryintoinquiry.com/2023/10/24/peirces-law-6/
7. https://inquiryintoinquiry.com/2023/10/25/peirces-law-7/

Praeclarum Theorema
• https://inquiryintoinquiry.com/2023/10/05/praeclarum-theorema-a/
Blog Series
1. https://inquiryintoinquiry.com/2023/10/13/praeclarum-theorema-1/
2. https://inquiryintoinquiry.com/2023/10/14/praeclarum-theorema-2/
3. https://inquiryintoinquiry.com/2023/10/15/praeclarum-theorema-3/

Proof Animations
• https://oeis.org/wiki/User:Jon_Awbrey/ANIMATION#Proof_Animations

Resources —

Survey of Animated Logical Graphs
• https://inquiryintoinquiry.com/2024/03/18/survey-of-animated-logical-graphs-7/

Regards,

Jon

cc: https://www.academia.edu/community/543dbD
cc: https://mathstodon.xyz/@Inquiry/113129787112676868