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: Godel's Second IT vs Category Theory

John Onstead (May 20 2024 at 14:27):

A few weeks ago I asked about the category Set in the context of the relation between axiomatic set theory and category theory. There, I learned about a connection between Godel's first incompleteness theorem and category theory in terms of models of theories. After reading up a bit and thinking more on the subject since then, I wanted to come back to this because I've come across a schema to "get around" the second incompleteness theorem. Obviously this is impossible, but I'm curious where the mistake in my reasoning lies. Here is the schema I have come up with:

1. Choose Von Neumann-Bernays-Godel (NBG) set theory as a basis. Use this to construct category theory.
2. Write NBG as a theory in first order logic, which we will call NBG
3. Construct the syntactic category Syn(NBG)
4. Syn(NBG) is an object in the category of syntactic categories for first order theories (which I believe is related in some way to the category of Heyting categories). Construct this category.
5. Analyze Hom(Syn(NBG), Set) within this category of syntactic categories. Is this hom category an empty category or a non-empty category? In other words, look at the directed graph structure of the category of syntactic categories- is there any edges connecting the vertex representing Syn(NBG) to the vertex representing Set?
6. Godel's completeness theorem states that if a first order theory like NBG is syntactically consistent, it will have a model. Thus, if NBG is syntactically consistent, then Hom(Syn(NBG), Set), the category of models of NBG in Set, cannot be empty.

We therefore seem to be able to prove whether or not NBG is consistent using category theory, which is itself based in NBG- therefore, we have used NBG to prove its own consistency or non-consistency. Of course this violates Godel's second incompleteness theorem, so please tell me in which step of reasoning outlined above that this famous theorem destroys the argument! I'm eager to see so I can better understand the interplay of categories and Godel!

John Baez (May 20 2024 at 14:45):

If you can prove whether or not NBG is consistent using category theory, please do so! I don't see you settling this question here.

Yes, the consistency of a theory can be reduced to the question of whether a some graph has an edge from some vertex to another. But that latter question cannot always be settled in your favorite theory, whether it be PA, ZFC or NBG.

Zoltan A. Kocsis (Z.A.K.) (May 20 2024 at 14:48):

Consider the language $(\in)$ of Neumann-Bernays-Gödel set theory.

What is a model of a theory $T$ in the language $(\in)$? It is a carrier set $W$ together with a distinguished subset $W_\in \subseteq W^2$ so that whenever $\varphi$ is some sentence in the language $(\in)$ such that $T \vdash \varphi$, the following holds: if we replace the quantifiers $\forall x$ and $\exists x$ in $\varphi$ with bounded quantifiers $\forall x \in W$ and $\exists x \in W$ and replace all atomic propositions $x \in y$ with $(x,y) \in W_{\in}$, we get a true statement of NBG set theory.

Gödel's completeness theorem asserts that a theory $T$ in language $(\in)$ is consistent precisely if it has a model.

Gödel's completeness theorem is provable in NBG set theory. We can take $T=\mathrm{NBG}$ itself and get that NBG is consistent precisely if it has a model.

NBG does not prove that NBG is consistent. NBG also does not prove that NBG has a model.

What about the entire universe $V$, equipped with the relation $\in$? Isn't that a model of NBG?! Absolutely not! The definition of model requires that the carrier set be a set, not a proper class. But $V$ is a proper class. If you try to prove a variant of completeness theorem for class-models in NBG, you'll see that there is no way to carry out this proof. That's the end of the story.

Zoltan A. Kocsis (Z.A.K.) (May 20 2024 at 14:52):

Bringing in category theory doesn't change anything: all you get here is a paraphrasis of the simple fact that NBG knows that "NBG is consistent precisely if NBG has a model". But that's not news, that's just the completeness theorem. You haven't shown "NBG is consistent", nor have you shown "NBG has a model".
(So in particular step 5, where you analyze Hom(Syn(NBG), Set), is vacuous: NBG won't be able to carry out such an analysis, because it doesn't know that NBG is consistent.)

Patrick Nicodemus (May 20 2024 at 14:57):

Yes, I think that there is some circularity implicit in steps 5 and 6. I think that what this argument shows is that
"NBG proves that if NBG is consistent, it has a model", which is definitely true! So, if NBG could prove that NBG is consistent, then it would prove that NBG has a model by Completeness, which by the soundness theorem would imply that NBG is consistent. But, as Zoltan said, I think the argument doesn't really get you anywhere because of this circularity. If NBG can prove NBG is consistent, then NBG can prove that there is a category-theoretic model; and then this would mean that NBG proves NBG is consistent; but that is what we originally assumed, so we have not made much progress.

Patrick Nicodemus (May 20 2024 at 14:58):

In particular, I guess you're assuming that the question you ask in 5 can be answered, and it likely can't (in NBG, at least; that is, NBG does not prove that there is an edge Syn(NBG) -> Set, and it does not prove that there is not an edge, either)

John Onstead (May 20 2024 at 18:11):

John Baez said:

Yes, the consistency of a theory can be reduced to the question of whether a some graph has an edge from some vertex to another. But that latter question cannot always be settled in your favorite theory, whether it be PA, ZFC or NBG.

Zoltan A. Kocsis (Z.A.K.) said:

Bringing in category theory doesn't change anything: all you get here is a paraphrasis of the simple fact that NBG knows that "NBG is consistent precisely if NBG has a model". But that's not news, that's just the completeness theorem. You haven't shown "NBG is consistent", nor have you shown "NBG has a model".
(So in particular step 5, where you analyze Hom(Syn(NBG), Set), is vacuous: NBG won't be able to carry out such an analysis, because it doesn't know that NBG is consistent.)

Patrick Nicodemus said:

In particular, I guess you're assuming that the question you ask in 5 can be answered, and it likely can't (in NBG, at least; that is, NBG does not prove that there is an edge Syn(NBG) -> Set, and it does not prove that there is not an edge, either)

