Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: deprecated: logic

Topic: logical graphs


view this post on Zulip Jon Awbrey (Jul 03 2021 at 14:00):

Cf: Animated Logical Graphs • 77

A place for exploring animated forms of visual inference inspired by the work of C.S. Peirce and Spencer Brown.

view this post on Zulip Jon Awbrey (Jul 03 2021 at 16:00):

Cf: Animated Logical Graphs • 78

As far as the “animated” part goes, I lost my klutz-friendly animation app in my last platform change and then got immersed in other things, so it may be a while before I get back to that, but here's two examples of animated proofs in a CSP∫GSB-style propositional calculus just to give a hint of how things might develop.

view this post on Zulip Henry Story (Jul 03 2021 at 16:16):

I think in this 2020 Applied Category Theory talk by @Rocco Gangle A Generic Figures Reconstruction of Peirce's Existential Graphs (Alpha) he is looking at showing how Peirce's work can be expressed in terms of Category Theory.

view this post on Zulip Jon Awbrey (Jul 03 2021 at 16:40):

Cf: Animated Logical Graphs • 79

Henry Story said:

I think in this 2020 Applied Category Theory talk by Rocco Gangle, A Generic Figures Reconstruction of Peirce's Existential Graphs (Alpha), he is looking at showing how Peirce's work can be expressed in terms of Category Theory.

I looked at that once, I think, seem to recall he is still using the planar maps which I consider the mark of a novice, but I will give it another look.

view this post on Zulip Jon Awbrey (Jul 03 2021 at 16:50):

Okay, I see he introduces forests about half-way through, that's a good thing, but he's not up to cacti yet, which is something I found necessary early on for the sake of both conceptual and computational efficiency.  So there's a few things I will need to explain …

view this post on Zulip Jon Awbrey (Jul 03 2021 at 18:02):

I started working on logical graphs early in my undergrad years, after my first encounter with Peirce's Collected Papers, quickly followed by my study of Spencer Brown's Laws of Form, and from the outset trying everything I could hack by way of syntax handlers and theorem provers in every mix of languages and machines I got my hands on.  That combination of forces and media summed to form my current direction.

Peirce broke ground and laid the groundwork, Spencer Brown shored up the infrastructure of primary arithmetic and leveled the proving grounds to facilitate equational inference, and a host of computers supplied the real-world recalcitrance of matter, the resistance to facile simplicity, and the rebuke of all too facile reductionism.

view this post on Zulip Chad Nester (Jul 09 2021 at 07:10):

Re: categorical treatments of existential graphs, https://www.ioc.ee/~pawel/papers/peirce.pdf

view this post on Zulip Jon Awbrey (Jul 09 2021 at 12:12):

Cf: Animated Logical Graphs • 80

Chad Nester said:

Re: categorical treatments of existential graphs, https://www.ioc.ee/~pawel/papers/peirce.pdf

Re: Nathan Haydon and Paweł Sobociński • Compositional Diagrammatic First-Order Logic

Thanks, Chad, for that extremely nice treatment of Peirce's existential graphs at the β level, tantamount to predicate calculus or first order logic as we know it today.

The logic of relatives and the mathematics of relations appear in a different light from the perspective of Peirce's own standpoint on logic, evolving as it does out of distinctive pragmatic and semiotic insights.  The reflections of Spencer Brown afford a few angles Peirce anticipated but in a glass, darkly.  And my own time tumbling recalcitrant calculi toward more ready tools for inquiry may add a few wrinkles, with luck to more than my own brow.  All that will develop as we go.

view this post on Zulip Chad Nester (Jul 09 2021 at 14:54):

Recently a few of us have been using the "cartesian bicategories of relations" of Carboni and Walters, in particular their string diagrams, as syntax for relations. The string diagrams in question are more or less a directed version of Peirce's lines of identity. They're usually described in terms of commutative special frobenius algebras. I suspect the reason we keep finding commutative special frobenius algebras is that they support lines of identity in this way.

view this post on Zulip Henry Story (Jul 09 2021 at 15:05):

