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: community: general

Topic: Nonstandard models of arithmetic

John Baez (Sep 21 2020 at 16:33):

Michael Weiss and I have a new post out:

• Non-standard models of arithmetic (Part 18).

It's a dialog, and in this part we go over some theorems in a paper by Enayat, just clarifying what these theorems say.
The simplest one is:

• Every ZF-standard model of PA that is nonstandard is recursively saturated.

Don't worry - we go through what all these phrases mean!

Nikolaj Kuntner (Sep 21 2020 at 18:46):

Thanks for sharing.
On post 1, in the paragraph with phi and psi, I think it's hard to follow why something there holds "indeed all finite n’s".
(I also spotted one grammar error there, "a extension")

Nikolaj Kuntner (Sep 21 2020 at 18:48):

"Roughly, my dream is to show that “the” standard model is a much more nebulous notion than many seem to believe."
How nefarious of you :smiling_devil:

Nikolaj Kuntner (Sep 21 2020 at 19:49):

(Strange sentences / Typos:
Post 4: Says „at this remove„, which is probably an autocorrect insert of the word remove. Probably it means „at this point“.
Post 4: „I can prove in there that’s there’s an initial model of PA“ also seems to have been broken with edits. Funny thing is that that line is also quoted again in Post 5.
Post 6: „To me, it lies one of these patches that come after all the standard numbers.“)

Continuing with post 2: When types are sets of formulas relating to an element and we prove stuff with it, what’s our metalogic - if formalized at all. It seems to collect sets of formulas, so it sounds strong. People invoke True Arithmetic, but whether that might be easy to grasp and formally capture doesn’t seem to be bothering many?
I suppose the rest of the first 6 posts was then philosophy and perspectives.
How come Predcativism didn’t come up? I wonder if some of the circularity concerns and standard vs. non-standard discussions would be disallowed upfront by that approach.
What’s also a bit up in the air for me is what a construction of non-standard model in ZFC entails. I mean in plain old FOL, we just have some closed there-exists formulas anyway.
With regard to the „Hilbert gambit“ discussed, I think that’s somewhat by accepting not numbers or well-formed formulas, but computer code.
I personally don’t understand Platonism or the desire to pin down a model. To me, the syntactic structure given by a set of axioms together with deduction rules just is what it is and proves what it proves?

John, you speak about playing the „name the largest number“ game and making use of the busy beaver, but maybe - since the last 3 posts are all philosophical and all - there’s no point of playing the game with non-computable functions and symbols.

I stopped before post 7 but will read on when I get to it.
I really like the socratic dialog form of it all, I laughed a couple of times with the anecdotes.

John Baez (Sep 22 2020 at 01:11):

Thanks for the corrections/comments, NIkolaj!

"At this remove" means "from this far away". E.g. "at this remove, all Middle-Eastern sheikhs with autocratic tendencies look the same" - that's something a western journalist could say.

John Baez (Sep 22 2020 at 01:14):

Continuing with post 2: When types are sets of formulas relating to an element and we prove stuff with it, what’s our metalogic - if formalized at all. It seems to collect sets of formulas, so it sounds strong.

We're not formalizing it much, but if you want to, it's something nice and strong, like ZFC. We want to be able to reason freely here, using all the tools of classical mathematics.

John Baez (Sep 22 2020 at 01:15):

Here's a more readable summary of Post 18, which I wrote today:

• John Baez, Enayat on Nonstandard Numbers, Azimuth.

John Baez (Sep 22 2020 at 01:15):

By the end of this post you should be able to roughly understand what this means - but not why it's true:

In short, Enayat has found that countable ZF-standard models of Peano arithmetic in the universe V come in two drastically different kinds. They are either ‘as standard as possible’, namely V-standard. Or, they are ‘extremely rich’, containing n-tuples with all possible lists of consistent properties that you can print out with a computer program: they are recursively saturated.

John Baez (Sep 22 2020 at 01:26):

Nikolaj Kuntner said:

On post 1, in the paragraph with phi and psi, I think it's hard to follow why something there holds "indeed all finite n’s".

Let's see, you're talking about this:

