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: learning: questions

Topic: Suggestions on formulating a question about the presentat...


view this post on Zulip Julius Hamilton (May 12 2024 at 16:17):

This is a sort of free-form question that I consider a supplementary exercise to my ongoing study of logic. I’d appreciate anyone offering suggestions for how to fully formulate the question.

There are a few markup languages for representing mathematical graphs. For example, GraphML is one such language.

In general, a computer program is an ordered sequence of symbols. Since I am most familiar with set theory, I will try to specify this in set theory, specifically, ZFC; but I would love to see ways to formalize this in other formal systems.

The “symbols” of an alphabet or a language can be any (distinct) arbitrary elements in a model of ZFC. Then let’s define our alphabet AA as nothing other than “some arbitrary (finite) set”: AUA \in U, where UU is a universe we are working in. (UU can not be the set of all sets, as is well-known; so we have to choose a universe).

I am hung up on some confusion about how to specify “the set of all finite sequences in our universe”, but this would allow us to specify “the set of computer programs”, roughly.

Graphs may be defined as an ordered pair whose first element Nodes can be any set, and whose second element Edges is a set of pairs taking values in Nodes.

A graph markup language maps the data of a graph into a sequence of symbols. Some of those maps would be undesirable. For example, mapping any graph into the empty string “” would not be usable as a markup language. We want to be able to reconstruct the graph from the string.

I would like to study the class of maps from graphs to strings to discover unexpected encodings that could have interesting properties, so as to discover new possible graph markup languages.

view this post on Zulip John Baez (May 12 2024 at 16:27):

People often choose (abstract) 'symbols' to be elements of some fixed set SS. Then ordered nn-tuples of symbols are elements of SnS^n and finite strings of symbols are elements of the disjoint union

n=0Sn \bigsqcup_{n=0}^\infty S^n

if we allow the empty string; start at n=1n = 1 if you don't want to.

view this post on Zulip John Baez (May 12 2024 at 16:28):

It's not so common to take SS to be an entire 'universe'.

view this post on Zulip John Baez (May 12 2024 at 16:29):

I can't tell if you're used to working with constructs like products of sets, the nth power of a set SnS^n, or disjoint unions of sets; if not they're worth studying.

view this post on Zulip Julius Hamilton (May 12 2024 at 17:42):

Thanks!

I have some familiarity with those concepts, though more to learn.

I think I am hung up on an underlying topic.

The language of set theory only includes one relation symbol, ‘\in’.

I read that you can always express a first-order theory without function symbols; so let’s assume set functions like the union are going to be defined a posteriori in terms of \in. (AB:={xxAxB}A \cup B := \{x | x \in A \vee x \in B\})

All of the concepts that emerge in a set theory must have their “data encoded” in terms of \in.

We can encode the data of a function by specifying its elements. A set of values suffices to characterize a function.

A concept of “order” is also a desirable thing to encode.

I have often wondered if looking for a mathematical definition of a concept is an example of the “paradox of analysis”.

Let us consider that I will freely guess hypotheses for what the properties of “order” should be.

I could say, “an ‘order’ is at minimum a relation that is transitive”.

Or I could say, “No, an ‘order’ is at minimum a relation that is transitive and connected.”

Or I could say, “Actually no, an ‘order’ should be thought of as a relation that is at minimum anti-symmetric.”

I find it interesting that there is seemingly no systematic way to derive the properties of an “order”. In order to do so, we could imagine I at least know one strict criterion I would like an “order” to fulfill. Then it would make sense to say, “I want to find a collection of properties which guarantee that a set fulfills that criterion”.

Sometimes we are looking for a definition and a definiendum at the same time.

I have gotten the impression that definitions of things like ordinal numbers and ordered pairs (Von Neumann’s, Kuratowski’s) are ways of looking for how the desired properties of an ‘order’ would appear, in a system with only one relation, ‘\in’.