Knowledge Representation in Bicategories of Relations is also drawn up in terms of string diagrams, as a way of explaining the W3C RDF and OWL standards. So it looks like we have a nice route from Peirce to RDF via string diagrams. Or the other way around: whichever route one prefers to travel.

view this post on Zulip Henry Story (Jul 09 2021 at 16:22):

It could also be that there are missing features not captured by these mappings, and that would be useful to know about.
For one I think the bicategories of relations does not capture an aspect that requires Quads, or the deployment of RDF on web servers which would fall under pragmatics. (so there are spaces outside of Bicategories of relations that are important but not captured).
It could be that the pieces missing for a full account of the semweb are the same as those @Jon Awbrey feels is missing in the account of Peirce.
After all the Web as an engineering project, is first of all a pragmatic one. (Well: engineers should use mathematics during the course of planning, designing and testing).

view this post on Zulip AZ Andersons (Jul 09 2021 at 17:10):

Once one has shown that a system of symbols and rules can be completely mapped into First Order Logic, you really are done with First Order Logic (FOL). In FOL one can quantify over individuals, but not properties. @Jon Awbrey in his search for Differential Logic through his question, "what do you have to do to change p?", is, in my opinion, looking for Second Order Logic (SOL). In SOL you can assert that "a is a cube and b is a cube" and conclude that "there is a property that a and b share." Sew https://faculty.washington.edu/smcohen/120/SecondOrder.pdf You might also find Stanford University's take on ti interesting: https://plato.stanford.edu/entries/logic-higher-order/

My reason for being in this discussion is to explore the "Laws of Form" (LoF) as articulated by George Spencer-Brown. One of the important concepts in LoF is that they deal with distinctions and the naming of distinctions without specifying the domain of the distinction. That makes them applicable to individual things or to any aspect, facet, property, or characteristic of an individual thing. The LoF formalize the concept of "levels of abstraction", thus formally establishing the categories that Category Theory takes.

May the Form be with you!
Best regards,
Lyle

view this post on Zulip Henry Story (Jul 09 2021 at 17:12):

There is also modal logic. I saw it written that Peirce had some notations for that too. That could be missing from the first order part.

view this post on Zulip AZ Andersons (Jul 09 2021 at 18:12):

Henry,
Model logic would be talking about the "predicates" and that is what is added when one goes to the second order. If you want arcs and bubbles to talk about processes, then I suggest you explore the Data Flow Diagrams of "Structured Analysis and System Specification" by Tom DeMarco. It takes you though the steps of modeling the current system, converting that physical model to a logical, i.e. implementation independent, model. of the current system, creating the logical model of the new system, and finally the physical model of the new system. We used it, along with an automated documentation tool I developed to quadruple military software productivity in the early 1980s. That is when I learned about sticking my head up above the crowd. I bought extra copies after it wen out of print, and would be happy to send you one if you like.
May the Form be with you!
Best regards,
Lyle

view this post on Zulip Johannes Drever (Jul 09 2021 at 18:17):

Speaking of Laws of Form: There is a paper called "The Laws of Form As A Categorical Algebra". It is not published anywhere and it seems to orginate from a sci.math.* mailing list. The author is not specified. Does anyone know who could be the author? ..It sounds quite interesting:

However, the categorical logic underlying the Spencer Brown system goes beyond merely a categorification of the proof theory of Boolean logic. It generalizes to a categorical proof theory for ortholattices; thus, also to Quantum logic. This serves to complete the analogy (Curry-Howard:Intuitionistic logic) = (???: “Ortho”-logic).

view this post on Zulip Henry Story (Jul 09 2021 at 18:20):

@AZ Andersons wrote

Model logic would be talking about the "predicates" and that is what is added when one goes to the second order.

Is Model logic the same as Modal logic? (I guess they are quite closely related, as Modal logic allows one quantify over the models, right?).
Things roughly like:
P    wW,wP \Box P \iff \forall w \in W, w \in P
(where w ranges over worlds, or states, ...)

view this post on Zulip AZ Andersons (Jul 09 2021 at 18:49):

don't kno off hand. Ask Google!

view this post on Zulip Henry Story (Jul 09 2021 at 18:51):

ok. It was just that I mentioned "modal logics" above, and you answered with "model logic" :-)