If the set you want to code is totally arbitrary, well, you can't even express it in the language of PA, so we want to look at sets that are definable by a formula. Then we can apply the overspill lemma. Say $\varphi(x)$ is the formula for the set. Consider the formula $\psi(y) \iff (\exists z)(\forall x\lt y)[\varphi(x)\leftrightarrow p_x|z]$. Here $p_x$ is the xth prime. Since $\psi(n)$ holds for arbitrarily large finite $n$'s (indeed all finite $n$'s), overspill says that it also holds for some non-standard $n$.

John Baez (Sep 22 2020 at 02:57):

So: we've got a set S of natural numbers described by some formula $\varphi$, and $\psi(y)$ says "there is a natural number $z$ that's the product of all primes $p_x$ for which $x < y$ and $x$ is in the set S." So yes, this is true for all $y$.

John Baez (Sep 22 2020 at 03:01):

Really $\psi(y)$ says "there is a natural number $z$ such that for all $x \lt y$, the xth prime divides $z$ iff $x$ is in the set S". But this is equivalent.

André Beuckelmann (Sep 22 2020 at 15:58):

If I may piggyback off this thread, have you studied (or know) whether there are any connections between nonstandard models of PA and category theory? I'm curious, if, for example, there is some natural way to view any model of PA as the natural numbers object of some nice category.
I guess you could use your model to get one of finite set theory and view this as a category. You would then have to add a couple of colimits to it, but do so in some way that is interesting (you could, of course, add only one colimit to construct your natural numbers object, but that wouldn't really result in a nice category), and doesn't allow you to construct the "actual " natural numbers (so we probably cannot simply take the cocompletion). Without any evidence, I'd conjecture there is probably some nicer way to do it, though.

John Baez (Sep 22 2020 at 16:16):

I'm trying to develop the connection between nonstandard models of PA and category theory: in parallel to Michael Weiss and I talking about nonstandard models of PA, we're talking about categorical logic. But don't get your hopes up too high: I've been moving forward very slowly. So I don't know if any model of PA is the natural numbers object in some category. This seems like a nice thing to try.

Enayat, whose work we are discussing, is focused on "T-standard models" of PA, where T is a recursive extension of ZF. These are models that "look standard" in some model of T. I'd bet these are natural numbers objects in certain categories.

Jonas Frey (Sep 22 2020 at 16:24):

André Beuckelmann said:

If I may piggyback off this thread, have you studied (or know) whether there are any connections between nonstandard models of PA and category theory?

I haven't read through the entire conversation and am not super familiar with the subject, but my understanding is that non-standard models of 1st order theories are obtained as "ultrapowers" of "standard" models, and these have been studied by Makkai, and more recently Lurie, from a categorical perspective.

Jonas Frey (Sep 22 2020 at 16:26):

However, in this approach you don't think about models of PA as NNOs in different categories, but you think about all Set-models of PA as forming one category, morphisms being elementary embeddings, I think. The observation then is that this category admits an "ultracategory structure".

Jonas Frey (Sep 22 2020 at 16:27):

But actually Makkai only does this for coherent and geometric theories, so I'm not sure how it works in the 1st order case.

John Baez (Sep 22 2020 at 16:30):

Ugh, there's so much I need to learn. I've tried a few times to understand ultrapowers, but my mind bounces off them instantly - they're not something I have any feeling for.

John Baez (Sep 22 2020 at 16:32):

I'm trying to learn about hyperdoctrines because they're a categorical approach to classical first-order logic. I want to strike a nice balance between traditional model theory and category theory. That is, I want to be able to translate existing results about model theory for first-order logic (esp. results on nonstandard models of PA) into category theory without doing a whole lot of work.

Jonas Frey (Sep 22 2020 at 16:33):

I'll share my thinking about the coherent case: whereas categories of models of algebraic theories (eg the category of monoids) are closed under all limits and colimits, models of coherent theories (eg the category of fields) are neither. However, there is a supercategory of the category of fields which consists of objects equipped with the operations +,x,0,1, but not subject to the field axioms. Such things are sometimes called "structures" over the "signature" $\Sigma=\{+,x,0,1\}$, so let's call the category $\Sigma$-$Struct$.

Jonas Frey (Sep 22 2020 at 16:37):

$\Sigma$-Struct is closed under arbitrary limits and colimits, in particular under "categorical ultrapowers": Given a structure S, a set A, and an ultrafilter $\mu$ on A, the ultrapower of S by $\mu$ is the filtered colimit over the filter (ordered by inverse inclusion), of the powers $S^U$ for $U\in\mu$.

Jonas Frey (Sep 22 2020 at 16:39):

Now the observation is that is $S$ a model of the coherent theory -- eg fields -- , then any ultrapower is again, even though the powers $S^U$ are normally not. I think that also works for 1st order, and model theorists have name for that which I don't remember.

Jonas Frey (Sep 22 2020 at 16:44):

So ultrapowers are a mix of limits and colimits, and so don't have a nice universal property (that I know of). The ultrapower of fields can only be defined by embedding the category into the larger category $\Sigma$-Struct. However, the ultrapowering operation satisfies some axioms; a category with such an operation satisfying these axioms is called "ultracategory" by Makkai.

John Baez (Sep 22 2020 at 16:44):

Thanks. This is clearer than anything I've read so far! "Ultrapower = filtered colimit of powers, where the diagram involved is an ultrafilter".

Jonas Frey (Sep 22 2020 at 16:45):

yes! but often defined relative to an inclusion of categories, where the powers are in the larger category, whereas the result is in the smaller one again.

John Baez (Sep 22 2020 at 16:46):

At some point I'll ask Michael Weiss to list a bunch of ways to create nonstandard models of PA, and see if something like ultrapowers is one.

Jonas Frey (Sep 22 2020 at 16:47):

I thought that was the "standard" way of getting non-standard models :-D

Jonas Frey (Sep 22 2020 at 16:49):

anyway, "abstract" ultracategories are equipped with a stucture of ultrapowers that only have to satisfy certain axioms, and are not necessarily given by a filtered colimit of powers.

Jonas Frey (Sep 22 2020 at 16:50):

there's a strong link to topology: an ultrastructure on a small discrete categgory (ie a set) is a compact Hausdorff topology on the space.

Jonas Frey (Sep 22 2020 at 16:53):

coming back to PA, it's interesting that while we spend a lot of time studying the category of models of, say the theory of groups, category theorists are much less used to thinking about the category of models of PA (which might be an ultracategory in the sense of Makkai).

Dan Doel (Sep 22 2020 at 17:44):

Well, there's probably at least a couple reasons for that. One being inherited bias about "foundational" theories vs. the theories studied in algebra. Another being that when you discover something is e.g. a topos, you get a really convenient set/type theoretic theory to work in, but discovering the same thing about PA still requires you to encode all your ideas as formal natural numbers.

Reid Barton (Sep 22 2020 at 17:48):

As a category theorist who isn't used to thinking about models of PA: is there a way to present PA that doesn't involve an axiom schema that quantifies over formulas?

Reid Barton (Sep 22 2020 at 17:49):

Because that already makes it feel like the sort of thing I don't really know anything about.

John Baez (Sep 22 2020 at 17:53):

If they want a finitely axiomatizable theory people often work with Robinson arithmetic, also called "Q". I don't think PA is finitely axiomatizable. But I haven't done anything - in my extremely limited work on these matters! - where a finitely axiomatizable theory has better behavior than a recursively axiomatizable theory.

Dan Doel (Sep 22 2020 at 17:54):

Q is considerably weaker though, I think.

John Baez (Sep 22 2020 at 17:55):

Yes!

As far as I can tell it's just a nice approximation to "the weakest theory of arithmetic for which Goedel's first incompleteness theorem holds".

Nikolaj Kuntner (Sep 22 2020 at 17:56):

When I mentioned predicativity in relation to the busy beaver considerations, I had e.g. this book in mind, which tries to get as far as possible without induction.
https://web.math.princeton.edu/~nelson/books/pa.pdf
That's not quite finitism, but (at the risk of painting a strawman) I think the case being made is as follows:
Not assuming anything beyond PA, we'd generally define the natural numbers as the collection of terms fulfilling 2 axioms about equality, 2 about addition, 2 about multiplication and then induction. With the induction scheme thus says the natural numbers are that which fulfills all these axioms. The impredicativity concern is then that in the scheme we include predicates that are also complicated somewhere in the hierarchy and have quantifiers over.. well the natural numbers. But didn't we just define them in terms of all the predicates? :)

John Baez (Sep 22 2020 at 17:57):

Yes, I like Nelson's work.

John Baez (Sep 22 2020 at 17:57):

(He refused to take me on for my undergraduate thesis at Princeton, but that's okay.)

Nikolaj Kuntner (Sep 22 2020 at 17:58):

:D

Nikolaj Kuntner (Sep 22 2020 at 17:58):

He does have a cool pic online

Nikolaj Kuntner (Sep 22 2020 at 17:58):

Edward_Nelson.png

Nikolaj Kuntner (Sep 22 2020 at 18:02):

So, with your concern about the busy beaver, is it likely that something can be said about it that puts people in shock?
You wrote about potential of numbers of that sort could in some way be rather in the transfinite range, did I understand this correctly? I know as a function the thing is not computable, but if we pick some given n and consider the corresponding busy beaver value, will this not be a normal number of some sort?

Nikolaj Kuntner (Sep 22 2020 at 18:02):

necessarily

John Baez (Sep 22 2020 at 18:03):

What I really like about Nelson's work is his crazy idea that some seemingly standard natural numbers may actually be nonstandard. This is hard to formalize but he did a great job in his work on internal set theory.

John Baez (Sep 22 2020 at 18:08):

but if we pick some given n and consider the corresponding busy beaver value, will this not be a normal number of some sort?

Of course that's true according to the usual approach to mathematics. Nelson's crazy idea is that very large seemingly standard numbers can only be proved to exist using principles of logic that one might decide to drop.

Reid Barton (Sep 22 2020 at 18:10):

I think what sets PA apart for me is not just that it has infinitely many axioms (for instance, so do complex vector spaces or operads) but that quantification over formulas in particular has a syntactic nature which would need to be digested somehow.

Nikolaj Kuntner (Sep 22 2020 at 18:14):

By quantification over formulas you mean the axiom schema notion in general?

Reid Barton (Sep 22 2020 at 18:14):

In particular, you can "compile out" the definition of a group (or whatever) as the models of a first-order theory into ordinary mathematical statements like "for all $g$, $g \cdot 1 = g$", but you can't do the same thing to PA without keeping the notions of formulas and satisfaction... as far as I know.

John Baez (Sep 22 2020 at 18:16):

Certainly there's no Lawvere theory for PA the way there is for groups.

John Baez (Sep 22 2020 at 18:18):

Perhaps the infinitary nature of the principle of mathematical induction in PA - the fact that it's an axiom schema that (apparently) can't be compressed to finitely many axioms - is part of what makes Nelson suspicious of it.

John Baez (Sep 22 2020 at 18:18):

If one is trying to understand the countably infinite, doing so with a countably infinite set of axioms seems somehow unfair. :upside_down:

Nikolaj Kuntner (Sep 22 2020 at 18:20):

So what's your true motivation for wanting for people to be more wary about those things?
Do you think too few people are too sure of what they think to know is essentially correct? What's the quest.

Dan Doel (Sep 22 2020 at 18:20):

That doesn't seem like the nature of the complaint.

Nikolaj Kuntner (Sep 22 2020 at 18:22):

I agree, I don't necessarily categorize the "predicativity guys" among those wanting finitely layed out structures.

Dan Doel (Sep 22 2020 at 18:22):

There are impredicative theories with, I think, finitely many axioms.

Nikolaj Kuntner (Sep 22 2020 at 18:24):

Tautologically so if we define a theory loosely as just what comes with a set of axioms :)

John Baez (Sep 22 2020 at 18:24):

I like this passage in Nelson's book Internal Set Theory - it's inspiring to me. He develops a way of adding a predicate called "standard" to a wide class of theories, and he proves:

Theorem 4. There is a finite set that contains every standard object.

Then he says:

If we think of “standard” semantically—with the world of mathematical objects spread out before us, some bearing the label “standard”and others not—then these results violate our intuition about finite sets.

[....]

Perhaps it is fair to say that “finite” does not mean what we have always thought it to mean. What have we always thought it to mean? I used to think that I knew what I had always thought it to mean, but I no longer think so.

Dan Doel (Sep 22 2020 at 18:25):

Well, I have specific examples in mind. Like System F or the calculus of constructions, although those don't line up exactly with PA.

Dan Doel (Sep 22 2020 at 18:25):

They both let you define the natural numbers and functions on them that Nelson didn't like, though.

Nikolaj Kuntner (Sep 22 2020 at 18:26):

inspiring to some, scary to others :D

Nikolaj Kuntner (Sep 22 2020 at 18:28):

burger.jpg
The most entertaining angry rants of a finitist are Wildberger on youtube.
But at the end of the day he doesn't engage on any syntactic axiomatic level, so the debate is not a formalizable one.

Dan Doel (Sep 22 2020 at 18:29):

Although even predicative polymorphic lambda calculi let you define too much by his criteria.

Nikolaj Kuntner (Sep 22 2020 at 18:30):

When you say System F I think Haskell, and then I think computers, and then I don't know if enough people have yet dedicated time to studying actually bounded-memory-only computation and mathematics.

John Baez (Sep 22 2020 at 18:34):

Nikolaj Kuntner said:

So what's your true motivation for wanting for people to be more wary about those things?

I don't want anyone to be wary about these things unless they enjoy it. I'm not interested in making people worry more. I just want to have fun.

Do you think too few people are too sure of what they think to know is essentially correct? What's the quest?

I'll say this very vaguely, since you're wisely asking for a quest instead of a theorem. (To understand what a mathematician is doing you need to know their quest, not their theorems.)

I think the concept of "standard" model of PA is circular in a subtle way.

Very very crudely, the standard natural numbers are 0, 1, 1+1, 1+1+1, ... But what does the "..." mean? It means that we keep on going. But how long do we keep on going? What sort of expressions 1+...+1 count as natural numbers? Only those where there's a standard natural number of plus signs!

But this is circular.

There's a lot of evidence that every model of PA "feels standard to itself", but I want to make this clearer.

To do this, I want a way to exhibit situations where I think I'm dealing only with standard natural numbers, while you think some of my numbers are nonstandard. That is: I want a framework where in some context some model of PA counts as "standard", but in some other context that model counts as "nonstandard".

Nikolaj Kuntner (Sep 22 2020 at 18:40):

Okay, I see. I hope you succeed clearing things up in a new way.

Nikolaj Kuntner (Sep 22 2020 at 18:41):

Do you discuss models without set theory context in the blog beyond post 7?

Nikolaj Kuntner (Sep 22 2020 at 18:43):

You single out standard models as less understood. Maybe something like this holds for insert type of models kind of models in general.
And then maybe one approach is to work in terms of not-non-standard models :)

