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: What are some uses of exponential objects?

Julius Hamilton (Jul 28 2024 at 21:35):

Once we have defined exponential objects, what can we do with them? For example, are there any interesting morphisms into or out of them that we can use to represent a particular concept? What about mappings between $B$ or $A$ and $B^A$?

Ryan Wisnesky (Jul 28 2024 at 23:22):

one answer to this question is that a cartesian closed category (such as the simply typed lambda calculus) allows higher order programming, whereas a cartesian category (such as equational logic) only allows first order programming. for many purposes this is not a meaningful distinction - but for many purposes it is meaningful. For a technical answer to your question, you can define exponentiation with an object X as adjoint to taking a product with X, and probe exponentiation that way.

Julius Hamilton (Jul 30 2024 at 13:52):

Thanks, these are all great answers!

John Baez (Jul 30 2024 at 13:57):

Another answer: there's

• a set of maps from a set to a set,
• a poset of order-preserving maps from a poset to a poset,
• a category of functors from a category to a category,
• a vector space of linear maps from a vector space to a vector space,
• a topological space of continuous maps from a topological space to a topological space,

etc., and we'd like to formalize this pattern:

there's a thing (of some sort) of maps from any thing (of that sort) to any other thing (of that sort)

Formalizing this pattern requires [[cartesian closed categories]] but also more general [[monoidal closed categories]].

John Baez (Jul 30 2024 at 13:59):

There are sometimes obstacles that can be gotten around (like with topological spaces), and often things just don't work like this: for example, there's not a monoid of monoid homomorphisms from a monoid to a monoid.

(I'm picking "monoid" because it's the simplest thing I can think of where this happens, but there are lots.)

Joe Moeller (Jul 30 2024 at 18:36):

In [[synthetic differential geometry]], the tangent bundle of a space X is an exponential object $X^D$ where D is the “infinitesimal space”. So a tangent vector in this context is literally an infinitesimal path in X.

Madeleine Birchfield (Jul 30 2024 at 18:49):

In homotopy theory, path space objects of an object $X$ are exponential objects $X^I$ where $I$ is the interval object.

Eric M Downes (Jul 31 2024 at 03:24):

I recall someone posed to you a problem of realizing $X^2$ as an exponential object in $\sf Set$ and exhibiting an isomorphism to $X\times X$… I highly recommend that exercise!

Exponential objects play a central role in Lawvere’s fixed point theorem that unifies Cantor’s Diagonal argument, the Halting Problem, and several other “no go” / impossibility theorems. Currying also makes an appearance.

That is a very abstract theorem but it doesn’t actually have a lot of stuff you need to know before hand. Jöst has a great treatment of it in his book Conceptual Mathematics that I studied until I understood it. It’s def worth the payoff, and the original theorem by Cantor is well worth studying in its own right!

$End_C(X)$ (morphisms in $\sf C$ from an object to itself) always exists and is a monoid. But that monoid is not always isomorphic to an object within $\sf C$. When it is we call it $X^X$.

$Aut_C(X)=End_C(X)\cap Iso_C(X,-)$ similarly exists and forms a group. (I’m assuming $\sf C$ is not enriched here by using $\cap$.) Similarly, this cannot always be realized as an object within $\sf C$.

To appreciate those statements, you might need to build up more intuition about monoids, though…. as always, the powerset $2^X$ is the basis for a lot of cool mathematics and you can practice a kind of “yoga of three operations” in $\sf Set$ by looking at direct images and preimages in addition to functions.

John Baez (Jul 31 2024 at 10:29):

Eric M Downes said:

$End_C(X)$ (morphisms in $\sf C$ from an object to itself) always exists and is a monoid. But that monoid is not always isomorphic to an object within $\sf C$. When it is we call it $X^X$.

One little correction:

$End_C(X)$ is a set, while $X^X$, when it exists, is an object of $C$, so it makes no sense to say they're isomorphic - except of course when $C$ is the category of sets.

There is a relation between the set of endomorphisms of $X$ and the object $X^X$, but it's subtler. For starters, elements of $End_C(X)$ correspond bijectively to morphisms $1 \to X^X$, if $C$ is a cartesian closed category.

Julius Hamilton (Jul 31 2024 at 16:52):

Eric M Downes said:

To appreciate those statements, you might need to build up more intuition about monoids, though….

Awesome, I will.

One idea I had for exploring interesting morphisms into or out of an exponential object would be a way for a morphism from $A$ to $B^A$, the exponential object, representing functions, to represent “function application”, like $f(A)$ for some $f$.

However, since $B^A$ represents all possible functions $A \to B$, I wonder if there could be a parametrized function, which changes depending on the elements of the domain set $A$? Then, for each map $A \to B^A$, you would have a different function being applied to the elements of $A$? I’m going to see if something similar to that could work, but this thought came about because I was considering a functor which instead of being defined on a fixed source category has a “corresponding behavior” for any category in a family of categories you pass to it…

Ryan Wisnesky (Jul 31 2024 at 17:29):

often parameterized functions are given type A*B->C where one of the A or B are thought of as parameters. or, in dependent type theory, you could write a function of type e.g., forall x : A, T(x) where T : A -> Type is a "type level function". Check out "Coq" for an example dependently typed programming environment

Eric M Downes (Jul 31 2024 at 18:04):

John Baez said:

$End_C(X)$ is a set,

Thank you! When you want to specify the monoid formed by the endomorphisms of an object $X$ in some category $\sf C$, and not just the set, would you call that $\mathbf{B}End_{\sf C}(X)$ the delooping of $End_C(X)$, or just $Hom_C(X,X)$ or something else?

while $X^X$, when it exists, is an object of $C$, so it makes no sense to say they're isomorphic - except of course when $C$ is the category of sets.

