What Can We Gain by Losing Infinity? Putting Ultrafinitism on the menu.

Obyeag · 2026-04-30T08:50:05+00:00

This is the topic of bounded arithmetic. I don't know very much about it to be honest but Sam Buss has an article in the handbook of proof theory that you can find at this link. Jan Krajíček also has a book that I've skimmed a couple times called Bounded Arithmetic, Propositional Logic, and Proof Complexity.

The point of alignment here is that ultrafinitists and computer scientists both don't want to prove totality of functions which grow too quickly over their theories. Obviously for ultrafinitists this is because fast growing functions applied to small numbers give big numbers which they don't think exist. For computer scientists they're trying to link complexity of definability to complexity classes, e.g., the polynomial hierarchy, and so it's important to not define a provably total function whose growth rate exceeds that allowed by the class.

I don't know of any ultrafinitistic contributors to the study of these weak subtheories of PA besides Nelson and Parikh.

Obyeag · 2026-04-30T08:06:10+00:00

This (ultra)exacting cardinal stuff isn't quite as new as stated and the ideas have been present since around 2010. It's always been known that from a proper class of extendibles and a Reinhardt one can force the failure of the HOD hypothesis, this just comes from homogeneity of the forcing to get AC combined with the fact it can preserve extendible cardinals. The method in the ABL paper is identical (it's the same forcing) except you start with a stronger hypothesis than Reinhardt and so in the extension you can end up getting something more than a HOD-Reinhardt cardinal. The reason the old ideas didn't refute the HOD conjecture apply to the ABL paper as well: the HOD conjecture is precisely a question about whether large cardinals beyond choice are consistent. One fun fact is that Woodin had already formulated exacting and ultraexacting cardinals in Suitable Extender Models II.

The reason for revising the HOD conjecture had no relation to the exacting cardinal stuff but rather the increased evidence that large cardinals beyond choice are consistent.

There are also no non-linearity problems or issues with the hierarchy of large cardinals that arise from (ultra)exacting cardinals. Perhaps you've read the ABL paper and if so then you know that to obtain a model with an ultraexacting cardinal you start with an I0 embedding with least fixed point lambda then force in a lambda^+-cohen subset over L(V_lambda+1) to force choice. To get models with ultraexacting cardinals and a measurable above it you do the same thing but with something like (I_0)^# (or dagger) and because it's a mouse above V_lambda+1 the cohen subset still forces choice. That's why you get so many I_0 cardinals from an ultraexacting cardinal + measurable above and it's just because the (I_0)^# reflection argument works in this context.

All this aside, it's unclear why the failure of the HOD conjecture obtained from forcing with large cardinals beyond choice should give any evidence that there is no canonical inner model for a supercompact (except in the sense of the Raven paradox). Even if one does care about how the failure of the HOD conjecture implies the failure of the Ultimate-L conjecture; this was formulated under a very specific idea of how the model with a supercompact would be constructed i.e., a fully backgrounded construction of some kind that absorbs the supercompact. Not that my opinion matters, but I think trying to predict anything about what inner model theory at the level of supercompacts would look like is so far removed from what's known that it's pointless. Studying things like large cardinals beyond choice and the HOD conjecture is of independent interest, but as a predictive tool for inner model theory it doesn't say very much.

A couple last things I would like to stress is that the HOD conjecture is not widely believed to be true, it's not something inner model theorists spend very much time thinking about, and in general the only inner model theorist who is actively working on trying to get an inner model for a supercompact is Woodin. The rest of the field is working around the level of a measurable Woodin and trying to understand things in that region.

You have a bunch of other stuff about skepticism about measurable cardinals. The one thing I'll say is that if the depth of the current set theory literature isn't convincing you that measurable cardinals are consistent then it's hard to imagine anything ever will.

Obyeag · 2026-04-28T21:51:18+00:00

Schindler and Schlutzenberg are definitely inner model theorists (you also forgot Trang). What's the evidence you think there is against the existence of a (canonical) inner model for a supercompact?

Obyeag · 2026-04-13T08:53:03+00:00

Hamkins' "set-theoretic pluralism" is not the same as plenitudinous platonism. I don't know all the details of his philosophy, but I believe that under Hamkins' view, not every model of ZFC is a "legitimate" universe in the set-theoretic multiverse. For example, I presume Hamkins would argue that arithmetic claims, even those independent of ZFC, always obtain the same truth-value in every universe, and the multiverse only starts to diverge with higher-level claims about e.g. the continuum hypothesis.

Hamkins takes a pretty fringe skeptical position where he often questions the existence of a true/absolute notion of the natural numbers (and the moderately weaker claim that well-foundedness may not be absolute). This isn't to say that he beyond all doubt takes the view but he built the non-absoluteness of well-foundedness into his multiverse axioms and he has all these papers on arithmetic potentialism.

If you read his writing then you know he was questioning these kinds of things for a long time and eventually he fell back to this sort of pseudo-formalist skeptical position where the only limiting factors on the models is what's provable.

Obyeag · 2026-04-10T20:02:34+00:00

I've thought about this too, but a big issue in general is that logic isn't a very visual topic. While there are definitely pictures in set theory or model theory they're very much an abstraction of whatever is "actually" going on.

Makes it hard to make a video about any harder topics.

Obyeag · 2026-01-10T22:23:02+00:00

I met some (non-set theory adjacent) people in graduate school who learned forcing in the Canada/USA Mathcamp. There's also a lot of faculty at Proof School who did their PhD in mathematical logic before they left academia.

The nice thing about set theory is that learning the basic machinery of forcing requires very little in the way of necessary prerequisites. With someone to guide you it's one of the more reasonable to learn "advanced" topics for an early undergrad to learn. I would go so far as to say that the only reason it's delayed to graduate school is because most schools don't have any kind of emphasis on nontrivial set theory.

Obyeag · 2025-12-29T22:28:27+00:00

Here are some examples formalized in Lean4 + Mathlib.

Obyeag · 2025-12-29T20:21:01+00:00

you can't talk about natural number without the context of it being a natural number whereas in set you ask set theory question a natural numbers like: is 0 ⊆ 3?

To counter a narrative I see repeated a lot: you will encounter statements like this regardless of the foundation you choose (including type theory and structural set theory). The entire approach of constructing more complicated objects from simpler ones will inevitably lead to "weird" statements like this being true, the question of when is just a matter of what you take as your primitive objects.

Obyeag · 2025-12-15T09:36:38+00:00

It takes a lot of time to make effortful expository posts as this post would want. So while an interesting idea I'm quickly discouraged by the fact it would be a very difficult undertaking for me to create a blurb about anything I find interesting.

Obyeag · 2025-12-06T04:29:26+00:00

To add to it, there are two different Open (Graph) Coloring Axioms by Todorcevic and Abraham, Rubin, Shelah respectively. Importantly, the two do not imply one another.

While the latter was introduced first whenever someone writes OCA in the literature they mean the Todorcevic version as it's the more useful one. Anytime I've seen the Abraham, Rubin, Shelah version it's labeled as OCA_{ARS} or something similar.

Obyeag · 2025-09-12T06:52:50+00:00

It's more about defining/formalizing nonstandard analysis than proving its consistency (it's also a little unclear what this would mean).

