Logical Graphs • Formal Development

[Jon Awbrey]

Logical Graphs • Formal Development 1
• https://inquiryintoinquiry.com/2023/09/15/logical-graphs-formal-development-1/

Recap —

A first approach to logical graphs can be found in the article linked below.

Logical Graphs • First Impressions
• https://inquiryintoinquiry.com/2023/08/24/logical-graphs-first-impressions/

That introduces the initial elements of logical graphs and hopefully supplies
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.

Regards,

Jon

cc: https://www.academia.edu/community/VrW8bL
cc: https://mathstodon.xyz/@Inquiry/111070230310739613

[Jon Awbrey]

Logical Graphs • Formal Development 2
• https://inquiryintoinquiry.com/2023/09/16/logical-graphs-formal-development-2-2/

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

Regards,

Jon

[Jon Awbrey]

Logical Graphs • Formal Development 3
• https://inquiryintoinquiry.com/2023/09/17/logical-graphs-formal-development-3/

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

Regards,

Jon

cc: https://www.academia.edu/community/VqAaOV
cc: https://mathstodon.xyz/@Inquiry/111070230310739613

[Jon Awbrey]

Logical Graphs • Formal Development 4
• https://inquiryintoinquiry.com/2023/09/26/logical-graphs-formal-development-4/

Equational Inference —

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

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.

Regards,

Jon

cc: https://www.academia.edu/community/VrdjZl
cc: https://mathstodon.xyz/@Inquiry/111070230310739613

[Jon Awbrey]

Logical Graphs • Formal Development 5
• https://inquiryintoinquiry.com/2023/09/27/logical-graphs-formal-development-5/

Frequently Used Theorems —

A sense of how equational proofs develop in the present graphical syntax
can be gained by working through the proofs of a few essential 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

Regards,

Jon

cc: https://www.academia.edu/community/5AzooV
cc: https://mathstodon.xyz/@Inquiry/111070230310739613

[Jon Awbrey]

Logical Graphs • Formal Development 6
• https://inquiryintoinquiry.com/2023/09/28/logical-graphs-formal-development-6/

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

Generation Theorem
• https://inquiryintoinquiry.files.wordpress.com/2010/04/logicalgraphfigure271.jpg

Here is a proof of the Generation Theorem.

Generation Theorem • Proof
• https://inquiryintoinquiry.files.wordpress.com/2010/04/logicalgraphfigure281.jpg

Regards,

Jon

cc: https://www.academia.edu/community/l7GGel
cc: https://mathstodon.xyz/@Inquiry/111070230310739613

[Jon Awbrey]

Logical Graphs • Formal Development 7
• https://inquiryintoinquiry.com/2023/09/29/logical-graphs-formal-development-7/

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.files.wordpress.com/2010/04/logicalgraphfigure291.jpg

Here is a proof of the Dominant Form Theorem.

Dominant Form Theorem • Proof
• https://inquiryintoinquiry.files.wordpress.com/2010/04/logicalgraphfigure301.jpg
Regards,

Jon

cc: https://www.academia.edu/community/VXaQzL
cc: https://mathstodon.xyz/@Inquiry/111070230310739613

[Jon Awbrey]

Logical Graphs • Formal Development 8
• https://inquiryintoinquiry.com/2023/09/30/logical-graphs-formal-development-8/

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 couple of all‑time favorites are linked below.

Peirce's Law
• https://inquiryintoinquiry.com/2008/10/06/peirces-law/

Praeclarum Theorema
• https://inquiryintoinquiry.com/2008/10/05/praeclarum-theorema/

Regards,

Jon

cc: https://www.academia.edu/community/V03DO5
cc: https://mathstodon.xyz/@Inquiry/111070230310739613