Thank you again. Let me correct my statement.

In $\sf C$ having all binary products and $\mathsf{C}_0\ni X,Y,Z,1$ with $1$ the initial object, the exponential object $X^Y$ satisfies the following universal property

So, for every $v,f$ as above there is an object $X^Y$ equipped with operation $\lambda-$ such that $f=v\circ(\lambda f\times id_Y)$. (Julius: Don't worry what the operation is until you can describe the universal property in your own terms, think of $\lambda f$ as just some unique function we get for every $f$, that makes the diagram commute. Then once you have a hypothesis about how this all works, try to implement it in python using the lambda function. Or any language, but you know python IIRC.)

You can interpret this in $\sf C=Set$ as $Z$ indexing the functions "stored" in $X^Y\cong\{g:Y\to X\}$. Like how monoid elements index the transformations of a set.

But if we stay in $\sf C$ and just set $Z=1$ we can now connect with John's statement.

There is a relation between the set of endomorphisms of $X$ and the object $X^X$, but it's subtler. For starters, elements of $End_C(X)$ correspond bijectively to morphisms $1 \to X^X$, if $C$ is a cartesian closed category.

John Baez (Jul 31 2024 at 18:13):

Eric M Downes said:

John Baez said:

$End_{\mathsf{C}}(X)$ is a set,

Thank you! When you want to specify the monoid formed by the endomorphisms of an object $X$ in some category $\sf C$, and not just the set, would you call that $\mathbf{B}End_{\sf C}(X)$ the delooping of $End_{\sf C}(X)$, or just $Hom_{\sf C}(X,X)$ or something else?

I'd still call it $End_{\mathsf{C}}(X)$. Above I said $End_{\mathsf{C}}(X)$ is a set, but I could equally well have said it's a monoid: mathematicians generally think "we're all smart enough to know a monoid has an underlying set, let's not sweat the difference when it doesn't matter". In some cases it does matter and we have to be careful, but there's no standard notation to distinguish the monoid from its underlying set: you just have to explain what you're talking about.

Here my point was that in contrast $X^X$ is not a set, nor for that matter a monoid: it's an object in $\sf C$, and in fact a monoid in $\sf C$. And you got my point, so all is well.

Chris Grossack (they/them) (Jul 31 2024 at 19:41):

Maybe this is a nice place to shamelessly plug an old blog post of mine about cartesian closed categories, internal groups, and enriched functors:
https://grossack.site/2024/02/18/internal-enriched-groupoids

We know that a group action $G \curvearrowright X$ is fruitfully thought of as a functor from $G \to \mathsf{Set}$ (viewing $G$ as a one-object category, and this functor sends the unique object to $X \in \mathsf{Set}$). The question, then, is what happens if you want a group in a category to act on an object in that category (for instance, a topological group acting on a topological space). It will come as no surprise that here the cartesian closed structure (read: the presence of exponential objects) is essential.

Todd Trimble (Jul 31 2024 at 21:41):

$Aut_C​(X)=End_C​(X) \cap Iso_C​(X,−)$ similarly exists and forms a group. (I’m assuming $C$ is not enriched here by using $\cap$.)

This last sentence looked a little strange to my eye, since from one point of view all categories are enriched in something, but perhaps more piquantly, it's not like "being enriched" is a property: enrichment is a structure.

(Also I don't see the symbol $\cap$ as precluding all that much. For example, taking intersections of subobjects is a commonplace.)

Just want to say (possibly overlapping Chris's blog post) that you can form internal automorphism groups $\mathrm{Aut}_C(X)$ in any finitely complete cartesian closed category $C$. More generally, you can form the object $\mathrm{Iso}(X, Y)$ by taking the equalizer of two maps of the form

$Y^X \times X^Y \rightrightarrows X^X \times Y^Y$.

One is the map whose components (valued in $X^X, Y^Y$) are the two different orders of internally composing, one diagrammatic and the other Leibnizian. The other map is

$Y^X \times X^Y \overset{!}{\longrightarrow} 1 \overset{(\lceil 1_X\rceil, \lceil 1_Y\rceil)}{\longrightarrow} X^X \times Y^Y$

What the equalizer $\mathrm{Iso}(X, Y) \hookrightarrow Y^X \times X^Y$ internally expresses is the object of pairs $(f: X \to Y, g: Y \to X)$ such that $f ; g = 1_X$ and $g ; f = 1_Y$.

(One should also check that the composition $\mathrm{Iso}(X, Y) \hookrightarrow Y^X \times X^Y \overset{\pi_1}{\to} Y^X$ is a monomorphism, internally expressing uniqueness of inverses. This isn't very hard, although it's a good intro exercise to internal reasoning.)

Eric M Downes (Jul 31 2024 at 22:11):

Thanks! That’s … very interesting.

I should perhaps have just said, “I’m assuming Aut(X) and Iso(X,-) are sets so that $\cap$ is clearly defined.” That’s clearer. I think someone as advanced as you Todd can find a way to make it work despite this restriction, but I was more afraid of Julius thinking $\cap$ was some other cool and interesting product than what I meant: automorphisms are the endos that are also iso.

And I admit I have not internalized the difference between structure and property, though I look forward to one day.

Eric M Downes (Jul 31 2024 at 23:05):

Actually @Todd Trimble have you considered editing or linking from [[automorphism]]? I'm finding this really fun to think about, and nearly the exact same syntax is used there. (No CCC of course, but maybe something can be said about a more general family of $\cap$, which I haven't a name for.)

John Baez (Aug 01 2024 at 07:13):

And I admit I have not internalized the difference between structure and property, though I look forward to one day.

You may have heard people say this already, but "properties" correspond to true or false questions, like "are you married?", while "structures" correspond to questions where there is a set of possible answers, like "who is your wife?"

John Baez (Aug 01 2024 at 07:14):

So when you said "I'm assuming $C$ is not enriched" it rubbed Todd a bit wrong, because the yes-or-no question "is $C$ enriched?" makes no sense: being enriched is not a property, it's a structure.

John Baez (Aug 01 2024 at 07:17):

He wasn't trying to make a federal case of it, and neither am I, though the length of this explanation makes it sound like I am. I just love the yoga of property, structure and stuff.

A simple example of someone screwing up the structure-property distinction would be someone who asked "is the set $\{1,2,3\}$ a group?" But the problem tends to arises because some adjectives in mathematics describe properties while others describe structures. For example "is this category cartesian?" makes sense, because cartesianness is a property of a category, but "is this category monoidal?" does not.

Graham Manuell (Aug 01 2024 at 08:01):

Chris Grossack (they/them) said:

It will come as no surprise that here the cartesian closed structure (read: the presence of exponential objects) is essential.

This is nitpicking, but I wouldn't say it's essential, since you can talk about internal group actions without exponentials. Indeed, topological spaces are an example where we don't have exponentials but still want to consider internal group actions. Exponentials do make things easier though, which was probably what you meant in the first place.

Julius Hamilton (Aug 01 2024 at 13:44):

John Baez said:

A simple example of someone screwing up the structure-property distinction would be someone who asked "is the set $\{1,2,3\}$ a group?" But the problem tends to arises because some adjectives in mathematics describe properties while others describe structures. For example "is this category cartesian?" makes sense, because cartesianness is a property of a category, but "is this category monoidal?" does not.

I’m curious to understand this better.

Let’s say we write a definition of a monoidal category in first-order logic, as a theory, $\Phi$.

I guess we would say that any monoidal category $M$ “satisfies” or “models” $\Phi$: $\Phi \models M$.

Couldn’t we interpret the question “Is category $M$ monoidal?” as, “Do the monoidal axioms, applied to $M$, evaluate to True?”

John Baez (Aug 01 2024 at 13:57):

It doesn't pay to get fancy and bring model theory into this conversation before you get the basic idea, which is pretty simple.

There's no way you can look at a set $S$ and tell whether it's a group or not, because a group is a set $S$ with extra structure: an operation $\cdot$ and an element $1$ obeying some equations. You can ask if the triple $(S,\cdot, 1)$ is a group or not. It makes no sense to ask if $S$ is a group or not.

Similarly, there's no way you can look at a category $M$ and tell whether it's monoidal or not, because a monoidal category is a category $M$ with some extra structure: a functor $\otimes$ and an object $I$ and some natural transformations $a, \ell, r$ obeying some equations. You can ask if the sextuple $(M, \otimes, I, a, \ell, r)$ is a monoidal category or not. It makes no sense to ask if $M$ is a monoidal category or not.

Suppose I show you a tire and and ask "is this car painted red?" I have to ask you "what car?"

John Baez (Aug 01 2024 at 13:59):

But there's a lot more to this: there's a whole yoga of properties, structure, stuff, 2-stuff, etc.

Julius Hamilton (Aug 01 2024 at 14:01):

Cool, well, for anyone interested, here appears to be a reference on these ideas - https://ncatlab.org/nlab/show/stuff,+structure,+property

Julius Hamilton (Aug 01 2024 at 14:32):

Eric M Downes said:

Exponential objects play a central role in Lawvere’s fixed point theorem that unifies Cantor’s Diagonal argument, the Halting Problem, and several other “no go” / impossibility theorems.

I stumbled upon someone’s exegesis of Lawvere’s fixed point theorem on YouTube last night - https://youtu.be/bNxjbt0Cn1c?si=dMaCd1cYO8BIvb5Q

The first part I want to check my comprehension of is the motivation for the definition of “weak point surjectivity”.

Maybe someone can give me a mathematical way of exploring this, like a little exercise or proof.

For example, maybe I should try to think through:

Let’s assume we want to “generalize” the properties of surjective functions to a property of diagrams. How should we discover the definitions for epimorphism, point surjectivity, and weak point surjectivity?

Julius Hamilton (Aug 01 2024 at 15:43):

This is one way of thinking about exponential, I think. It’s meant to supply an intuition rather than be rigorous.

When we say $Hom(A, C^B) \cong Hom(A \times B, C)$, since we “think of” $C^B$ as the set of functions $\{ f | f : B \to C \}$, we can think of it as $Hom(B, C)$, and so we can “think of” the first formula as $Hom(A, Hom(B, C)) \cong Hom(A \times B, C)$, which to me now almost sounds like an axiom similar to associative laws, distributive laws, or something.

It makes me think that if we could find a way to express $C$ as a Hom-set (I’m not sure if $Hom(C, C)$ would work - maybe $Hom(1, C)$?), we can continue manipulating such expressions by “moving things into their Hom-set form”, if we want - something like $Hom(A \times B, C) \cong Hom(A \times B, Hom(C, 1)) \cong Hom(A \times B \times C, 1)$. I don’t know if that’s true, but I’ll explore avenues like this.

Julius Hamilton (Aug 01 2024 at 15:48):

I realize the above can’t be correct, since $Hom(X, 1)$ is a singleton set - itself a terminal object - for any object $X$. And yet, I find that an interesting observation in its own right.

Maybe a clever trick using the dual?

$Hom(A, B) \cong Hom(B, A)$, I think?

No, that’s not it - more like $Hom_C(A, B) \cong Hom_{C^{op}}(A, B)$, I think.

I’m wondering if this way of rewriting exponentials can help motivate the definition of weak point surjectivity, though.

I think weak point surjectivity says that a morphism $f:A \times B \to C$ is weak point surjective if for any $x: X \to C$, there exist (unique?) maps $u_1: 1 \to X$ and $u_2: 1 \times 1 \to A \times B$, such that $\Delta_1 \circ u_2 \circ f = u_1 \circ x$? I’ll double-check. But I’m wondering if the fact that we see a product here means we can rewrite this as an exponential in an insightful way, maybe.

Julius Hamilton (Aug 01 2024 at 15:51):

(deleted)

Joe Moeller (Aug 01 2024 at 18:02):

John Baez said:

It doesn't pay to get fancy and bring model theory into this conversation before you get the basic idea, which is pretty simple.

There's no way you can look at a set $S$ and tell whether it's a group or not, because a group is a set $S$ with extra structure: an operation $\cdot$ and an element $1$ obeying some equations. You can ask if the triple $(S,\cdot, 1)$ is a group or not. It makes no sense to ask if $S$ is a group or not.

Similarly, there's no way you can look at a category $M$ and tell whether it's monoidal or not, because a monoidal category is a category $M$ with some extra structure: a functor $\otimes$ and an object $I$ and some natural transformations $a, \ell, r$ obeying some equations. You can ask if the sextuple $(M, \otimes, I, a, \ell, r)$ is a monoidal category or not. It makes no sense to ask if $M$ is a monoidal category or not.

Suppose I show you a tire and and ask "is this car painted red?" I have to ask you "what car?"

An example of this: is Set monoidal? I could find "yes", "no", and "depends" all as reasonable answers.

• Does Set admit a monoidal structure? Yes, namely the cartesian one, the cocartesian one, and a bunch of others.
• Is Set a monoidal category? No, Set is the underlying category of several monoidal categories. So if you said something to me like "for instance take the monoidal category Set", I might assume you meant cartesian, but I'd genuinely be obliged to ask which structure. The cocartesian structure is also important enough that you may be talking about it.
• Is Set a monoidal category without me having to specify a tensor etc? No, this is a type error.

Chris Grossack (they/them) (Aug 01 2024 at 19:08):

Graham Manuell said:

This is nitpicking, but I wouldn't say it's essential...

To nitpick the nitpick, I do think it's essential if you want a nice story of how group actions $G \curvearrowright X$ internal to $\mathcal{C}$ are related to functors $BG \to \mathcal{C}$ sending the point of $BG$ to $X$. But this probably falls into the category of

Exponentials do make things easier though, which was probably what you meant in the first place.

(and you're right that this is more what I was getting at)

Julius Hamilton (Aug 01 2024 at 19:26):

One thing I'm quite interested in, and which I think is connected to exponential objects, is something like the following.

Imagine that I want to model a real-world phenomenon with category theory.

For each "primitive type of thing" (something that will not be defined in terms of something else, for example, time, money, people, cars, etc.), I create an object which I will consider "the set of all such things".

Once I have my primitives, there are some very common semantic constructs we use in everyday life to reason about the world, which can be expressed within the formalisms of a diagram. For example, when I say, "A person", I feel like the indefinite article "a" actually implies a "universal set" defined by "unrestricted comprehension", if that can be allowed in some way (since it isn't normally, in set theory): The set of all elements x such that x is a person.

When I say "The person", a map from a terminal object into the object People conveys a specific person. And maybe, if I have some further maps from People to something else, there will be a commutative diagram using that map, so that the individual person pointed at corresponds to some individual associated thing in some other object, like the motorcycle they own, or something.

Now, what about collections of people? In set theory, I can take the power set of a set.

I actually have a lot more questions about this, but I can start with this simple one. I can try to "categorify" the idea of a power set, but how should I get there? I have been learning a little bit about how not all structures "categorify" well. Should I try to figure out what functional relationships a power set has to other sets, to decide what exact properties I would want on morphisms from a power set, to identify what a concise way to express "collections of things" would be, categorically?

Todd Trimble (Aug 01 2024 at 19:26):

The first part I want to check my comprehension of is the motivation for the definition of “weak point surjectivity”.

Maybe someone can give me a mathematical way of exploring this, like a little exercise or proof.

I would say the motivation is that it is a fairly minimal hypothesis that suffices to get the proof of the Lawvere fixed point theorem to work. "Weak point surjectivity" is not, I don't think, an especially important concept on its own.

Let's just look at the proof a moment, as played out in the category of sets. The statement is that if there is an endofunction $f: B \to B$ with no fixed point $b: 1 \to B$, then there can be no surjective map $A \to B^A$ for any set $A$. Or, to phrase it more positively: if there exists a surjective map $\phi: A \to B^A$, then every function $f: B \to B$ has a fixed point. The proof proceeds as follows:

1. Let $q: 1 \to B^A$ name the function $A \to B$ that sends an element $a \in A$ to $f(\phi(a)(a))$. Since $\phi$ is surjective, there is some $a_0 \in A$ such that $\phi(a_0) = q$, or in other words so that $\phi(a_0)(a) = q(a)$ for all elements $a: 1 \to A$.

2. Claim: $\phi(a_0)(a_0)$ is a fixed point of $f$. This is because
   $\phi(a_0)(a_0) = q(a_0) = f(\phi(a_0)(a_0))$
   according to how $q$ was defined, QED.

This simple proof can be abstracted and generalized so that it holds in categories much more general than the category of sets. So now suppose $f: B \to B$ is a map in a cartesian closed category, and $\phi: A \to B^A$ is any map. Then we may construct $q: 1 \to B^A$ so that it corresponds to the map $A \to B$ formed as the composite

$A \overset{\delta}{\to} A \times A \overset{\phi \times 1_A}{\longrightarrow} B^A \times A \overset{\mathrm{eval}_{A, B}}{\longrightarrow} B \overset{f}{\to} B.$

(This internalizes the series of maps $a \mapsto (a, a) \mapsto (\phi(a), a) \mapsto \phi(a)(a) \mapsto f(\phi(a)(a))$.)

Then, the remainder of the proof will also go through, if we assume of $\phi: A \to B^A$ that for every point $q: 1 \to B^A$ there is a point $a_0: 1 \to A$ such that $\phi(a_0)(a) = q(a)$ for all elements $a: 1 \to A$. This assumption or condition on $\phi$ is called "weak point surjectivity".

Todd Trimble (Aug 01 2024 at 19:41):

Should I try to figure out what functional relationships a power set has to other sets...?

In ordinary set theory, the power set $P(X)$ is naturally isomorphic to the exponential $\mathbf{2}^X$ where $\mathbf{2} = \{\bot, \top\}$ is the set of truth values. This exponential is the set of functions $f: X \to \mathbf{2}$. The natural isomorphism assigns to each subset $S \subseteq X$ the function $f_S: X \to \mathbf{2}$ defined by $f_S(x) = \top$ if $x \in S$, and $f_S(x) = \bot$ if $x \notin S$. In the inverse direction, to each $f: X \to \mathbf{2}$ we may associate a subset $S_f = \{x \in X|\; f(x) = \top\}$.

This leads naturally to the notion of truth-value object, aka [[subobject classifier]].

A useful fact is that maps $Y \to \mathbf{2}^X$ are in natural bijection with relations from $X$ to $Y$.

Julius Hamilton (Aug 02 2024 at 12:37):

Beautiful, man thank you so much for these detailed answers.

Julius Hamilton (Aug 06 2024 at 14:40):

I feel like I want today to be a “math day” (congratulations to those of you for whom every day is a “math day”).

But I feel like my mind has touched on a number of new frontiers lately, and I do want to take stock of some uncharted territory (for me), instead of working on some small, specific problems - both have their benefits.

I might try to get into words some of these big questions my mind has been orbiting around.

Julius Hamilton (Aug 06 2024 at 14:45):

I think one thing that can hopefully unify a lot of different things I think about is how, if we restrict ourselves to first-order logic, how seemingly all the different topics I encounter have an axiomatization in FOL (and I’m not currently worrying about theories which in fact do not; i.e., require a higher-order logic).

Julius Hamilton (Aug 06 2024 at 14:54):

And I’m very interested in simply enumerating theories. For me, it just feels like it has the potential to be thorough and comprehensive.

I think I maybe have been wanting to understand a general theory of “enumeration” (if it can be called that), for a while.

I mean a general technique for producing all formulae derivable from a set of formulae.

My original approach was to consider if for any collection of formulae, and I suppose how they interact with a deduction system, to study in general terms if there is always the ability to find a function which can consecutively generate all the formulae. That is a question I can imagine digging into today. The issue I think is often because some deduction rules are conditional, as I have mentioned earlier, and so some change in how the situation is presented is needed because we cannot apply a deduction rule to every formulae. I think this leads me towards ideas like category algebras, incidence algebras, partial algebras, which I would definitely want to study today.

I also found some alternative approaches online where you think about enumerating terms more as finding a bijective from natural numbers to terms; and what interested me is that sometimes these numbering functions are not as simple as one would hope. I can provide some examples of those as well.

I’ll try to present some specific thoughts on this next.

Julius Hamilton (Aug 06 2024 at 14:56):

I also want to read Kripke’s book about Wittgenstein and Rule-following today.

Julius Hamilton (Aug 06 2024 at 14:57):

Anyway:

One good small initial exercise is just like, enumerating all possible formulae in FOL. This would be the first step towards enumerating all possible theories (collections of formulae + formulae derivable from them).

Julius Hamilton (Aug 06 2024 at 15:00):

I sometimes have thought that if you can find a function to enumerate formulae, it has a strong connection to the set of formulae it determines; so that of course, you cannot practically enumerate an infinite set of formulae; but I expect there are ways in which you can use the function that would generate those formulae, as a representative of that set; this or that mathematical operation on that function would correspond to this or that operation on the set of formulae it generates. The idea is that finding a generating function is extremely useful not because we actually want to generate all the terms, but because it captures information in some “perfect” way; and we can compare the generating functions of different theories, to learn things about comparisons between the theories themselves. I expect this is possible in some limited extent.

Julius Hamilton (Aug 06 2024 at 15:03):

Now, I think that luckily this takes me back to my post/question about Boolean algebras. I think that a given signature uniquely determines a collection of atomic formulae; and a collection of atomic formulae uniquely determines the Boolean algebra from them. This is a good opportunity to go back and try to better understand what I’ve even learned about Boolean algebras.

Julius Hamilton (Aug 06 2024 at 15:11):

John Baez showed me (I believe) that to my surprise, a Boolean algebra on $n$ generators is actually a finite set. I did not expect this initially. And Todd Trimble is in the process of showing me (I think) that a Boolean algebra on $n$ generators is not “logically amorphous”, as I originally thought. I think that the elements of the algebra have an ordering - maybe a partial order - and maybe a Boolean algebra is, or is close to, a lattice of formulae. I want to understand what this ordering “means”. Since it was suggested that I show that $\bot \leq \top$, it feels like the formulae are maybe on a spectrum of “truth”.. I think Trimble used the worth “strength”. So far, my only idea is that a formula is “stronger” than another if, maybe, it contains “more truth” than another formula. Since these are composite formulae, made of arrangements of atomic formulae, I can imagine that a composite formulae is “stronger” if regardless of the truthhood or falsehood of its constituent atomic formulae, we can prove say, in more cases it evaluates to true than false, compared to some other composite formulae.

Julius Hamilton (Aug 06 2024 at 15:20):

But I want to know what this ordering “means”. Or, maybe it’s an interesting observation, but it actually doesn’t play a role in trying to enumerate theories from collections of formulae. Or maybe it does.

If we have an empty signature, the only atomic formulae are statements of equivalence.

This theory should be easy to enumerate, I think.

If we assume an infinite set of variable symbols, and since $\equiv$ is a binary relation symbol, I think that there might be various cool ways to look at “the number of choices”. For example, maybe you can go variable by variable, and ask yourself “how many statements of equivalence can I make using this formulae as the first argument”. Or, maybe you can instead start with the $\equiv$ symbol, and think “how many choices” you have for each argument. I expect the answer is $2^\omega$, but this is something I want to think through in a lot more careful detail.

On a side note, a question that I keep thinking about is, it seems very easy to enumerate something when there is only one operation to deal with. But in the case of a Boolean algebra, and other situations, we have multiple operations we can apply, and their interaction gets more complicated. It would be cool if we could always find a way to “separate” a free algebra with certain operations into a distinct algebraic structure for each operation in its own, and then show an algebraic relationship between each of those “isolated” algebras - like a way of “factorizing” any free algebra, I think.

Julius Hamilton (Aug 06 2024 at 15:24):

I’m actually just gonna stop there and let these fresh ideas simmer in my mind a bit, and come back later. I’ll be reading Kripke for the next few hours. Any suggestions or commentary on the above would be of great interest to me. Thank you very much.

Todd Trimble (Aug 06 2024 at 21:29):

So far, my only idea is that a formula is “stronger” than another if, maybe, it contains “more truth” than another formula. Since these are composite formulae, made of arrangements of atomic formulae, I can imagine that a composite formulae is “stronger” if regardless of the truthhood or falsehood of its constituent atomic formulae, we can prove say, in more cases it evaluates to true than false, compared to some other composite formulae.

Believe it or not, it's the other way around. If you say that someone is making too strong a claim, like "I am the best educated American", that means you think it's unlikely to be true. Conversely, a weaker statement like "I had an above average education for an American" is more likely to be true. Stronger statements imply relatively weaker statements. If I am the best educated American, then it would follow that I had an above average education for an American.

The weakest statements are the tautologies, the unconditional truisms, the things that go without saying, like "Today I am a day older than I was yesterday". The strongest statements are those which just can't be true, are unconditionally false, self-contradictory statements like "tomorrow it will rain, and tomorrow it will not rain".

A statement of type $p \wedge q$ is stronger than $p$, because for it to be true, both $p$ and $q$ have to be true. Thus $p \wedge q \leq p$. If you agree with that, then you have to agree with that in the case $q = \neg p$, where $p \wedge \neg p$ is unconditional falsity, is equivalent to $\bot$. Thus $\bot \leq p$ for any statement $p$.

(This segment of the discussion seems more appropriate to the Free Boolean Algebras thread.)

Ryan Wisnesky (Aug 07 2024 at 05:03):

btw, if anyone needs exponentials of copresheaves computed, we have java code to do it. Of course, this is intractable for all but the smallest inputs, but I thought a concrete example of "how all database mappings from X to Y on schema S" can be thought of as "a database on S" might be instructive.
Screenshot-2024-08-06-at-10.00.04PM.png

Julius Hamilton (Aug 19 2024 at 16:08):

Todd Trimble said:

Let's just look at the proof a moment, as played out in the category of sets.

The statement is that if there is an endofunction $f: B \to B$ with no fixed point $b: 1 \to B$, then there can be no surjective map $A \to B^A$ for any set $A$.

I’m going to respond to each thing you’ve written, restating it in my own words to process it and see if I follow along.

I’ll define a fixed point of an endofunction $f: B \to B$ as an element $b \in B$ s.t. $f(b) = b$.

In an identity mapping, every element is a fixed point.

There exist endofunctions which have no fixed points. For example, map every element $n$ of $\mathbb{N}$ to $n + 1$.

(I want to start identifying which of my statements I need to come back and prove so I wonder if I can refer to the previous statement as a lemma or a proposition: Lemma 1: the function $f : \mathbf{N} \to \mathbf{N}$ such that $f(n) = n + 1$ has no fixed points.)

(I wonder if I can define a fixed point for a function $f: A \to B$ as $x \in A, B$ s.t. $f(x) = x$.)

The statement is that if there is an endofunction $f: B \to B$ with no fixed point $b: 1 \to B$, then there can be no surjective map $A \to B^A$ for any set $A$.

Here, we are talking about set-theoretic constructs via morphisms, so we talk about a fixed point technically as a morphism $1 \to B$.

Then a fixed point is a map $1 \to B$ which still points at the same element even after $B$ has been “rearranged” by some endomorphism. This is equivalent to saying that for endomorphism $e$, and monomorphism $1_B : 1 \to B$, $e \circ 1_B = 1_B$.

This would indicate that a fixed point of a morphism is an “absorptive” element. In algebra, if for all $a$, $a \cdot 0 = 0$, then $0$ is “absorptive””. Conjecture 1: The fixed points of a morphism $f: B \to B$ are all monomorphisms $g : 1 \hookrightarrow B$ such that…”

(I will write conjectures instead of questions, and leave them blank if I need to think more about them.)

Julius Hamilton (Aug 19 2024 at 16:19):

The statement is that if there is an endofunction $f: B \to B$ with no fixed point $b: 1 \to B$, then there can be no surjective map $A \to B^A$ for any set $A$.

If there exists a single endofunction that does not have a fixed point, on a set $B$, then there is a relationship between functions into $B$, and the domain of those functions: the domain cannot map surjectively to its collection of functions into $B$. It sounds like this would be because to each $a \in A$, we can associate more than one function in $B^A$, so there are too many functions in $B^A$ for $A$ to “cover” them all.

To phrase it more positively: if there exists a surjective map $\phi: A \to B^A$, then every function $f: B \to B$ has a fixed point.

Julius Hamilton (Aug 19 2024 at 16:38):

The proof proceeds as follows:

1. Let $q: 1 \to B^A$ name the function $A \to B$ that sends an element $a \in A$ to $f(\phi(a)(a))$.

$\phi$ is the surjective map previously mentioned, $\phi : A \to B^A$. $f$ is any endofunction $B \to B$. So $\phi(a)$ returns a function $i: A \to B$. And $f(\phi(a)(a))$ is $f$ being applied to $\phi(a)(a)$, which respectively is $i(a) \in B$. So $f$ is acting on an element $b$, which is the result of selecting a function $A \to B$ and applying it to some $a \in A$. So $\phi(a)(a)$ means, “choose a function and apply it to an element as well”.

Example: (to be added).

Since $\phi$ is surjective, there is some $a_0 \in A$ such that $\phi(a_0) = q$, or in other words so that $\phi(a_0)(a) = q(a)$ for all elements $a: 1 \to A$.

2. Claim: $\phi(a_0)(a_0)$ is a fixed point of $f$.

We said that if there exists a single $\phi: A \to B^A$ which is surjective, then every function $f : B \to B$ has a fixed point. The fixed point is $\phi(a)(a)$ for $a \in A$. I’m not sure how this can be a fixed point for any function $f$.

This is because $\phi(a_0)(a_0) = q(a_0) = f(\phi(a_0)(a_0))$ according to how $q$ was defined.

I don’t follow why $q(a_0) = f(\phi(a_0)(a_0))$. Maybe this is saying that since $q(a_0)$ is in $B$, then $f(q(a_0))$ is also in $B$.

Julius Hamilton (Aug 19 2024 at 17:46):

Let $q: 1 \to B^A$ name the function $A \to B$ that sends an element $a \in A$ to $f(\phi(a)(a))$.

$q$ is a morphism which selects a function $f(\phi(x)(x))$, $x \in A$. $q$ is a function $A \to B$, and $\phi(x)(x)$ assigns elements of a set to functions on that set, and then evaluates them. For example, say that $A = \mathbb{N}$, and $\phi(n) = x^n$. Then we have $\phi(0)(0) = 1, \phi(1)(1) = 1, \phi(2)(2) = 4, \phi(3)(3) = 27$, etc.

$f$ is an endofunction, and $q$ is just that endofunction precomposed with $\phi$; for example, if $f(x) = x^2$, then $q(x) = (x^x)^2 = x^{2x}$.

Since $\phi$ is surjective…

If $\phi$ is surjective, then my above example doesn’t work. Let’s explore $A = \mathbb{Z}, B = \mathbb{N}$. I could use help understanding if there is a surjection from $\mathbb{Z}$ to $\mathbb{N}^{\mathbb{Z}}$ or not.

Lemma 2: There does not exist a surjection from $\mathbb{Z}$ to $\mathbb{N}^{\mathbb{Z}}$, because Lemma 3: there cannot be a surjection from a set to a set of larger cardinality, and Lemma 4: $\mathbb{N}^{\mathbb{Z}}$ is of greater cardinality than $\mathbb{Z}$, which is respectively because of Lemma 5: $|A|^{|B|} > |A|$ for $|A|, |B| > 1$.

Proof:

(I might appear to be getting off-track unfortunately, so maybe I should not go into this, but I was thinking it could help me understand the fixed-point theorem by coming up with an example of a surjection from a set $Y$ to a set $X^Y$.)

(Currently working on proof of the above.)

This makes me think the fixed-point theorem is very much related to cardinality.

Todd Trimble (Aug 20 2024 at 13:08):

This makes me think the fixed-point theorem is very much related to cardinality.

Yes. For example, Lawvere's fixed point theorem subsumes Cantor's theorem, which says that for any set $X$, the power set $2^X$ has greater cardinality than $X$. Because if $2^X$ has the same cardinality as $X$, then there exists a bijection $X \cong 2^X$, which in turn means that there exists a surjection $X \to 2^X$, which by Lawvere's theorem means that every endofunction $2 \to 2$ has a fixed point. But this is absurd, since the transposition on the set $2 = \{0, 1\}$ that swaps $0$ and $1$ obviously has no fixed point!

There is nothing particularly special about $2$ here. For any set $A$, as soon as you know how to construct an endofunction on $A$ that has no fixed point, the same reasoning shows that $A^B$ and $B$ must have different cardinalities, for any set $B$. This applies in particular to $A = \mathbb{N}$, because as you pointed out in Lemma 1, the successor endofunction on $\mathbb{N}$ has no fixed point.

So your lemma 5, for example, follows fairly readily from Lawvere's theorem if we prove that any set $A$ such that $|A| > 1$ has a fixed-point-free endofunction on it. One way of constructing such an endofunction starts off by well-ordering $A$, and then considers the function that takes all but the greatest element of $A$ (if there is one) to its successor (exercise: what is that?), and takes the greatest element (if there is one) back to the first element.

Part of my point is that you don't need to prove lemmas 2 through 5 "off to the side", away from Lawvere's theorem. They follow from Lawvere's theorem.

(I might appear to be getting off-track unfortunately, so maybe I should not go into this, but I was thinking it could help me understand the fixed-point theorem by coming up with an example of a surjection from a set $Y$ to a set $X^Y$.)

And indeed you can do this. In the first place, there is a set $X$ for which every endofunction has a fixed point. We've already narrowed down the possibilities pretty drastically: we know from above the cardinality of $X$ can't be too big. So this gives some idea where to look.

You were doing well so far, but I encourage you to press on reading through the proof of Lawvere's theorem. You seemed to break away temporarily from your reading, where you wrote

I could use help understanding if there is a surjection from $\mathbb{Z}$ to $\mathbb{N}^\mathbb{Z}$ or not.

I'm saying you already know in your gut that the answer is "not", and you will know this for certain once you've worked all the way through Lawvere's theorem, coupled with your Lemma 1, and understand how it answers this question.

There's a nice paper by Noson Yanofsky that elaborates on Lawvere's point, that diagonalization arguments in general all seem to boil down to some version of the simple argument that bears his name. (After all these years, I still find it a wonderful argument, even though I just called it "simple". Like the Yoneda lemma, it's both beautiful and simple! My favorite kind of proof.)

I'll also say that the ramifications of this simple argument extend well beyond applications to cardinality.

Julius Hamilton (Aug 20 2024 at 13:23):

Nice.
I was reading Yanofsky yesterday, and a point it made was that “objects without a fixed-point-free endomorphism” basically mean “degenerate objects”. Amongst sets, every set has what I think he calls a “free endomorphism” (no fixed points) except singleton sets.

Todd Trimble (Aug 20 2024 at 14:10):

Amongst sets, every set has what I think he calls a “free endomorphism” (no fixed points) except singleton sets.

Bingo! And this is the clue to answering one of the questions (or things you want to understand) that I quoted.

I don't remember Noson using the phrase "degenerate objects" in this situation. (Not saying he didn't; I'd have to look again at the paper.) There is some justice in the phrase if the objects are sets.

On the other hand, if the objects are for example sup-lattices, there is a famous result called the Knaster-Tarski theorem which says that every order-preserving endofunction on a sup-lattice has a fixed point! Thus, for the full subcategory of the category of all posets consisting of sup-lattices, every object would be "degenerate"!

(Tangentially, there is a Cantor-type theorem that says there is no surjective poset map of the form $P \to [P, \mathbf{2}]$ or of the form $P \to [P^{op}, \mathbf{2}]$, for any poset $P$ and taking $\mathbf{2}$ to be the poset $\{0 \leq 1\}$, and taking $[X, Y]$ to be the poset of order-preserving maps $X \to Y$. I once recorded a proof of these facts, here. This proof also has a "diagonalization flavor" to it, but it's not AFAICT a simple corollary of Lawvere's theorem. There may be more juice in seeing what's "really going on" here.)

Suraaj K S (Aug 27 2024 at 00:25):

Ryan Wisnesky said:

one answer to this question is that a cartesian closed category (such as the simply typed lambda calculus) allows higher order programming, whereas a cartesian category (such as equational logic) only allows first order programming. for many purposes this is not a meaningful distinction - but for many purposes it is meaningful. For a technical answer to your question, you can define exponentiation with an object X as adjoint to taking a product with X, and probe exponentiation that way.

I was wondering what categories are being referred to, when you say STLC is a CCC, and equational logic is a cartesian category? Are these categories of 'theories' of these logics, where a theory is a pair consisting of a signature and a set of equations? What are the morphisms then?

Ryan Wisnesky (Aug 27 2024 at 00:44):

To turn the STLC into a CCC, as shown in e.g. Awodeys textbook, you consider the objects to be types of the STLC and a morphism x to y to be a term of type y with a free variable of type x; the STLC equations such as beta and eta allow one to establish the required universal properties of products, exponentials, etc. To turn an equational theory in a CC you do the same thing, but since you don't have lambda anymore you end up with a cartesian category, i.e., one with all products. These are also called 'multi-sorted equational theories' and 'algebraic theories' in the literature. Anyway, you can form a category of theories (equational, Horn, etc), where the morphisms from theory A to theory B (on a possible different signature) are 'theory morphisms': mappings from one to signature to another that preserve provability: if F : A -> B is a theory morphism, then if p = q is provable in A, F(p)=F(q) should be provable in B. Typically theory morphisms are expressed as mappings from the symbols in A to symbols in B (or to open terms in "B". Think mapping "+" to "*" for example).

Suraaj K S (Aug 28 2024 at 12:46):

Ryan Wisnesky said:

To turn the STLC into a CCC, as shown in e.g. Awodeys textbook, you consider the objects to be types of the STLC and a morphism x to y to be a term of type y with a free variable of type x; the STLC equations such as beta and eta allow one to establish the required universal properties of products, exponentials, etc. To turn an equational theory in a CC you do the same thing, but since you don't have lambda anymore you end up with a cartesian category, i.e., one with all products. These are also called 'multi-sorted equational theories' and 'algebraic theories' in the literature. Anyway, you can form a category of theories (equational, Horn, etc), where the morphisms from theory A to theory B (on a possible different signature) are 'theory morphisms': mappings from one to signature to another that preserve provability: if F : A -> B is a theory morphism, then if p = q is provable in A, F(p)=F(q) should be provable in B. Typically theory morphisms are expressed as mappings from the symbols in A to symbols in B (or to open terms in "B". Think mapping "+" to "*" for example).

Is there a reason you use the STLC, but an equational theory? I would like to think that we should use 'an STLC theory' or something? I'm thinking of STLC as a "doctrine", where we can define a signature and some axioms to form a particular 'theory' of STLC...

Ryan Wisnesky (Aug 28 2024 at 14:48):

I wrote "the" STLC because I was thinking about turning that specific theory into the free CCC, but you can certainly turn a theory of STLC into a quotient of a CCC.