John Baez (Sep 22 2020 at 18:43):

I don't know what you mean by "models without set theory context".

John Baez (Sep 22 2020 at 18:44):

Michael Weiss and I talked about the framework I'd like to use for understanding models of first-order theories here:

• First-order categorical logic

John Baez (Sep 22 2020 at 18:45):

But I got too busy to work on this right around when it started getting interesting. I hope to return to it sometime.

Nikolaj Kuntner (Sep 22 2020 at 18:45):

Since it's a negative notion, I don't mean anything particular - I ask for models that don't involve set theory to build them and maybe you know just as much as me haha

Nikolaj Kuntner (Sep 22 2020 at 18:48):

John Baez said:

Michael Weiss and I talked about the framework I'd like to use for understanding models of first-order theories here:

• First-order categorical logic

Ah, so it's not the first conversation between you that's recorded in this fashion.

I find the idea of a first-order theory that ties closely to universal properties in the category sense very appealing, but as long as I naturally tend to think of arrows as the derived notion, using category theory on the lowest level of languages appears as importing overhead and so I never really dared to leave $\in$ out and aside.

John Baez (Sep 22 2020 at 18:51):

Nikolaj Kuntner said:

John Baez said:

Michael Weiss and I talked about the framework I'd like to use for understanding models of first-order theories here:

• First-order categorical logic

Ah, so it's not the first conversation between you that's recorded in this fashion.

These two conversations were (and are) going on in parallel. Roughly Michael was teaching me logic, and I was teaching him category theory. But I was also trying to learn about hyperdoctrines and build them into a framework for studying model theory in first-order classical logic. My ambitions exceeded my energy. But I may keep trying.

John Baez (Sep 22 2020 at 18:57):

Nikolaj Kuntner said:

...using category theory on the lowest level of languages appears as importing overhead and so I never really dared to leave $\in$ out and aside.

I'm not interested in "establishing foundations for mathematics" - setting it up from scratch - so I don't care about "importing overhead". I want the freedom to use any tools I want to study logic, just as I would in algebra or geometry. To do mathematics these days without using categories is like tying one hand behind one's back, and the same is true for metamathematics.

Nikolaj Kuntner (Sep 22 2020 at 19:14):

JB: Wow, three remarks and two questions! This is truly a hydra-headed comment. Unlike Hercules, I won’t tackle them all, just a few of my favorites.

lol

André Beuckelmann (Sep 22 2020 at 20:27):

@John Baez First of all, thanks for your response earlier.

If I understand your goal correctly, I think you might be interested in Joel David Hamkins work on the set theoretic multiverse and the well-foundedness mirage. Now, I cannot even remotely understand his it (I'm just aware of its existence), but I believe his point is the following: as you have already noticed, the "standardness" of your natural numbers depends very much on your background theory. Hamkins now applies this principle to set theory (though his motivations for doing so are different): instead of focusing on one particular model, he tries to axiomatise the collection of all models of set theory (which he, then, calls the multiverse). One particular axiom he adds, the well-foundedness mirage - and which turns out to be consistent - is that the ordinals, or even the natural numbers, of every particular set theoretic universe appear to be non-standard to another, better universe.

Nikolaj Kuntner (Sep 22 2020 at 21:43):

In regards to the axiom schema conversation before
https://mathoverflow.net/questions/326470/does-every-first-order-theory-have-a-finitely-axiomatizable-conservative-exten

Morgan Rogers (he/him) (Sep 22 2020 at 21:45):

John Baez said:

There's a lot of evidence that every model of PA "feels standard to itself", but I want to make this clearer.

This reminds me of a very insightful comment I heard at Toposes in Como back in 2018, made by a guy called Alexander whose last name I can't remember, that:

Every elementary topos thinks it's a Grothendieck topos,

which is to say that the constructive internal logic of any topos is the same, despite the quantifiable differences between them as categories. That's not all: for example, Set has all Set-indexed colimits, but in fact any elementary topos $\mathcal{S}$ has all $\mathcal{S}$-indexed colimits, so the notion of "small" colimits is relative to our notion of what sets are.

Returning to the present topic, I would be curious if someone were to investigate precisely which class of models of PA can occur as NNOs of toposes. Non-toposic NNOs would have an extra level of "non-standardness" to me.

Nikolaj Kuntner (Sep 22 2020 at 21:49):

Can you qualify "internal logic of any topos is the same" more, given $1\to\Omega$ can take quite different shapes?
Also, should I read into this that all logics (also w.r.t. the above comment) that I see in any elementary topos, I already see in Grothendieck topoi?

David Michael Roberts (Sep 22 2020 at 23:58):

@[Mod] Morgan Rogers Alexander Gietelink Oldenziel?

John Baez (Sep 23 2020 at 00:02):

Alexander Grothendieck?

David Michael Roberts (Sep 23 2020 at 00:03):

@John Baez ho ho, but 2018 was too late.

Morgan Rogers (he/him) (Sep 23 2020 at 06:52):

Nikolaj Kuntner said:

Can you qualify "internal logic of any topos is the same" more, given $1\to\Omega$ can take quite different shapes?
Also, should I read into this that all logics (also w.r.t. the above comment) that I see in any elementary topos, I already see in Grothendieck topoi?

I was referring to the metatheorem that 'every constructively provable Set-theorem holds in any topos'. There are caveats to that, like how for almost anything infinitary you need the topos to have a NNO, so don't take this as a precise statement, but a more precise form of this principle is in constant use in topos theory :grinning_face_with_smiling_eyes:

André Beuckelmann (Sep 23 2020 at 09:08):

There is also the fact that Kripke frames (presheaves on a poset) are a complete semantic for intuitionistic first order logic, so, whenever you have an elementary topos satisfying some some collection of sentences, you can find one such topos (in particular, a Grothendieck topos) that does the same. I'm not sure, if there are other logic that can tell the difference between elementary topoi and Grothendieck topoi, though (infinitary logics might work, but I don't think you can interpret them in arbitrary elementary topoi, so this doesn't really count).

John Baez (Sep 24 2020 at 23:07):

Here's another blog article where Michael and I try to figure out what Enayat is talking about:

• Non-standard Models of Arithmetic 19: We marvel a bit over Enayat's Prop. 6, and especially Cor. 8. The triple-decker sandwich, aka three-layer cake: $\omega^U \subset U \subseteq V$. More about why the omegas of standard models of ZF are standard. Refresher on $\Phi_T$. The smug confidence of a ZF-standard model.

Nikolaj Kuntner (Sep 29 2020 at 21:02):

I was wondering, if there is any set theory which, instead of Regularity or Set Induction, instead adopts Infinity and postulates Induction only for $\omega$. In a scarce environment otherwise, how much of set theory is implied by induction just for the naturals? Going through some papers about constructive math without LEM and Powerset, it indeed doesn't even seem to be implied by the existence of function spaces. My findings are inconclusive on how Full Mathematical Induction as an axiom would relate to Strong Collection (LEM+Replacement implies full Separation which I think implies Mathematical Induction). E.g. can full mathematical induction be proven in Aczel non-wellfounded theory?

Daniel Geisler (Oct 01 2020 at 22:09):

I hope this question is appropriate here. John Conway found that games are a generalization of numbers. Doesn't there need to be a "game" arithmetic?

Nikolaj Kuntner (Oct 01 2020 at 22:26):

@Daniel Geisler https://en.wikipedia.org/wiki/Surreal_number#Arithmetic

John Baez (Oct 03 2020 at 20:16):

More fun mathematical logic:

• Nonstandard Arithmetic: A Long Comment Thread

This is a discussion between Michael Weiss, Bruce Smith and me. Topics: (a) Why do standard models of ZF have standard ω’s? (b) Interactions between the Infinity Axiom and the Foundation Axiom (aka Regularity). (c) The compactness theorem. (d) The correspondence between PA and “ZF with infinity negated”: nonstandard numbers vs. ill-founded sets, and the Kaye-Wong paper.

John Baez (Oct 03 2020 at 20:17):

There are further comments on this comment thread, for example about "how effective is Goedel's completeness theorem?"

John Baez (Oct 03 2020 at 20:19):

Also:

• Topics in Nonstandard Arithmetic 1: Table Setting.

This is Michael Weiss explaining the context for work on nonstandard models of Peano arithmetic.

John Baez (Oct 03 2020 at 20:20):

• Topics in Nonstandard Arithmetic 2: The Arithmetic Hierarchy.

This is Michael's easy intro to the arithmetic hierarchy - a classification of subsets of the natural numbers.

Todd Trimble (Oct 11 2020 at 18:59):

John Baez said:

Certainly there's no Lawvere theory for PA the way there is for groups.

There is however a Lawvere theory for primitive recursive arithmetic: PRA can be described as the initial object among Lawvere theories whose generating object is a parametrized NNO.

Jonas Frey (Oct 11 2020 at 19:07):

PRA can be described as the initial object among Lawvere theories whose generating object is a parametrized NNO.

I don't know what you mean by "Lawvere theories whose generating object is a parametrized NNO". For me, Lawvere theories are categorical manifestations of (single sorted) algebraic theories, and PRA is not algebraic. I would have said that the syntactic category of PRA is the free "list -arithmetic pretopos".

edit: OK, I guess the generating object of a Lawvere theory can be a parametrized NNO, I have never thought about it this way. That's interesting!

Jonas Frey (Oct 11 2020 at 19:19):

... but what would the models of this Lawvere theory be? The Set-models in the usual sense would form a locally finitely presentable category, having in particular a terminal object. That's clearly different from non-standard models of PA/PRA. On the other hand, when restricting to Set-models preserving the pararmetrized NNO, I think we're back to only the standard model.

Dan Doel (Oct 11 2020 at 19:21):

An NNO isn't a product, so it doesn't need to be preserved, right?

Jonas Frey (Oct 11 2020 at 19:23):

No, it's not a product in a non-trivial sense. In particular, the terminal model of the Lawvere theory that Todd proposes maps the NNO to the singleton set, which is not an NNO in Set.

Todd Trimble (Oct 11 2020 at 19:30):

A few more details here.

I meant that the equations provable in PRA are precisely the equations that hold in this initial object.

One can consider models other than $\mathsf{Set}$-valued ones.

John Baez (Oct 11 2020 at 20:21):

What's the terminal model in Set? A one-element set where all operations are what they have to be? I guess that's what it has to be, since that's how it works for Lawvere theories (since the category of models in Set has a right adjoint forgetful functor to Set)/

Oh - Jonas Frey said this. (It's easy for me to read posts here without seeing that they have followups.)

John Baez (Oct 11 2020 at 20:32):

So, one curious feature of this version of arithmetic is that unlike in Peano arithmetic, you cannot prove any inequalities at all. So you can't prove $1 \ne 0$.

Todd Trimble (Oct 11 2020 at 20:49):

For the theory itself, of course you can prove $1 \neq 0$. The product-preserving functors need not preserve inequalities.

Dan Doel (Oct 11 2020 at 21:35):

That seems like talking about two different things.

Todd Trimble (Oct 11 2020 at 21:59):

Jonas Frey said:

PRA can be described as the initial object among Lawvere theories whose generating object is a parametrized NNO.

I don't know what you mean by "Lawvere theories whose generating object is a parametrized NNO". For me, Lawvere theories are categorical manifestations of (single sorted) algebraic theories, and PRA is not algebraic. I would have said that the syntactic category of PRA is the free "list -arithmetic pretopos".

edit: OK, I guess the generating object of a Lawvere theory can be a parametrized NNO, I have never thought about it this way. That's interesting!

So I think we're talking about the same subject matter, essentially. It may be best if I refer to the (excellent) master's thesis of Alan Morrison. A lot of details of Joyal's unpublished notes on his approach to Gödel incompleteness can be found there. A cartesian category $E$ with (parametrized) NNO $N$ is a Skolem theory if every object in $E$ is a finite power of $N$. All of primitive recursive arithmetic can be interpreted in a Skolem theory. From $E$ one can form a new category $E'$ whose objects $P$ are "predicates" on $N$ (morphisms $f: N \to N$ whose values are $0, 1$; more formally, satisfying $f \cdot f = f$), and whose arrows $A \to B$ are functions $g: N \to N$ for which $A \leq B \circ g$. (Correction: one needs to take suitable equivalence classes of such morphisms.) This forms a regular extensive category with suitable arithmetic list objects. By taking its exact completion $E''$, we get a list-arithmetic pretopos, called an arithmetic universe. The Joyal story continues from there: one shows that internal to any arithmetic universe, one has enough structure to construct an initial Skolem theory.

Todd Trimble (Oct 11 2020 at 22:12):

Anyway, I was saying that PRA can be neatly described in terms of Lawvere theories. Skolem theories are by definition Lawvere theories where the generating object is an NNO. I wasn't trying to draw attention particularly to the category of product-preserving functors from a Skolem theory to $\mathsf{Set}$. It seems that Morrison is putting the category of Skolem theories more at the center of attention (he defines a morphism of Skolem theories to be "lex functors that preserve recursion", definition 5.2, and claims that the assignment $E \mapsto E''$ gives a full embedding into the category of arithmetic pretoposes, lemma 6.15).I haven't studied any of this in detail.

Jonas Frey (Oct 11 2020 at 22:34):

Todd Trimble said:

I wasn't trying to draw attention particularly to the category of product-preserving functors from a Skolem theory to $\mathsf{Set}$.

Yes that was me, I was just thinking out loud. Anyway, the notion of Skolem-theory is very nice!

John Baez (Oct 11 2020 at 22:45):

Todd Trimble said:

For the theory itself, of course you can prove $1 \neq 0$. The product-preserving functors need not preserve inequalities.

Sorry, I was secretly switching to a more traditional view of models of first-order theories in Set, where you have axioms and what's provable is exactly what holds in all models. I think you can take any Lawvere theory L and create a first-order theory T (written in the predicate calculus) whose models (in the usual sense of first-order logic) correspond to models of L (in the usual sense of Lawvere theories). My point was that Lawvere theories translate into first-order theories T that can't prove any inequalities. That's what I was trying to say (without explaining what I meant).

John Baez (Oct 11 2020 at 22:47):

It's odd that I changed the outlook without explaining what I was doing; I think it's because I'm talking to Michael Weiss about the traditional model-theoretic approach to PA these days.

Todd Trimble (Oct 11 2020 at 23:35):

Right. My "you can prove" was at a meta level. There's a whole array of completeness theorems for various "categorical logics" (finite product logic, finite limit logic, regular logic, etc.), but finite-product logic is too weak to speak internally of inequalities.

Anyway, if you have any pretopos with a parametrized NNO N, you can manufacture a Skolem theory in an obvious way, and what I was sketching above implies that all Skolem theories (= models of PRA in the sense I was intending) arise in this way. There are lots of "nonstandard" Skolem theories, e.g., take an ultrapower of $\mathsf{Set}$ and the NNO inside that. I'm tentatively suggesting it could be easier to think about those than about nonstandard models of PA (cf. Reid's discomfort with the syntactic nature of having to quantify over formulas, and the messages by Dan and Reid at 1:44 PM and 1:48 PM on September 22 [this time may be referring to EDT; I'm not sure]).

Jonas Frey (Oct 12 2020 at 00:45):

Two comments on the $0\neq 1$ issue. These might be obvious to you, but I remember being confused about similar things myself in the past, so I think it might be worth spelling these out.

• $0\neq 1$ is "provable" in PA, but only because $\forall x (0\neq S(x) )$ is an axiom. So the proof is simply an instantiation of this axiom.
• I would say that in a Skolem theory one cannot even ask the question whether $0\neq 1$ holds, since Skolem theories are purely equational and don't admit negation. However, Todd pointed out that every Skolem theory has an "enveloping" pretopos, and there the $0\neq 1$ is always true, even if $0=1$ holds in the Skolem theory (in the latter case the theory associated to the pretopos is inconsistent, ie the pretopos is the terminal category)

Todd Trimble (Oct 12 2020 at 01:03):

Nice comments, Jonas, particularly the second.

Morgan Rogers (he/him) (Oct 12 2020 at 08:52):

John Baez said:

Todd Trimble said:

For the theory itself, of course you can prove $1 \neq 0$. The product-preserving functors need not preserve inequalities.

Sorry, I was secretly switching to a more traditional view of models of first-order theories in Set, where you have axioms and what's provable is exactly what holds in all models.

Even without any completeness results, it seems perverse to talk about "proving" things in the theory which aren't preserved by the semantics under discussion, even if you pass to an enveloping category which can carry richer logical structure. This is the problem with using the word "theory" to refer to both a category and the syntax/formal logic it encodes, since these things are fundamentally different (sorry Lawvere!). If I use 'syntactic category' to refer to the former thing, then what I'm trying to say is that you can prove things about that syntactic category "at a meta level", as @Todd Trimble puts it, but any logical-categorical structure not preserved by the interpreting functors can't be considered part of the theory that category carries. The discussion above shows how easy it is to accidentally conflate these ideas because they sometimes carry the same name.

John Baez (Oct 12 2020 at 15:40):

Todd wrote:

It seems that Morrison is putting the category of Skolem theories more at the center of attention (he defines a morphism of Skolem theories to be "lex functors that preserve recursion", definition 5.2.

It would be nice to know the internal language of Skolem theories, i.e. roughly the things you can "say" in a Skolem theory that are preserved by these morphisms.

John Baez (Oct 12 2020 at 15:41):

Maybe the embedding into an arithmetic pretopos would help answer this: I don't know anything about the internal language of a pretopos, but probably someone does.

Todd Trimble (Oct 12 2020 at 16:59):

It helps to think of a pretopos as a set-like environment in which to do [intuitionistic] first-order logic (in a topos, you can do first-order logic and higher-order logic). That is, it has the basic exactness properties of a topos (you have finite limits, disjoint coproducts, quotients of equivalence relations, these colimits are nicely stable under pullback, and there is a natural bijections between equivalence relations, kernel pairs and partitions = iso classes of quotients) -- but you don't have power objects. Paul Taylor's book Practical Foundations of Mathematics is a pretty good place to read about them.

Dan Doel (Oct 12 2020 at 17:07):

Which sort of pretopos does that describe? ΠW?

Dan Doel (Oct 12 2020 at 17:14):

I'd been thinking of them as different variants of predicative type theory, but it's not clear to me how you'd get $0 \neq 1$ in the 'obvious' type theory corresponding to the explicit features, since in e.g. Martin-löf type theory you need a universe (small object classifier) to have disjoint coproducts and the like.

Jonas Frey (Oct 12 2020 at 17:17):

I think Johnstone calls a pretopos that interprets full first order logic a "Heyting pretopos". In general, pretoposes need not admit implication and universal quantification, but only model "coherent logic", ie the fragment of first order logic with the connectives $=,\wedge,\top,\exists,\vee,\bot$.

Dan Doel (Oct 12 2020 at 17:18):

Oh, that's the weakest version I'm familiar with, actually. :)

Dan Doel (Oct 12 2020 at 17:18):

I guess a Heyting pretopos has a 'universe' of propositions that is too large for it to quantify over itself?

Dan Doel (Oct 12 2020 at 17:19):

(Looking at nlab.)

Jonas Frey (Oct 12 2020 at 17:20):

For example, when replacing "partial recursive functipons" with "primitive recursive functions" in the construction of the effective topos, one gets a list-arithmetic pretopos that doesn't have $\forall,\Rightarrow$.

Jonas Frey (Oct 12 2020 at 17:22):

Dan Doel said:

I guess a Heyting pretopos has a 'universe' of propositions that is too large for it to quantify over itself?

That's a possible way of looking at it, as one can always embed into a suitable category of sheaves where the presheaf of subobjects is representable.

Todd Trimble (Oct 12 2020 at 17:23):

Sorry for the confusion!

Dan Doel (Oct 12 2020 at 17:25):

@Jonas Frey Oh, I guess it could be a parallel judgment to the $\mathsf{type}$ judgment. That'd probably be more like it.

Dan Doel (Oct 12 2020 at 17:27):

Although in that case it's not terribly clear how you get disjointness of constructors.

Dan Doel (Oct 12 2020 at 17:27):

Unless you just add rules for it.

Jonas Frey (Oct 12 2020 at 17:51):

Dan: disjointness of constructors (eg $0\neq 1$) follows from disjointness of coproducts in the pretopos, which is explicitly required in additon to the structure required to interpret coherent logic. Yes, type theoretically it is a consequence of enough (non-propositional) universes using encode-decode, but it should also follow from existence of an impredicative universe of propsitions (toposes can be proven to have disjoint coproducts). I guess I'm still confused about that :-)

Jonas Frey (Oct 12 2020 at 17:56):

Going off on a tangent, it is remarkable that the existence of univalent universes implies a much stronger exactness property: descent. Both disjointness of coproducts and effectivity of quotients is a consequence of descent. But for a category-theoretic formulation of that one has to go to $\infty$-categories, specifically $\infty$-toposes.

Dan Doel (Oct 12 2020 at 18:01):

Isn't that because a type theory with univalence is an $\infty$-something?

Dan Doel (Oct 12 2020 at 18:02):

Anyhow, you only need a very weak classifier to prove disjointness. It just has to classify the empty and singleton types, I think.

Jonas Frey (Oct 12 2020 at 19:50):

Todd Trimble said:

[...] and claims that the assignment $E \mapsto E''$ gives a full embedding into the category of arithmetic pretoposes, lemma 6.15).I haven't studied any of this in detail.

I thought a bit more about these "AU-envelopes" of Skolem theories (AU = arithmetic universe = arithmetic pretopos), and I don't think it's really a full embedding. 6.15 only says "There's a bijective correspondence between morphisms of Skolem theories, and morphisms of AUs of the form $\overline{\overline{E}}$. That sounds more like faithfulness to me, admittedly stated in a slightly awkward way. Anyway, I think if the functor was full in addition to being faithful it would mean that the adjunction between Skolem theories and AU's was a coreflection, and I have trouble believing that right now. But I might be wrong ...

Todd Trimble (Oct 12 2020 at 22:24):

To me it sounded like this: for given Skolem theories $E_1, E_2$, the functorial map $\mathsf{SkolemTheory}(E_1, E_2) \to AU(E_1'', E_2'')$ is a bijection, which I take to be an expression of full faithfulness. I'm not vouching that this statement is correct; I'm just giving my reading.

John Baez (Oct 13 2020 at 00:19):

Next time we'll go further.

Jonas Frey (Oct 13 2020 at 00:42):

Todd Trimble said:

To me it sounded like this: for given Skolem theories $E_1, E_2$, the functorial map $\mathsf{SkolemTheory}(E_1, E_2) \to AU(E_1'', E_2'')$ is a bijection, which I take to be an expression of full faithfulness. I'm not vouching that this statement is correct; I'm just giving my reading.

ahh I see, the "of the form" refers to AU's, not morphisms of AU's. Probably you're right, I'll look into it more closely.

John Baez (Oct 13 2020 at 02:07):

Woo-hoo! Michael Weiss almost taught me how to prove every nonstandard model of PA is "recursively saturated".

• Non-standard Models of Arithmetic 20.

The idea is this: suppose you have an infinite list of predicates in Peano arithmetic: $\phi_1(x), \phi_2(x), \dots,$ and suppose that for any finite collection of these our model of PA has an element $x$ obeying those predicates. Then is there an element $x$ obeying all these predicates?

John Baez (Oct 13 2020 at 02:08):

Of course this isn't true for the standard model of PA: consider the predicates

$x \gt 0, x \gt 1, x \gt 2, \dots$

John Baez (Oct 13 2020 at 02:09):

For any finite set of these we can find a standard number that satisfies them.

John Baez (Oct 13 2020 at 02:09):

But no standard number satisfies all of them.

John Baez (Oct 13 2020 at 02:10):

With Michael's nudging I learned how to show that the answer to the question is "yes" if:

1. the model is nonstandard,
2. you can write a computer program that lists all these predicates $\phi_1(x), \phi_2(x), \dots,$
3. there's an upper bound on the number of alternating quantifiers $\forall \exists \forall \exists \cdots$ in these predicates.

This is summarized by saying "every nonstandard model of PA is recursively $\Sigma_n$-saturated".

John Baez (Oct 13 2020 at 02:11):

This sort of result is interesting because it shows any nonstandard model of PA is "fat" in a certain way, very different from the standard model.

With a further assumption on our nonstandard model we can drop assumption 3.

Morgan Rogers (he/him) (Oct 13 2020 at 07:19):

John Baez said:

The idea is this: suppose you have an infinite list of predicates in Peano arithmetic: $\phi_1(x), \phi_2(x), \dots,$ and suppose that for any finite collection of these our model of PA has an element $x$ obeying those predicates. Then is there an element $x$ obeying all these predicates?

Is "any finite collection" here indexed over the model of PA in question, or over some "standard" model to which the non-standard one is being compared?

André Beuckelmann (Oct 13 2020 at 11:36):

[Mod] Morgan Rogers said:

Is "any finite collection" here indexed over the model of PA in question, or over some "standard" model to which the non-standard one is being compared?

It should be the latter. The notion of a (recursively) saturated model also makes sense for theories that don't have any internal notion of finiteness. There is another reason the "outside" notion of finiteness is the correct one to use: By the compactness theorem, every finite collection being satisfied by some element is the same thing as that collection of predicates being consistent (with the theory of our model). Being recursively saturated, then, just means that everything (sufficiently nice) that is consistent is already satisfied.

Morgan Rogers (he/him) (Oct 13 2020 at 13:43):

So there's some relative arithmetic happening here! I wonder what a model that's recursively saturated with respect to a recursively-saturated non-standard model looks like. Is this property compositional (ie still recursively saturated with respect to the original standard model)? Can two models of PA be recursively saturated with respect to one another?

André Beuckelmann (Oct 13 2020 at 15:17):

That is a good question. On the one hand, you have fewer collections of formulae such that all finite subsets of them are satisfyable, since some infinite subsets are, now, also finite. On the other hand, more of them are going to be recursive. Certainly, $\omega_1$-saturated models (i.e. those satisfying the property for arbitrary countable collections of formulae, not just recursive ones) do have that property. You can, for example, construct them by taking the ultrapower using a nice ultrafilter - just taking your index set to be the natural numbers, together with any non-principle ultrafilter $\mathcal{U}$ should work. The model that gives you is the set of all sequences $(n_1,n_2,...)$ of natural numbers, quotiented by $(n_1,...)\sim (m_1,...) \Leftrightarrow \{i|n_i=m_i\}\in \mathcal{U}$, with component wise successor, addition, and multiplication, and $(n_1,...)\leq (m_1,...)\Leftrightarrow \{i|n_i\leq m_i\}\in \mathcal{U}$. If $n_i$ satisfies $\varphi_1(x),...,\varphi_i(x)$, then $(n_1,n_2,...)$ satisfies all $\varphi_i(x)$.

Edit: Some further thoughts: Depending on how exactly we interpret the question, we might also run into the problem that your non-standard model has a different notion of what a formula even is (since their notion of finiteness is different) - let $\varphi_i$ be (some encoding of) the formula $\exists n_1\exists n_2\exists ...\exists n_i:\text{ something}$, then, by the overspill lemma, our model thinks that $\varphi_n$ is a formula for some non-standard number $n$, but, clearly, there is no way to make sense of this formula in an arbitrary model (unless our model knows about it).

For some formulations of your question, this could lead to trivial answers: If we call collections of formulae $\varphi_1,...$ recursive in our model, only if there is some recursive function $f$ (in the sense of our model) whose range is exactly this collection (and, hence, contains no "non-standard formulae"), then we can only get finite collections - otherwise, by the overspill lemma, again, there should be some non-standard $n$ satisfying $\text{there is some }i\text{ such that the code of }f(i)\text{ is at least }n$, i.e. there would have to be a "non-standard formula". This might be solved, if we allow the range to contain non-standard formulae and simply ignore those, or require that the non-standard formulae are equivalent (in the internal sense) to one of the $\varphi_i$. In the latter sense, you can get $\omega_1$-saturation, as any model of $\neg Con(PA)$ should believe that every formula is equivalent to any other one - the case for models with $Con(PA)$ might be more interesting. No idea, what exactly you will get using the first approach.

John Baez (Oct 13 2020 at 15:48):

Is "any finite collection" here indexed over the model of PA in question, or over some "standard" model to which the non-standard one is being compared?

The standard model. Classical model theory is done in the context of set theory, in this case ZFC set theory, and one can prove there is a standard model, the initial model: an isomorphic copy of this model is contained in every model.

John Baez (Oct 13 2020 at 15:50):

So, for example, recursive saturation lets us do an argument like this (a trivial special case):

For any standard-finite set of the predicates

$x \gt n$

we can find $x$ obeying all the predicates in that set. Therefore in a recursively saturated model of PA we can find $x$ greater than all standard $n$.

If we drop "standard" in either of these two places, the statement becomes false.

John Baez (Oct 13 2020 at 16:00):

I explained this stuff a bit more clearly in my blog article:

• Recursive saturation.

André Beuckelmann (Oct 13 2020 at 16:27):

John Baez said:

For any standard-finite set of the predicates

$x \gt n$

we can find $x$ obeying all the predicates in that set. Therefore in a recursively saturated model of PA we can find $x$ greater than all standard $n$.

If we drop "standard" in either of these two places, the statement becomes false.

I don't think we can even drop the standard in the second place. For some non-standard number $n$, $x\gt n$$ is not a formula in the language of $PA$. We can add all the elements of some particular non-standard model as constants to our language, but then we get different recursively saturated models which may or may not satisfy that property.

John Baez (Oct 13 2020 at 18:24):

I'm not sure what "the second place" was, but you're right, I'm taking $n$ to be standard in $x \gt n$ so this is a predicate in PA. Treating the case where $n$ is nonstandard is beyond my abilities right now!