Thanks for the help, it seems the step that is going wrong is Step 5. It seems that, for some reason, whether Hom(Syn(NBG), Set) is empty or not is not possible to figure out in NBG.
I can see how the argument might seem circular. I think it might be better to rephrase it as this syllogism: 1. If Hom(Syn(NBG), Set) is non-empty, NBG is consistent (Godel's completeness theorem). 2. Hom(Syn(NBG), Set) is non-empty. 3. Therefore, NBG is consistent. The problem then seems to be that step 2 is not provable within NBG.

John Baez (May 20 2024 at 18:16):

It seems that, for some reason, whether Hom(Syn(NBG), Set) is empty or not is not possible to figure out in NBG.

Of course the reason is Gödel's second incompleteness theorem. More precisely, if NBG is inconsistent you can use NBG to prove that NBG has a model in Set, and you can also use NBG to prove that NBG does not have a model in Set. But if it is consistent, you can neither use NBG to prove that NBG does have a model in Set (since that would violate Gödel's second incompleteness theorem) nor prove that it does not (since then it would be inconsistent).

John Onstead (May 20 2024 at 18:43):

I think I understand that this is not possible due to Godel's second incompleteness theorem. What I am still missing is why this is not possible. Let me explain:
It might seem that introducing category theory is just a way to change the language around a bit from the usual set theoretic discussion- it's just another way of saying the same thing. The reason why I wanted to ask this question, however, is because I wonder if you can actually use the tools of category theory to figure out the result, provided you are determined enough. This is why I brought directed graphs into the discussion in the first place- they are concrete entities that you can actually sit down, pull out a piece of paper, and draw on the paper. If you were determined enough and had all the time in the universe, this means you could theoretically sit down and start drawing dots and arrows and eventually (in the infinite future) draw out the entire category Set or Cat. Of course, most categories like Set or Cat are infinite so it isn't practical to consider drawing out the full directed graph structure, but practicality isn't relevant- what matters is that, in principle, you could draw out any category onto some really big piece of paper.
Due to this, Hom(Syn(NBG), Set) isn't some mystical structure that might or might not exist depending on your set theory. Instead, it's a real concrete directed graph that exists the moment you define Syn(NBG) and Set. So what, precisely and mechanistically, stops you from being able to just sit down and draw out its directed graph structure? Or better yet, what stops you from drawing out the entirety of the directed graph of Cat, finding Hom(Syn(NBG), Set) as dot in this directed graph, and seeing how many arrows you drew between the terminal category and it? So long as you have the graph of all of Cat, this is just a simple lookup operation, there shouldn't be any mystical force stopping you from then just counting arrows that you already drew on a (potentially very physical) piece of paper!

Evan Washington (May 20 2024 at 19:26):

I think I can help a little in correcting the misunderstanding. Consider the following analogy. Let $r$ be the number that is $1$ if the Riemann hypothesis is true and $0$ otherwise. Although $r$ very much is a number (just as the construction you indicate very much is a category/directed graph), saying true things about $r$ (like whether it equals $0$) requires much more work than that mere stipulation (like proving things about the Riemann hypothesis). Of course, if you had infinite time, you might even check whether or not each finite sequence of statements gives a proof of the Riemann hypothesis. After infinite time, you would know the value of $r$. Like counting edges in graphs, this is a purely combinatorial exercise. But these facts tell us basically nothing about the value of $r$.

Gödel's incompleteness theorem tells you that you cannot prove when such a combinatorial exercise will be complete for an arbitrary statement in your theory. And consistency of a theory is an example of a statement for which your theory cannot prove when that combinatorial exercise will complete. (To draw out that lookup analogy, for each lookup you have to wait and see whether or not you enter an infinite loop! It's a halting problem!)

John Baez (May 20 2024 at 19:49):

I'll repeat what Evan said in a slightly different way. If you had "all the time in the universe" - or more precisely, if you could do a calculation with a countable infinity of steps - you could go through all proofs in NBG, check to see if there's a proof of 0 = 1, and if not, then you'd know NBG is consistent (and therefore has a model). But this process cannot be turned into a proof in NBG, because proofs in this system can only have finitely many steps.

The method @John Onstead suggested, drawing the categories Syn(NBG) and Set "on a large sheet of paper" and seeing if you can find a suitable map from the former to the latter, would take a lot more than a countably infinite number of steps. After all, Set has a proper class of objects and morphisms. So, going through all possible maps from Syn(NBG) to Set and seeing which if any are valid models would take not just a countably infinite amount of time, but an amount of time larger than every cardinal!

This shows, by the way, the power of Goedel's completeness theorem: it reduces the proper-class-sized challenge of seeing whether NBG has a model to the countably-infinite-sized challenge of seeing whether there's a proof of 0 = 1 in NBG.

John Onstead (May 20 2024 at 21:22):

Thanks @Evan Washington and @John Baez I think I understand this a little better now. I like the connection with the halting problem. For instance currently there's computers calculating higher and higher nontrivial roots of the Riemann zeta function, but trying to prove that this program will eventually terminate in a zero not on the 1/2 line is equivalent to proving the Riemann hypothesis itself. Which means we have no way of knowing that this computer program will actually give a counterexample or not until it does, or until we prove some other way that it won't. We are finite beings so we don't always have the ability to do "exhaustive brute force" proofs, such as when infinite things need to be checked. So if we set some computer to check all functors between Syn(NBG) and Set, or to enumerate Cat's structure and look up Syn(NBG) inside it, we cannot prove "ahead of time" that these will terminate via NBG and we will just have to wait for infinite time to pass!
Though I'm still confused about the notion of "absolute truth" in these scenarios. It seems whether or not a set theory is consistent is a statement that has some "absolute truth" value regardless of the theory you are working in, because you can always systematically check all proofs and see if any imply 0 = 1 (or, in my case, look at the categories involved), even though this does take infinite time. It's just that within some set theories this truth is not "accessible". That is, within the context of some set theory, there's no way to either go through all its own proofs and check if it implies 0 = 1 (as this is an infinite process) or to construct a finite proof with equivalent "power", so while the truth is "out there" (and the categories exist), we can't use that theory to directly "access it" (analyze the properties of these categories). But this conflicts with how Godel's first incompleteness theorem implies that there is no absolute truth- that an undecidable statement in one axiomatic system can be both true and false in differing axiomatic systems. For instance, there's no "absolute truth" of the Continuum Hypothesis since in some set theories this is true, and in others it is false. So is it that some statements (such as consistency of a theory) do have absolute truth while others (such as the continuum hypothesis) do not, or is it possible to find two set theories that disagree on whether NBG, ZFC, etc. are consistent? And if the latter is the case, then what would systematically checking proofs over infinite time (or constructing up the relevant categories) actually end up doing?