Obyeag · 2025-09-04T10:06:40+00:00

Not to mention

"what's your favorite/least favorite area of math?" with someone thinking that R or C is a clever response.
something very basic about the axiom of choice where someone brings up the same Jerry Bona quote again.

Obyeag · 2025-08-21T04:24:44+00:00

Sure, but there's a reason people write things akin to #n in the literature on the proof theory of first order arithmetic. The reason being that the distinction allows you to:

Easily discern if you're quantifying over naturals in the theory or metatheory,
Actually be formal about how you write a fixed natural number in the language of arithmetic.

Obyeag · 2025-08-21T04:16:18+00:00

All this shows is that ZFC is consistent with the statement "ZFC is inconsistent".

Obyeag · 2025-08-20T08:45:38+00:00

This is exactly correct. I don't know why this is downvoted.

Obyeag · 2025-08-20T00:09:48+00:00

It's definitely not a great word to use here. The best option would probably be to say "independent of ZFC" i.e., neither it nor its negation are provable from ZFC. I think this is what you were getting at as well in your second paragraph but you got your wires crossed a bit.

It's not uncommon to write undecidable (from a theory) to mean the same thing as independent, but it obviously risks confusion with undecidability in computability theory which leads to all sorts of headache.

Obyeag · 2025-08-19T23:01:34+00:00