view this post on Zulip Jon Awbrey (Jul 09 2021 at 19:48):

Johannes Drever said:

Speaking of Laws of Form: There is a paper called "The Laws of Form As A Categorical Algebra". It is not published anywhere and it seems to orginate from a sci.math.* mailing list. The author is not specified. Does anyone know who could be the author? It sounds quite interesting:

However, the categorical logic underlying the Spencer Brown system goes beyond merely a categorification of the proof theory of Boolean logic. It generalizes to a categorical proof theory for ortholattices; thus, also to Quantum logic. This serves to complete the analogy (Curry-Howard:Intuitionistic logic) = (???: “Ortho”-logic).

It was uploaded by Rock Brentwood and the Document Information says:

This is a reformatting of an couple articles I posted on the USENET in sci.math.* in the 1990's that presents Spencer-Brown's Laws of Form as a categorical logic, along the same lines as Lambek-Scott (for instance), by bringing out the latent categorical concept that already underlay his original presentation.

So RB appears to be the author?

view this post on Zulip AZ Andersons (Jul 09 2021 at 20:36):

Auto-correct strikes again.

view this post on Zulip Johannes Drever (Jul 10 2021 at 07:48):

Thanks! For some reasons I thought he only uploaded the paper. He still is active and commenting in the nforum.

view this post on Zulip Jon Awbrey (Jul 16 2021 at 10:28):

@Henry Story said:

Knowledge Representation in Bicategories of Relations is also drawn up in terms of string diagrams, as a way of explaining the W3C RDF and OWL standards. So it looks like we have a nice route from Peirce to RDF via string diagrams. Or the other way around: whichever route one prefers to travel.

@Henry Story said:

It could also be that there are missing features not captured by these mappings, and that would be useful to know about.
For one I think the bicategories of relations does not capture an aspect that requires Quads, or the deployment of RDF on web servers which would fall under pragmatics. (so there are spaces outside of Bicategories of relations that are important but not captured).
It could be that the pieces missing for a full account of the semweb are the same as those Jon Awbrey feels is missing in the account of Peirce.
After all the Web as an engineering project, is first of all a pragmatic one. (Well: engineers should use mathematics during the course of planning, designing and testing).

I'm still waiting for my copy of Diagrammatic Immanence — last word was it should arrive Monday :fingers_crossed: — the previews I get from Google are too skimpy on Peirce and seem to vary from device to device :shrug: so maybe I can get back to this next week.

view this post on Zulip Henry Story (Jul 16 2021 at 16:39):

I hope it did not cost too much for you.
I will be having to get back to programming very soon, which is where I get paid...

view this post on Zulip Jon Awbrey (Jul 16 2021 at 18:00):

Henry Story said:

I hope it did not cost too much for you.
I will be having to get back to programming very soon, which is where I get paid ...

Not too bad, found a paperback copy for under $30 —
oldtimer gotta have print if he's actually gonna study it.
Maybe I can use the meantime to clear up some issues. More coffee :coffee: first …

view this post on Zulip Jon Awbrey (Jul 28 2021 at 18:00):

Cf: Logical Graphs • Discussion 1

Re: Laws of FormJohn Mingers

John Mingers writes,

I find it very frustrating not to be able to draw crosses and expressions within emails or Word documents.  Does anyone know of any software or apps that can do this?  If not, with so many computer scientists on this group, could someone produce something?

People with backgrounds in computing, combinatorics, or graph theory would immediately recognize Spencer Brown’s expressions are isomorphic to what graph theorists know and love as “trees”, more specifically “rooted trees”, with a particular manner of attaching letters to the nodes to be described later.  In those fields there’s a standard way of mapping trees to strings of parentheses and letters.  This operation is called “traversing the tree” when one passes from trees to strings and the reverse operation is called “parsing the string” when one passes from strings to trees.

The transformation of Spencer Brown’s simple closed figures in the plane or his formal expressions of “crosses” into rooted trees, together with the further transformation of those two forms to “pointer data structures” in computer memory is, discussed in the following post on my blog.

There’s a more formal presentation of logical graphs, working from the axioms or “initials” I borrowed with modifications from Peirce and Spencer Brown, in the following blog post.