The Von Neumann ordinals are generated by a function which takes the union of a set with the set’s elements.

For the Von Neumann ordinals, the \in-relation is transitive and strongly connected, and acts as a strict total order.

I want a “complete” definition for “all possible computer programs” (I think), because I need to use that specification in proofs (proofs about the collection of all maps from the collection of all graphs to the collection of all strings).

You showed me that we can designate an arbitrary alphabet as any finite set SS.

You then gave me a formula for specifying the collection of all finite strings over that (arbitrary) alphabet.

With an explicit definition for “the set of all finite graphs SgS_g” and “the set of all finite strings SsS_s”, I think my desire is to see relationships between maps, in the set of all maps of the form f:SgSsf: S_g \to S_s.

For example, I can try to find out what various properties such maps ff can have. Before I think of more interesting properties, I can start with a basic one: “would be acceptable as a graph markup language”.

I would need to determine what formal property corresponds to the intuitive notion of, “the graph can be reconstructed when encoded under this mapping”. Maybe that’s just “is invertible”.

I personally think the point is to “categorify” the situation, but I need more justification about why that would make the situation better, and if there is a clear reason for some specific choice for what the arrows will be.

I’d appreciate if you could continue to give me feedback on my attempt to formulate this. Thanks.

view this post on Zulip David Egolf (May 12 2024 at 17:57):

If you're interested in maps f:SgSsf:S_g \to S_s from a set of graphs to a set of strings you might also be interested in functors from a category of graphs to some category of strings.

A nice thing about functors is that they "preserve relationship equations": if we know some graphs are related by certain equations involving graph homomorphisms, and we have some functor from our category of graphs to our category of strings, then the strings corresponding to those related graphs will also be related in an analogous way.

view this post on Zulip David Egolf (May 12 2024 at 18:01):

I suspect there are multiple interesting notions for a "category of graphs" and a "category of strings", depending on what one considers to be a 'graph' or 'string', and also depending on how one wishes to relate graphs to one another (and strings to one another).

But imagine we have some functor F:GraphStringF: \mathsf{Graph} \to \mathsf{String}, where Graph\mathsf{Graph} is some category of graphs and String\mathsf{String} is some category of strings. You mentioned being interested in being able to reconstruct a graph from an encoding (as a string, I think). We'd want then to avoid the situation where FF sends two non-isomorphic (essentially different) graphs to isomorphic (essentially the same) strings. That is, we don't want this to happen: a graph GG is not isomorphic to a graph GG', but the string F(G)F(G) is isomorphic to the string F(G)F(G'). So, we'd like FF to have this property: if F(G)F(G)F(G) \cong F(G'), then GGG \cong G'.

view this post on Zulip John Baez (May 12 2024 at 18:06):

I have trouble understanding what you're talking about, @Julius Hamilton, because you seem to be talking about many different things at once. So my previous response was just to this one sentence:

The “symbols” of an alphabet or a language can be any (distinct) arbitrary elements in a model of ZFC. Then let’s define our alphabet A as nothing other than “some arbitrary (finite) set”: A∈U, where U is a universe we are working in.

It sounded a bit "off" to me, since I've never seen anyone use an alphabet where the symbols are absolutely every element of some universe. That would be a funny alphabet where the empty set, and the set of real numbers, and the number π\pi, and the unit circle are all symbols. If you use so many things as symbols, you don't have much left for sentences - or more precisely, you'd have to escape the universe U to find things that aren't symbols. Everyone I've met feels content with a smaller, more manageable set of symbols (though some wild and crazy logicians use an infinite set).

view this post on Zulip John Baez (May 12 2024 at 18:10):

This is probably not so relevant to your main point, but since I didn't understand your main point I latched on to something I understood.

view this post on Zulip Julius Hamilton (May 12 2024 at 20:20):

It’s definitely relevant and appreciated, thanks. Let me think that over and respond when I feel I can bring more clarity to my ideas.