Mike Shulman (May 20 2024 at 21:32):

Whether or not there is a notion of "absolute truth" is a question of philosophy. I think most mathematicians probably believe there is a notion of "absolute truth" about the natural numbers, but may be less confident about, say, the continuum hypothesis (although plenty of set theorists, at least, do seem to believe that there is an absolute truth about the continuum hypothesis too).

Mike Shulman (May 20 2024 at 21:35):

But having an absolute truth about something doesn't preclude having different theories that disagree about it! For instance, assuming ZFC is consistent, we know that CH is independent of it, which means that both ZFC+CH and ZFC+notCH are consistent. Similarly, assuming ZFC is consistent, we know by the second incompleteness theorem that Con(ZFC) (i.e. "ZFC is consistent") is independent of it, which means that both ZFC+Con(ZFC) and ZFC+not-Con(ZFC) are consistent. In the latter case ZFC+not-Con(ZFC) is a nontrivial and consistent theory even though it includes the "false" fact not-Con(ZFC), because the falsity of this fact cannot be proven by the rest of the theory.

John Baez (May 20 2024 at 21:55):

@John Onstead wrote:

For instance currently there's computers calculating higher and higher nontrivial roots of the Riemann zeta function, but trying to prove that this program will eventually terminate in a zero not on the 1/2 line is equivalent to proving the Riemann hypothesis itself.

By the way, this is a tricky example because it not at all obvious that a computer can compute a zero of the Riemann zeta function with enough accuracy - infinite accuracy! - to show definitively that it lies on the line $\mathrm{Re}(z) = 1/2$. Say the program starts printing out more and more decimials:

$z = 0.49999999... + i 0.324810180188....$

When do you decide this zero is on the line $\mathrm{Re}(z) = 1/2$?

John Baez (May 20 2024 at 21:58):

For Goldbach's conjecture, it's fairly easy to write a computer program that looks for counterexamples and tells us when it finds one: an even number $\ge 4$ that's not the sum of two primes.

Mike Shulman (May 20 2024 at 22:00):

But if you're looking for counterexamples, you don't need to ever decide that the zero is on the line $\mathrm{Re}(z) = \frac12$, you only need to know how to decide that it isn't.

Mike Shulman (May 20 2024 at 22:02):

I don't know whether it's possible to write a program that enumerates all the zeros of the zeta function, but if you could do that, where to "give a zero" means that you have a program that will calculate it to any desired accuracy, then it seems to me you should be able to diagonally enumerate all of the zeros, each with greater and greater accuracy, and be guaranteed that if there is a zero that's not on the critical line you'll eventually discover that since you'll eventually compute that zero to sufficient accuracy to be able to tell that it's not on the line.

John Baez (May 20 2024 at 22:08):

Right. I was trying to explain some facts about where the Riemann Hypothesis and Goldbach's conjecture fit into the lightface hierarchy, but I was probably not doing a very good job. For Goldbach's conjecture you can write a program that recognizes whether an individual even number is an example or a counterexample, and thus a program that eventually reports the existence of a counterexample if there is one.

For the Riemann Hypothesis I believe you can write a program that enumerates the nontrivial zeros. Once you've found a zero (that is, proved that there's a single one inside some disc), you can write a program that recognizes whether it's a counterexample, but it's not so obvious you can write one that recognizes whether it's an example.

So, if my belief above is correct, you can again write a program that eventually reports the existence of a counterexample if there is one.

John Baez (May 20 2024 at 22:14):

@John Onstead wrote:

Though I'm still confused about the notion of "absolute truth" in these scenarios. It seems whether or not a set theory is consistent is a statement that has some "absolute truth" value regardless of the theory you are working in, because you can always systematically check all proofs and see if any imply 0 = 1 (or, in my case, look at the categories involved), even though this does take infinite time. It's just that within some set theories this truth is not "accessible". That is, within the context of some set theory, there's no way to either go through all its own proofs and check if it implies 0 = 1 (as this is an infinite process) or to construct a finite proof with equivalent "power", so while the truth is "out there" (and the categories exist), we can't use that theory to directly "access it" (analyze the properties of these categories). But this conflicts with how Godel's first incompleteness theorem implies that there is no absolute truth- that an undecidable statement in one axiomatic system can be both true and false in differing axiomatic systems.

I think bringing in the somewhat ill-defined concept of "absolute truth" only muddles these discussions, and it looks like you're giving a good example of how it does.

John Baez (May 20 2024 at 22:16):

You're saying a lot of reasonable stuff here. Everything reasonable about what you're saying can be said without phrases like "absolute truth" and "out there". If you drop those phrases, I claim the paradox you're pointing at will turn into something that's non-paradoxical - but very interesting.

John Baez (May 20 2024 at 22:20):

Start by stating Godel's first incompletness theorem in a more precise way: if a sufficiently powerful axiom system in first-order logic is finitely axiomatizable and consistent, there are sentences $P$ in this theory that are neither provable nor provable. If we add either $P$ or $\neg P$ to the axiom system, we get a new axiom system with all the same properties: it's still "sufficiently powerful", finitely axiomatizable and consistent.