Those two pieces are combined and extended in the following article.

The program I developed all through the 80s using those data structures in its logic module is documented so far as I’ve done to date on the following page.

view this post on Zulip Jon Awbrey (Jul 29 2021 at 18:40):

Cf: Logical Graphs • Discussion 2

Chad Nester said:

Recently a few of us have been using the "cartesian bicategories of relations" of Carboni and Walters, in particular their string diagrams, as syntax for relations. The string diagrams in question are more or less a directed version of Peirce's lines of identity. They're usually described in terms of commutative special frobenius algebras. I suspect the reason we keep finding commutative special frobenius algebras is that they support lines of identity in this way.

Chaos rules my niche of the world right now so I'll just break a bit of the ice by sharing a few links to my ongoing study of Peirce's 1870 Logic Of Relatives.

See especially the following paragraph.

To my way of thinking the above paragraph is one of the most radical passages in the history of logic, relativizing traditional assumptions of an absolute distinction between generals (universals) and individuals.  Among other things, it pulls the rug out from under any standing for nominalism as opposed to realism about universals.

view this post on Zulip Chad Nester (Jul 30 2021 at 13:34):

Thanks Jon. I'll have a look!

view this post on Zulip Jon Awbrey (Aug 01 2021 at 03:36):

Chad Nester said:

Thanks Jon. I'll have a look!

I opened another topic for discussing this view of relation theory.

view this post on Zulip Henry Story (Aug 01 2021 at 09:50):

The talks for ACT2021 have been published and the first one that caught my attention was the July 16th Graphical Regular Logic given by @tslil (they) . It gives an overview of recent work on the subject, and brings the subject a lot further along, in ways that I can't of course fully appreciate, not have read David Spivak and @Brendan Fong's work on Regular Logic.

view this post on Zulip Henry Story (Aug 01 2021 at 09:57):

I have though, studied @Evan Patterson's Knowledge Representation in Bicategories of Relations carefully, as that directly applied to the work on the W3C Semantic Web RDF and OWL which has occupied me for the past 16 years or so.

Tslil's work extends that to n-ary relations, and helps put the work into context.
N-ary relations could be of interest to the parallel ISO standardisation effort known as Comon Logic, as I believe they have n-ary relations, and are following the same structure as RDF: that is starting by fixing semantics, and allow syntax to vary.

The beauty of binary relations is that they are very easy to explain, which, when dealing with standards, is very important.
What I like about Evan's paper is that it also looks at complementing regular logic with its dual, giving us geometric logic, which is equivalent to full first order logic. Is that dual work being left out of these developments?

view this post on Zulip Henry Story (Aug 01 2021 at 10:14):

In his presentation @tslil (they) mentions contexts which are somehow associated with n-ary relations. That sounds very intriguing. I have the feeling that contexts emerge out of higher ordered networks such as simplicial sets. As @tslil (they) is a student of @Emily Riehl and her book on ncategories starts with simplicial sets (the first 2 pages I was able to follow!), that seems like where it could be going. That is the word "context" has quite a history in logic and philosophy (a few pointers) which in my view relates it to modal logic, so I hope it is not used just as a shorthand for nary relations... (unless there is some structural magic to n-ary relations that I am unaware of).

view this post on Zulip Jon Awbrey (Aug 01 2021 at 10:48):

Is this regular in the sense of regular expressions, finite state automata, or something else?

view this post on Zulip Henry Story (Aug 01 2021 at 10:54):

I don't know where "regular" comes from, but it is logic with just Truth, conjunction, existential quantification and equality. Screenshot from minute 10:21 of the talk
That seems particularly useful to make factual statements, that one can add to a database. Say if one has a database in which one only wants to put true statements, then one can just always add (conjunction) new true statements without worrying about their interaction with other statements.

