[CG] Re: Theme One Program • Discussion

Cf: Theme One Program • Discussion 8 http://inquiryintoinquiry.com/2022/06/27/theme-one-program-discussion-8/ Re: Ontolog Forum https://groups.google.com/g/ontolog-forum/c/vlsQqvEiIkY ::: Alex Shkotin https://groups.google.com/g/ontolog-forum/c/vlsQqvEiIkY/m/m2ESSeyeBQAJ Re: Theme One Program • Exposition 4 https://inquiryintoinquiry.com/2022/06/20/theme-one-program-exposition-4/ Re: Logical Graphs • Animated Proofs https://oeis.org/wiki/User:Jon_Awbrey/ANIMATION#Proof_Animations <QUOTE AS:> The animation is mesmerizing: I would watch and watch. But without the pause, next frame, and playback speed settings, it's just a work of art that calls to see it step by step. And on page [1] ( https://oeis.org/wiki/Propositional_Equation_Reasoning_Systems ) you start with the double negation theorem. Have a look at a few of my comments as a reader, and only on the graph topic taken separately. <...> </QUOTE> Dear Alex, Thanks for viewing the animations and taking the time to work through that first proof. Clearly a lot could be done to improve the production values — what you see is what I got with whatever app I had umpteen years ago. For the time being I'm focusing on the implementation layer of the Theme One Program, which combines a learning component and a reasoning component. The first implements a two‑level sequence learner and the second implements a propositional calculator based on a variant of Peirce's logical graphs. (I meant to say more about the learning function this time around but I'm still working up to tackling that.) To address your comments and questions we'll need to step back for a moment to a more abstract, implementation-independent treatment of logical graphs. There's a number of resources along those lines linked on the following Survey page. Survey of Animated Logical Graphs https://inquiryintoinquiry.com/2021/05/01/survey-of-animated-logical-graphs… The blog post “Logical Graphs • Formal Development” ( https://inquiryintoinquiry.com/2008/09/19/logical-graphs-2/ ) gives a quick but systematic account of the formal system I use throughout. The OEIS wiki article “Logical Graphs” ( https://oeis.org/wiki/Logical_Graphs ) gives a more detailed development. Here's an excerpt from the above discussions, giving the four axioms or “initials” which serve as graphical transformation rules, in effect, the equational inference rules used to generate proofs and establish theorems or “consequences”. 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 The statement of the Double Negation Theorem is shown below. C1. 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.… The following proof is adapted from the one given by George Spencer Brown 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-proo… That should fill in enough background to get started on your questions … Regards, Jon