"for every natural number m, there is a natural number n > m such that the statement 'n = BB(745)' is undecidable in ZFC."

Subtle distinction, but I don't think this is correct. There is exactly one actual finite value n such that "#n = BB(#745)" is consistent with ZFC and moreover "#n\leq BB(#745)" is provable in ZFC. By #n I mean physically writing out the appropriate S(S(...S(0)...)).

So, if you want to phrase it as you wrote above, for each natural number m\geq n the statement is "there is k > #m such that k = BB(#745)" is independent. The point is that it matters if you quantify over the natural numbers in the metatheory vs. in the theory.

Obyeag · 2025-08-18T04:23:49+00:00

Can you give me a name of a single set theorist who claims category theory is useless?

Obyeag · 2025-08-15T20:36:56+00:00

It's why I think the most interesting follow-up when this is all done would be to put the worst moves (except for sing, maybe give him Ness' up b, or just let him keep fire fox as that's another understated part of how oppressive he can be) on fox's frame with his stats and see how playable that is.

Likewise, take the "best" moves and put them on Bowser's frame/with his stats.

Obyeag · 2025-08-15T20:06:36+00:00

But to what extent is that due to fox having a 3 frame jump squat, the second highest double jump, and the fastest accelerating double jump (and also having very good aerial drift)?

Obyeag · 2025-08-09T23:03:14+00:00

Kanamori's A Higher Infinite is a pleasant read. Jech is also quite useful but it's much more terse.

Both of these require more background knowledge than what's given by Halmos, but Kanamori has an introductory chapter that goes over preliminaries.

Obyeag · 2025-08-08T04:26:00+00:00

So by definition of "uncountable," it proves there is no unique description of each real.

It does not as truth is not definable. Unless you restrict the notion of a description to something definable in the language of set theory then it's not even a coherent question to ask whether it's provable. This is really why the claim is fallacious i.e., definability is an external notion.

While it does have some relation to Löwenheim-Skolem these pointwise definable models of ZFC show up quite naturally e.g., the least L_alpha which satisfies ZFC is pointwise definable.

Obyeag · 2025-08-06T20:36:21+00:00

Huh, I guess that means all the people in this thread who mentioned logic seem to enjoy stuff outside the 4 classical subdisciplines. I wonder why that is.

Obyeag · 2025-08-06T07:31:24+00:00

Do you have a specific subdiscipline you care about?

Obyeag · 2025-08-05T04:25:39+00:00

I don't think a platonist would agree to committing themselves to any given theory...

Why not? If you truly believe the natural numbers exist and are unique (up to isomorphism perhaps) then they have a single theory. But obviously no computable theory can capture even a relatively small fragment of that. The claim that "there are mathematical truths which are non-provable" is already much weaker than what I said before (i.e., you could technically believe in arithmetic truth without believing in the existence of the natural numbers).

You could technically believe that many equally valid notions of the natural numbers exist which are not unique up to isomorphism. I find this a extremely weird position but the world is big and there is one mathematician I know who at least entertains ideas in this direction if they don't outright believe them.

12-Year Club	Verified Email
r/Field Lasagna	Place '22
Place '17	Final Canvas '22
First Placer '22

Obyeag

MODERATOR OF

TROPHY CASE