John Baez (May 20 2024 at 22:20):

(We can flesh out the details of what "sufficiently powerful" means, but this includes our friends PA, ZFC, NBG, ETCS, etc.)

John Baez (May 20 2024 at 22:21):

Note that we don't need to talk about "absolute truth" here.

John Baez (May 20 2024 at 22:24):

So, I think the essence of what you're noticing is this well-known but fascinating fact. Suppose a sufficiently powerful axiom system $T$ in first-order logic is finitely axiomatizable and consistent. By Godel's second incompleteness theorem, $T$ cannot prove $\mathrm{Con}(T)$. So by the first incompleteness theorem, we can add $\neg \mathrm{Con}(T)$ to the axioms in $T$ and get a new consistent theory $T + \neg \mathrm{Con}(T)$.

John Baez (May 20 2024 at 22:24):

So, there are models of $T + \neg \mathrm{Con}(T)$.

What's concerning you, I think, is that $T + \neg \mathrm{Con}(T)$ proves there exists a natural number $n$ such that if we enumerate proofs in $T$, the nth proof is a proof of $0 = 1$. This seems to contradict our assumption that $T$ is consistent!

John Baez (May 20 2024 at 22:32):

It's not actually a contradiction, because you can't get from this theorem in $T + \neg \mathrm{Con}(T)$ to a proof of $0 = 1$ in $T$.

In other words, even though $T + \neg \mathrm{Con}(T)$ proves a sentence of the form

$\exists n (n$ is the number of a proof that $T$ is inconsistent)

the number $n = 0$ is not a number with this property, nor is the number $n = 1$, nor is the number $n = 2$, and so on.

John Baez (May 20 2024 at 22:36):

We thus say the theory $T$ is "omega-inconsistent". For the definition of this term, and a bit more analysis of the puzzle I'm talking about now, try :

• Wikipedia, omega-consistent theory.

John Baez (May 20 2024 at 22:47):

One way to understand this more deeply invokes "nonstandard numbers", but I'm getting tired so I'll stop here.

Mike Shulman (May 20 2024 at 22:50):

I think it's really hard to avoid referring to a notion of "absolute truth" at least about the natural numbers, or equivalently to the existence of some "standard" set of natural numbers independent of your model. In particular, the notion of omega-(in)consistency only makes sense with reference to a notion of "standard" natural number.

John Baez (May 20 2024 at 22:53):