The extension with disjunction and False gives what is now known as coherent logic (according to E. Patterson's paper) , which used to be known as Geometric Logic.

Universal quantification
Universal quantification can then be brought in as shown above.

view this post on Zulip Morgan Rogers (he/him) (Aug 01 2021 at 11:07):

Henry Story said:

What I like about Evan's paper is that it also looks at complementing regular logic with its dual, giving us geometric logic, which is equivalent to full first order logic. Is that dual work being left out of these developments?

Careful, geometric logic is not the same as first order logic!!

view this post on Zulip Henry Story (Aug 01 2021 at 11:08):

I think Evans and other claim that geometric and first order logic are somehow equivalent - or at least as expressive as one another. I don't know the details.
Looking to understand geometric logic, I came across this helpful page on Skolem machines https://skolemmachines.org

view this post on Zulip Morgan Rogers (he/him) (Aug 01 2021 at 11:23):

There's a process called Morleyization for turning any (infinitary) first order theory into a coherent (resp. geometric) theory with the same models in any Boolean topos, in particular giving the same Set models, so geometric logic is as expressive in that sense.

view this post on Zulip Jon Awbrey (Aug 01 2021 at 11:40):

Spent/wasted some of the better years/decades of my life in the early SUO (Standard Upper Ontology) Working Group, W³C, Ontolog Forum 1.0, and still kibitz on the Ontolog Forum 2.0.  Know about Common Logic from long interaction in many groups with John Sowa, read his Conceptual Structures, one of the revivals of Peirce's logical graphs, back in '84, and participated briefly on the Common Logic Dev List.

To make a long story barely bearable, what I've learned from all these experiences is mostly a few things about the power of legacies to keep on legating no matter what.

view this post on Zulip Henry Story (Aug 01 2021 at 11:50):

As a thorough reader of Nietzsche (as I was 16 in the early 1980ies) I would have also been very suspicious of the semantic web, had I been convinced that I needed to go through upper ontologies, which would it seem be a form of Platonism. That worry was put to rest for me by reading Ruth Garett Millikan's Thought, Language and Other Biological Categories, a beautiful book that puts language and thought back into the biological reproductive space. That is a thought that pre-covid would have many people tremble. But I think we are now beyond that. The semantic web should be looked at as an evolutionary writing system, that grows by applications being used to intermediate human agents to other human and robotic agents. There is no need for a final upper ontology to get that to work.
At the same time, I am not against research in that space either. There is something about schemas that still has that Platonic flavor: functors from small shapes in the heavenly space of forms to our mixed world of Sets...

view this post on Zulip Jon Awbrey (Aug 01 2021 at 11:54):

It may be Fall before I get moderately organized again — too many things put off for the duration are now crying out for reckoning — but I'm working up to mapping the fork in the yarrow wood that Peirce took and how I came to follow it.  You'll thank me later …

view this post on Zulip Henry Story (Aug 01 2021 at 11:58):

There is also the continuation of work from Modal Logic by David Lewis in a pragmatic direction from his student Robert Brandom, (very much appreciated by @David Corfield) which I think would be also compatible with the semantic web. As apps intermediate humans that are trying to coordinate actions to get things done, these apps need to keep track of who said what (context) in order to allow the person using the app to decide whether to trust a statement found on the web, and use it for further reasoning. This is the game of giving and asking for reasons - which on the semweb is not fully automatiseable.

view this post on Zulip Henry Story (Aug 01 2021 at 12:00):

Anyway, that brought us a bit away from work on graphical logic discussed above. But it does bring in important questions as to how these logics tie into pragmatics and modal logic.

view this post on Zulip Jon Awbrey (Aug 01 2021 at 12:28):

Modal Logic, along with logics for tense and intension, have been a recurring (recursèd) topic for as long as I can remember, big debates going back to my Quine days, and it just came up again on both the Ontolog and Peirce lists, but I pretty much said the best I know some years ago.

It is critical to understand the pragmatic semiotic information-theoretic perspective going back to Peirce's earliest breakthroughs well anticipated and avoided in advance all the pet boondoggles of logical atomism and so-called analytic philosophy.

view this post on Zulip Henry Story (Aug 01 2021 at 12:35):

There have been quite a few threads discussing modalities here.

view this post on Zulip Jon Awbrey (Aug 01 2021 at 12:45):

If you want to know what I was hoping the web would be good for when it grows up, you could look at the statement of interest I wrote for my 3rd return to grad school, this time in systems engineering, intending to pull together all the loose threads of my previous interweavings.

view this post on Zulip Jon Awbrey (Aug 01 2021 at 12:52):

I opened a new topic for discussing inquiry driven systems.

view this post on Zulip Henry Story (Aug 01 2021 at 13:38):

To get back to the topic of this thread, the third talk following the talk on "Graphical Regular Logic" I mentioned above, was on Temporal Landscapes: a graphical logic of behavior by @Alberto S that starts 1 hour and 5 minutes into the recording . It covers temporal type theory, but I am not sure the authors think of it as a modal logic though. Still it seems to be going in the direction of modality and pragmatics...
screenshot of talk on temporal behavior

view this post on Zulip Jon Awbrey (Aug 01 2021 at 14:36):

Henry Story said:

To get back to the topic of this thread, the third talk following the talk on "Graphical Regular Logic" I mentioned above, was on Temporal Landscapes: a graphical logic of behavior by Alberto S that starts 1 hour and 5 minutes into the recording . It covers temporal type theory, but I am not sure the authors think of it as a modal logic though. Still it seems to be going in the direction of modality and pragmatics...
screenshot of talk on temporal behavior

Got errands to run and weeds to weed the rest of today, so won't have time for a video, but applying logic and dynamic∫neuronic systems to each other is what led me to develop differential logic.

See also Differential Logic and Dynamic Systems

view this post on Zulip Jon Awbrey (Aug 01 2021 at 20:06):

Cf: Logical Graphs • Discussion 4

Henry Story said:

Knowledge Representation in Bicategories of Relations is also drawn up in terms of string diagrams, as a way of explaining the W3C RDF and OWL standards. So it looks like we have a nice route from Peirce to RDF via string diagrams. Or the other way around: whichever route one prefers to travel.

I opened a topic on Relation Theory to discuss the logic of relative terms and the mathematics of relations as they develop from Peirce’s first breakthroughs (1865–1870).  As I have mentioned on a number of occasions, there are radical innovations in this work, probing deeper strata of logic and mathematics than ever before mined and thus undermining the fundamental nominalism of First Order Logic as we know it.

view this post on Zulip Jon Awbrey (Aug 26 2021 at 18:02):

Cf: Animated Logical Graphs • 81

Re: R.J. Lipton and K.W. ReganA Negative Comment On Negations

Minsky and Papert’s Perceptrons was the work that nudged me over the line from gestalt psychology, psychophysics, relational biology, etc. and made me believe AI could fly.  I later found out a lot of people thought it had thrown cold water on the subject but that was not my sense of it.

The real reason Rosenblatt’s perceptrons short-shrift XOR and EQ among the sixteen boolean functions on two variables is the adoption of a particular role for neurons in the activity of the brain and a particular model of how neurons serve computation, namely, as threshold activation devices.  It is as if we tried to do mathematics using only the inequality \le instead of using equations.  Sure, we can express equations in roundabout ways but why tolerate the resulting inefficiency?  As a final observation, xyx \le y for boolean variables x,yx, y is equivalent to xyx \Rightarrow y so this fits right in with the weakness of implicational inference compared to equational inference rules.

But there are other models for the role neurons play in the activity of the brain and the work they do in computation.

view this post on Zulip Jon Awbrey (Aug 29 2021 at 16:12):

Cf: Logical Graphs • Discussion 3

Re: Peirce ListJohn Sowa

The Peirce List discussion on “thinking in diagrams vs thinking in words” called to mind the time I spent a hefty sum on a copy of Stjernfelt’s Diagrammatology which ran to over 500 pages with many sections in very small print and had just over 50 diagrams between the covers.

In the same way, the real Versus monopolizing our attention here is not so much the difference between “thinking in diagrams” and “thinking in words” as the difference between “thinking in words about thinking in diagrams” and “thinking in words about thinking in words”.

Those of us who have been developing “moving pictures” from the very get-go have learned to see things rather differently.

Figure 1.  Peirce Syllabus

Normative science rests largely on phenomenology and on mathematics;
metaphysics on phenomenology and on normative science.

❧ Charles Sanders Peirce • Collected Papers, CP 1.186 (1903)
Syllabus • Classification of Sciences (CP 1.180–202, G-1903-2b)