I would not bring in "absolute truth", which is sort of like the "in case of emergency break glass" of mathematical logic. I would prefer to start doing my metamathematics inside some formal system (or if I'm feeling informal, some informal system) where I can reason about natural numbers, yet not claim that the theorems in this metasystem are examples of the "absolute truth".

John Baez (May 20 2024 at 22:55):

In particular, I've learned that some reasonable logicians don't treat a "standard model" of arithmetic as the "absolutely true" model of arithmetic. Rather, it has a more technical meaning without making such metaphysical claims. And that's how I use the term.

John Baez (May 20 2024 at 23:07):

Let me be more precise and then go to bed. Suppose I'm using ZFC to prove theorems about models of PA. Then I can prove there exist initial models of PA, which are of course all uniquely isomorphic, and I can call any of these "the standard model" of PA. Other models of PA will contain the natural numbers in the standard model but also others, which are "nonstandard numbers". We can then go ahead and prove a lot of things, like: for any nonstandard number there is a small nonstandard number.

Mike Shulman (May 20 2024 at 23:09):

Ok, that's fair. I prefer to avoid absolute truth myself. I just wanted to point out that the notion of omega-consistency depends on what the meta-natural-numbers are.

John Baez (May 20 2024 at 23:10):

Yes!

John Onstead (May 21 2024 at 01:05):

Thanks @Mike Shulman and @John Baez this really helped to clarify everything. The use of non-standard natural numbers in omega-consistency is very interesting, I'll have to look more into that. But from what I saw so far, their existence and use here seems to answer that question of mine about enumeration of proofs in a pretty creative way!
While my questions here have been answered, I was wondering tangentially about what it means that a "standard model" of PA is an "initial model" of PA. Does this have any relation/connection at all to the fact that the natural numbers object (NNO) such as the one in Set is an initial algebra for some endofunctor, as well as being the initial object in a category of similar "dynamical system"-like objects within Set?

John Baez (May 21 2024 at 05:26):

I'm a bit fuzzy on the relation between a NNO and the Peano axioms, but in response to a question by @David Michael Roberts, Andrej Bauer wrote:

J. Lambek and P. J. Scott: Introduction to higher-order categorical logic, Cambridge University Press, 1986, Part II, Section 4, Theorem 4.1 shows that a nno satisfies the first-order Peano rules (which are listed on page 135 under 3.7, 3.8., 3.9), while Part II, Section 12, Proposition 12.4 shows that Peano rules give a nno for the syntactic topos. By the universal property of the syntactic topos it then follows that in any topos which validates Peano rules has a nno.

John Baez (May 21 2024 at 05:33):

What does it mean for a topos to "validate Peano rules"? It's a topos with an object $\mathbb{N}$ and morphisms $S: \mathbb{N} \to \mathbb{N}$, $+ : \mathbb{N} \times \mathbb{N}$ etc. which validate the Peano axioms as formulated in the internal language of the topos? (This is a property not just of the topos but of all this extra structure.)

I'm left wondering how nonstandard models of Peano arithmetic - or more precisely, the existence of multiple nonisomorphic models of Peano arithmetic in Set - fits into this picture. If my understanding of Bauer's comment in the previous paragraph is correct, each such model of Peano arithmetic in Set gives a NNO. But all NNOs are isomorphic, by their initiality. So are nonisomorphic models of Peano arithmetic in Set giving isomorphic NNOs?

John Baez (May 21 2024 at 05:49):

I understand initial models of PA better than all this stuff. Just to make myself comfortable let's assume ZFC is consistent. In ZFC we can prove there exists an initial model of PA, say $\mathbb{N}_{init}$. This means that if $\mathbb{N}$ is some other model of PA we can prove there's a unique map of models

$i : \mathbb{N}_{init} \to \mathbb{N}.$

Thus $i(0) = 0$, $i(Sx) = S(i(x))$ where $S$ is the succcessor function in our models, $S(x+y) = S(x) + S(y)$, etc.

In ZFC one can then prove that $i$ is one-to-one and the image of $i$ is a model of PA which is an initial segment of $\mathbb{N}$: if $x \in \mathbb{N}$ is in the image, anything less than $x$ is also in the image.

We call the elements of $\mathbb{N}$ lying in the image of $i$ the standard elements $\mathbb{N}$, while the rest are nonstandard.

John Baez (May 21 2024 at 05:53):

Then if $\mathbb{N}$ is a model of $\mathrm{PA} + \neg\mathrm{Con}(\mathrm{PA})$, then it contains the Godel number of a proof of $0 = 1$, but this number is nonstandard!

Zoltan A. Kocsis (Z.A.K.) (May 21 2024 at 06:12):

@John Baez writes:

I'm left wondering how nonstandard models of Peano arithmetic - or more precisely, the existence of multiple nonisomorphic models of Peano arithmetic in Set - fits into this picture. If my understanding of Bauer's comment in the previous paragraph is correct, each such model of Peano arithmetic in Set gives a NNO.

Take a nonstandard model of the first-order Peano axioms in Set (i.e. an object $N$ equipped with maps $z':1\rightarrow N, s':N \rightarrow N, +:N^2\rightarrow N, \cdot:N^2\rightarrow N$ etc. so that certain conditions hold) whose carrier set is $N$ is outright uncountable.

You could trim this down to a diagram of the right shape $1 \rightarrow_{z'} N \rightarrow_{s'} N$ to give an NNO candidate, but this can't be isomorphic to the genuine NNO $1 \rightarrow_z \mathbb{N} \rightarrow_s \mathbb{N}$ since the existence of a suitable isomorphism would induce an isomorphism between $N$ and $\mathbb{N}$ as sets. But $N$ is uncountable, and therefore this cannot happen.

The diagram $1 \rightarrow_{z'} N \rightarrow_{s'} N$ is not going to be an NNO because it'll fail the initiality requirement (just take the actual NNO as the other diagram).

Zoltan A. Kocsis (Z.A.K.) (May 21 2024 at 06:17):

The initiality requirement for NNOs is largely analogous to satisfying the actual second-order induction axiom for all subsets: and indeed, the second order Peano axioms are categorical, having just one model up to isomorphism (and indeed unique isomorphism).

John Baez (May 21 2024 at 06:22):

Thanks, @Zoltan A. Kocsis (Z.A.K.)! That sounds convincing. So what's going on when Andrej Bauer writes

J. Lambek and P. J. Scott: Introduction to higher-order categorical logic, Cambridge University Press, 1986, Part II, Section 4, Theorem 4.1 shows that a nno satisfies the first-order Peano rules (which are listed on page 135 under 3.7, 3.8., 3.9), while Part II, Section 12, Proposition 12.4 shows that Peano rules give a nno for the syntactic topos. By the universal property of the syntactic topos it then follows that in any topos which validates Peano rules has a nno.

I assumed that when he wrote "Peano rules give a nno for the syntactic topos" he was still talking about the first-order Peano rules. I thought he was saying any model of the first-order PA axioms in a topos gives a NNO in a topos. But now that seems to be leading to a contradiction. So I guess he was talking about some higher-order Peano rules! I'll have to crack open Lambek and Scott.

Zoltan A. Kocsis (Z.A.K.) (May 21 2024 at 06:30):

lambek-scott-peano.png
Peano's rules as stated in Lambek-Scott are attached.
The third one is an induction axiom quantifying over all subsets (elements of the object $PN$). After a cursory skim it looks like the section of Theorem 4.1. is about proving that these rules hold in any topos.

John Baez (May 21 2024 at 06:48):

Okay, thanks! I'd call these axioms "2nd-order Peano arithmetic", though these are closer to Peano's original axioms than the first-order system we call PA.

So yes, Bauer is talking about this 2nd-order version of Peano arithmetic when he says "Peano rules give a nno for the syntactic topos".

Now there's no contradiction: nonstandard models of the first-order theory called PA in the category Set as described by ZFC don't give NNOs - and they also don't give models of the 2nd-order version of Peano arithmetic.

David Michael Roberts (May 21 2024 at 07:59):

Yes, I learned a long time ago that NNOs are really models for second-order Peano arithmetic, whereas when logicians usually talk about PA they really mean first-order PA. The former is 'categorical' in the sense that there is only one model up to isomorphism (though this assumes a background fixed set theory of course; varying this means you get different NNOs in different models of set theory), but the latter has non-standard models as we well know.

John Baez (May 21 2024 at 09:07):

I just commented on MathOverflow to remind everyone that "PA" means and should always mean the first-order formulation of Peano arithmetic, while "Peano Arithmetic" is a more flexible term, and Peano's original axioms were second-order.

Morgan Rogers (he/him) (May 21 2024 at 09:10):

I remember @Paul Blain Levy stopped posting in this Zulip years ago after debating with @Mike Shulman and others about what should be considered standard natural numbers :melting_face: do you think our collective understanding of natural numbers has improved since then?

John Onstead (May 21 2024 at 09:11):

This is interesting, that there's two takes on Peano Axioms, the first and second order versions. NNOs are models of second order Peano, meaning that a model of second order Peano in Set (for some set theory) selects the data of an NNO in that category. But then what is the categorical interpretation of a model of first order PA in Set? For instance, this wikipedia section gives something of a connection. A NNO is a special case of a "unary pointed system" internal to some category, which is a form of a dynamical system and also I believe what Zoltan above called a "candidate NNO" that might lack the property of initiality. Would a model of first order PA select some unary pointed system in the category then- so that finding some unary pointed system without initiality internal to Set is the same as finding some nonstandard system? That is, is the category of models of first order PA in Set equivalent to the category of unary pointed systems internal to Set?
The wikipedia article goes on to say that given the category of unary pointed systems internal to Set, the NNO in Set is the initial object. If these two categories are equivalent, it also then implies that the NNO is the initial model of PA, and maybe in a sense is a "minimal model" of first order PA. I know a similar concept of a "minimal model" might exist for ZFC- in general, maybe a "minimal model" is really just the initial object in the category of models?

John Baez (May 21 2024 at 09:14):

Morgan Rogers (he/him) said:

I remember Paul Blain Levy stopped posting in this Zulip years ago after debating with Mike Shulman and others about what should be considered standard natural numbers :melting_face: do you think our collective understanding of natural numbers has improved since then?

I don't remember that fight, so it's hard for me to say. I spent a lot of time discussing nonstandard models of PA with Michael Weiss around 2019, so my post-2019 understanding of those is better than my pre-2019 understanding, though I must admit it's going down again.

John Baez (May 21 2024 at 09:31):

John Onstead said:

But then what is the categorical interpretation of a model of first order PA in Set?

For me "PA" = "first order PA"; otherwise I talk about "Peano arithmetic". This is pretty standard among classical logicians.

This is a good question: how should a category theorist think about a model of PA in Set (or for that matter, some other topos)?

But the answer is probably a bit complicated since PA involves a rather complicated infinite set of axioms, including an induction axiom for each first-order formula with one free variable in the language of PA. In other words, it has an axiom schema for induction.

Would a model of first order PA select some unary pointed system in the category

Yes, I think is just a way of saying that any model of PA (= "first order PA") gives a set with a chosen element ("zero") and an chosen endofunction ("successor").

That is, is the category of models of first order PA in Set equivalent to the category of unary pointed systems internal to Set?

No. It's not true that any set with a chosen element and a chosen endofunction gives a model of PA. For example take the 1-element set equipped with its only possible element and only possible endofunction: that's not a model of PA! Or take the disjoint union of any model of PA and any set equipped with any endofunction!

Basically what you're calling a unary pointed system is a model of "brutally stripped-down PA" where we throw out the operations $+$ and $\times$, throw ALL THE AXIOMS, and only keep the constant symbol $0$ and the function symbol $S$ (successor).

So, a unary pointed system is a pathetically weak imitation of the natural numbers, and only initiality makes it become a model of PA (and much more).

John Onstead (May 21 2024 at 09:48):

John Baez said:

Basically what you're calling a unary pointed system is a model of "brutally stripped-down PA" where we throw out the operations + and ×, throw ALL THE AXIOMS, and only keep the constant symbol 0 and the function symbol S (successor).

So, a unary pointed system is a pathetically weak imitation of the natural numbers, and only initiality makes it become a model of PA (and much more).

Ah ok, this makes sense. So there might not be an equivalence but maybe there's some form of forgetful functor at least from the category of models of PA to this unary pointed system category, that does all the throwing out you are talking about!
Based on what is mentioned, it seems that a model of PA in Set has a form of a semiring structure, since you have both addition and multiplication (but not necessarily subtraction). It might then have some additional structure even beyond that since you might have a poset structure to give the ordering of the numbers, and of course a dynamical system structure to give the successor function. I'm not sure how to "make" the successor function structure work with the addition binary operation structure such that addition is the same as repeated succession (I haven't started reading anything about the relation between recursion theory and abstract algebra), but I'm sure this can be done.

John Baez (May 21 2024 at 09:59):

Right, the successor function $S$ needs to 'get along' with $+$ and $\times$, and PA provides the axioms saying exactly how it should. So we can define a Lawvere theory whose algebras are things with $0, S, +, \times$ obeying exactly those axioms. And this is some sort of watered-down version of PA.

But then comes an axiom that you can't describe using a Lawvere theory:

$Sx = Sy \implies x=y$

However, the hard part of PA is not any of this: it's the axiom schema for induction.

John Baez (May 21 2024 at 10:05):

By the way, if we mimic PA but leave out $\times$, we get Presburger arithmetic, and this is very interesting because unlike PA it's decidable. That is, we can write a program to decide whether or not any sentence is a theorem in Presburger arithmetic. But this program will be very slow: asymptotically it takes at least doubly exponential time. That means that Presburger arithmetic is quite complex, but not powerful enough to be Turing-complete.

John Onstead (May 21 2024 at 10:23):

John Baez said:

But then comes an axiom that you can't describe using a Lawvere theory:

Sx=Sy⟹x=y

However, the hard part of PA is not any of this: it's the axiom schema for induction.

So it seems that while an "arithmetic structure" like PA has some underlying algebraic structure, it's got extra non-algebraic "stuff" on top. This leads to an interesting observation: while arithmetic is taught before algebra and is usually considered "more elementary" than algebra, in a sense it is actually the opposite given "arithmetic structures" like PA, Presburger, etc. are much more "logically rich" than algebraic structures like groups, rings, etc.!

John Baez said:

By the way, if we mimic PA but leave out ×, we get Presburger arithmetic, and this is very interesting because unlike PA it's decidable. That is, we can write a program to decide whether or not any sentence is a theorem in Presburger arithmetic. But this program will be very slow: asymptotically it takes at least doubly exponential time. That means that Presburger arithmetic is quite complex, but not powerful enough to be Turing-complete.

That's cool! I suppose it "doesn't encode enough arithmetic" for Godel to apply. Which really makes me wonder what the "minimal theory" of arithmetic is such that Godel's incompleteness theorem starts applying. It seems to be "Robinson arithmetic" Q, which is interesting since this lacks induction- meaning induction isn't necessarily the thing that makes Peano incomplete! I guess this also explains how Presburger can be complete even with induction still in there.

John Baez (May 21 2024 at 10:44):

This leads to an interesting observation: while arithmetic is taught before algebra and is usually considered "more elementary" than algebra, in a sense it is actually the opposite given "arithmetic structures" like PA, Presburger, etc. are much more "logically rich" than algebraic structures like groups, rings, etc.!

Indeed! Of course the arithmetic we teach kids in first grade doesn't include mathematical induction.

John Baez (May 21 2024 at 10:49):

Which really makes me wonder what the "minimal theory" of arithmetic is such that Godel's incompleteness theorem starts applying. It seems to be "Robinson arithmetic" Q, which is interesting since this lacks induction- meaning induction isn't necessarily the thing that makes Peano incomplete! I guess this also explains how Presburger can be complete even with induction still in there.

Right, induction is not the key. Perhaps the key is the ability to describe all general recursive functions - this is called Turing completeness, and the basic idea is that your system is powerful enough to do anything you can do in any programming language. This is what I was calling "sufficiently powerful" earlier.

Actually I don't know if this is really the "key" to incompleteness. But it's true that any consistent finitely axiomatizable theory in first order logic that's Turing complete will contain sentences $P$ such that neither $P$ nor $\neg P$ are provable!

John Baez (May 21 2024 at 10:56):

But another issue is undecidability. The Lawvere theory of groups is already undecidable, meaning we can't write a program that decides whether or not a given sentence in the language of groups is a consequence of the axioms for groups!

(Again, we can write a program that will eventually say this sentence is a theorem if it is a theorem: just enumerate all theorems. But you can't write a program that will eventually say a sentence is a non-theorem if it's not a theorem.)

I see the undecidability of the theory of groups was proved by Tarski in 1951. Later Mal'cev proved undecidability of the theory of rings, and of semigroups.

Nathan Corbyn (May 21 2024 at 11:33):

The Lawvere theory of groups is already undecidable, meaning we can't write a program that decides whether or not a given sentence in the language of groups is a consequence of the axioms for groups!

I’m not sure I believe this—I thought the word problem for finitely presented groups was undecidable, but the word problem for free groups is straightforward

Nathan Corbyn (May 21 2024 at 11:36):

The Lawvere theory for groups is equivalent to the opposite of the category of finitely generated free groups, not finitely presentable groups. However if you encode groups as an essentially algebraic theory, the corresponding syntactic category is equivalent to the opposite of the category of finitely presentable groups and therefore undecidable.

John Baez (May 21 2024 at 11:43):

I shouldn't have said "the Lawvere theory of groups" - I meant the first-order theory of groups!!!

John Baez (May 21 2024 at 11:45):

Similarly for rings and semigroups.

Matteo Capucci (he/him) (May 21 2024 at 12:39):

John Baez said:

Right, the successor function $S$ needs to 'get along' with $+$ and $\times$, and PA provides the axioms saying exactly how it should. So we can define a Lawvere theory whose algebras are things with $0, S, +, \times$ obeying exactly those axioms. And this is some sort of watered-down version of PA.

But then comes an axiom that you can't describe using a Lawvere theory:

$ Sx = Sy \implies x=y$

However, the hard part of PA is not any of this: it's the axiom schema for induction.

Could this be statable in a sketch? This is saying that S is injective no? In that case, it's not far from being algebraic

Sridhar Ramesh (May 26 2024 at 00:23):

For what it's worth, here is a categorically-oriented way of saying what a model of first-order PA is : Suppose given a nontrivial semiring $N$ (that is, more precisely, a tuple $\langle N, 0, +, 1, \times \rangle$ satisfying the semiring properties and in which $0 \neq 1$). There is a smallest sub-Heyting-category $C$ of Set containing this semiring $\langle N, 0, +, 1, \times \rangle$.

We say this semiring is a model of first-order PA just in case $N$ is a natural numbers object in $C$ (more precisely, just in case the tuple $\langle N, 0, n : N \mapsto n + 1 \rangle$ is a parametrized natural numbers object in $C$).

Sridhar Ramesh (May 26 2024 at 02:28):

Actually, I think a better way to put it is that, given a semiring $\langle N, 0, +, 1, \times \rangle$, we consider the smallest sub-Heyting-pretopos $C$ of Set. This semiring will be a model of first-order PA just in case $\langle N, 0, n : N \mapsto n + 1 \rangle$ is a parametrized natural numbers object in this $C$.

(In this account, the trivial semiring will fail to be a model of first-order PA not by fiat but as a consequence of this pretopos $C$ containing things like the endofunction of $1 + 1$ with no fixed point.)

This NNO condition corresponds to the first-order induction schema (with the definition of $C$ ensuring that we only instantiate the induction schema using properties definable in the first-order language of arithmetic). The recurrences relating $+$, $\times$, and the successor function in PA are automatic here in our presumption of semiring structure (and conversely, this semiring structure is well-known to be derivable in PA). And I believe both the injectivity of successor and the fact that 0 is not in the range of successor should follow by suitable arguments from the NNO property.

[As with any post I ever write, particularly one which does not spell out all the details it alludes to: I could be wrong, but I believe I'm right.]

Sridhar Ramesh (May 26 2024 at 02:47):

In yet other words, the Heyting/Boolean pretopos corresponding to first-order intuitionistic/classical PA should be the initial Heyting/Boolean pretopos with a parametrized natural numbers object. This NNO will automatically carry a unique internal semiring structure satisfying the appropriate recurrences. Models will then be functors from this category to Set preserving Heyting pretopos structure.

(The only reason to even mention the semiring structure is because two such models need not agree in full simply from having the same choice of zero and successor, but they will agree on everything once they agree on addition and multiplication, given Gödel's Chinese remainder theorem trick for describing more general primitive recursions in first-order logic using just those.)

Todd Trimble (May 26 2024 at 03:02):

Sridhar Ramesh said:

In yet other words, the Heyting/Boolean pretopos corresponding to first-order intuitionistic/classical PA should be the initial Heyting/Boolean pretopos with a parametrized natural numbers object. This NNO will automatically carry a unique internal semiring structure satisfying the appropriate recurrences. Models will then be functors from this category to Set preserving Heyting pretopos structure.

(The only reason to even mention the semiring structure is because two such models need not agree in full simply from having the same choice of zero and successor, but they will agree on everything once they agree on addition and multiplication, given Gödel's Chinese remainder theorem trick for describing more general primitive recursions in first-order logic using just those.)

Interesting. This reminds me of the statement that PRA (primitive recursive arithmetic), as an equational theory, is initial among Lawvere theories such that the generating object is a parametrized NNO.

John Baez (May 26 2024 at 07:17):

Do you remember where you heard that statement, Todd? It's starting to sound obvious to me - it didn't at first - but I'd like to add a reference to the nLab, which includes this statement here (probably thanks to you).

John Baez (May 26 2024 at 09:02):

I also think it would be great if someone could prove @Sridhar Ramesh's claim, or find a reference where it's already been proved, because a good category-theoretic description of (classical, first-order) PA can set up a link between "categorical logic" and a big body of work on "traditional logic".

John Baez (May 26 2024 at 09:05):

It's interesting how parametrized NNOs are crucial in all this work, and that makes a lot of sense to me now, since one wants to describe recursion but not going so far as to consider a NNO in a cartesian closed category, which is "too powerful" compared to what we can do with primitive recursion or even recursion in PA.

Sridhar Ramesh (May 26 2024 at 17:36):

Let me expand on why the initial Heyting/Boolean pretopos with a parametrized NNO is equivalent to first-order intuitionistic/classical PA. [By "intuitionistic PA", I mean the same thing as what is standardly called "Heyting Arithmetic".]

Remember, intuitionistic/classical PA is the first-order intuitionistic/classical theory with a sort $N$, a zero element $0 : N$, a successor function $S : N \to N$, operations $+ : N \times N \to N$ and $\times : N \times N \to N$, axioms stating that $S$ is injective, $0$ is not in the range of $S$, recurrence identities $x + 0 = x$, $x + S(y) = S(x + y)$, $x \times 0 = 0$, $x \times S(y) = x \times y + x$, and the induction schema, which says any definable (in the sense of first-order definable in this language by a relation with parameters) subset of $N$ which contains 0 and is closed under $S$ must contain all of $N$.

So, let's see that a Heyting/Boolean pretopos with NNO proves everything first-order intuitionistic/classical PA proves: An NNO is an initial algebra for the $T \mapsto 1 + T$ endofunctor, and thus by Lambek's lemma, we obtain an isomorphism between $1 + N$ and $N$, where $N$ is the carrier of the NNO and the isomorphism is given by the combination of zero and successor. This being an isomorphism says in the internal language of the pretopos that every element of $N$ is precisely one of zero or a successor (not both; thus, $0$ is not in the range of the successor map) and that the successor map is injective.

Furthermore, our recurrence identities for $+$ and $\times$ directly describe how to define unique operators satisfying those recurrences on a parametrized NNO.

Finally, note that Heyting pretoposes are "closed under" first-order definability, so to speak (this is their raison d'être as a concept), so that any first-order definable relation $R(n, x)$ on $N$ and some other tuples of sorts $X$ in this language will correspond to some subobject of $N \times X$ in this pretopos. The set $\{x : X \mid R(0, x) \wedge \forall n : N \left( R(n, x) \Rightarrow R(S(n), x) \right) \}$ is first-order definable as a subobject of $X$ in this pretopos, and by passing to the slice category over it, we obtain another pretopos, where $N$ remains an NNO. In this slice pretopos, $\{n : N \mid R(n, x) \}$ is a subobject of $N$ which contains $0$ and is closed under $S$; thus, a sub-algebra of $N$ as algebras for the $T \mapsto 1 + T$ endofunctor. But as $N$ is an initial algebra, it is isomorphic to this subalgebra (any subobject of an initial object is isomorphic to the initial object). Thus, in this slice pretopos over $\{x : X \mid R(0, x) \wedge \forall n : N \left( R(n, x) \Rightarrow R(S(n), x) \right) \}$, we have established $\forall n : N, R(n, x)$, which amounts to having established the parametrized induction schema in our original pretopos.

Given the closure of Heyting/Boolean pretoposes under the derivations of first-order intuitionistic/classical logic, this concludes showing that a Heyting/Boolean pretopos with parametrized NNO proves in its internal language everything that first-order intuitionistic/classical PA does.

In the other direction, it's well-known how any first-order intuitionistic/classical logical theory gives rise to a Heyting/Boolean pretopos as its "syntactic category" in a suitable sense. We've just seen that when we apply this construction to first-order intuitionistic/classical PA, we get something "no stronger" than the initial Heyting/Boolean pretopos with a parametrized NNO. But what may not be obvious is that these are indeed equal; that we actually get the full structure of an NNO in the syntactic category for PA.

The induction schema guarantees the uniqueness aspect of algebra maps out of $N$, but their existence is not obvious. This existence however is granted by Gödel's Chinese remainder theorem trick showing how "primitive recursions" of functions from naturals to tuples of naturals can be defined in a first-order way using $+$ and $\times$.

John Baez (May 26 2024 at 17:43):

That's cool! If this result is not in the literature anywhere I may just copy a quote of this onto the nLab if that's okay, @Sridhar Ramesh, and say it's from you. I don't understand pretopoi at all but this sounds convincing to me (and the "raison d'etre" you're stating for pretopoi makes me more interested in them).

Valeria de Paiva (May 26 2024 at 19:52):

Sorry, I know nothing about this area. But isn't this exactly what Milly Maietti proved in "The internal type theory of a Heyting pretopos" https://link.springer.com/chapter/10.1007/bfb0097794 (2006)?

Sridhar Ramesh (May 26 2024 at 19:58):

That's certainly on the same topic of Heyting pretoposes with natural numbers objects, but I see no mention of Heyting/Peano Arithmetic within it.