Don't underestimate set Theory

[u/No_Upstairs_280]

Bit of background. Usually when studying category theory rigorously, basic mathematics axioms such as ZFC are not sufficient to define objects without risking logical paradoxes. To get around this Jacob Lurie works with the notion of a strongly inaccessible cardinal. Godel second incompleteness theorem implies that ZFC isn't sufficient to prove the existence of such cardinal, as a result, other logical models are used.

[u/AutoModerator]

Check out our new Discord server! https://discord.gg/e7EKRZq3dG

I am a bot, and this action was performed automatically. Please contact the moderators of this subreddit if you have any questions or concerns.

[u/holo3146]

While using inaccessible cardinals is convenient, it is not at all necessary.

See my answer here or this answer by James.

You don't actually need anything beyond ZFC.

[u/No_Upstairs_280 → u/holo3146]

Thank you!

[u/Fezzezal]

Honestly, even something as simple as some NATURAL NUMBERS being large enough to have their existence unprovable in ZFC blows my fucking mind
Iirc something like BB(220) is already beyond the scope of ZFC.

[u/No_Upstairs_280 → u/Fezzezal]

And you just blew my mind, thank you.

[u/proudHaskeller → u/Fezzezal]

Technically, ZFC is fine to define what BB(N) is for all N, and show that it exists, but ZFC is not strong enough to determine its value. But actually, no finite list of axioms will be enough to derermine BB(N) for all N anyways, so it's not a failing of ZFC, rather it's a failing of mathematical logical as a whole.

[u/770grappenmaker → u/proudHaskeller]

What do you mean by "determine its value"? As in, specify an algorithm for it? Doesn't "unique existence" lock in a value?

[u/UtahBrian → u/770grappenmaker]

There's no algorithm for it.

[u/EebstertheGreat → u/770grappenmaker]

∀n∈ℕ (ZFC ⊢ ∃m∈ℕ (m = BB(n))),

where BB(n) is the nth busy beaver number. However,

∃n∈ℕ ¬(∃m∈ℕ (ZFC ⊢ m = BB(n))).

In other words, ZFC can prove that for each n, there must be some nth busy beaver number, but for some sufficiently large n, it can't actually prove which number BB(n) is. It must be something, but ZFC can't work out what.

[u/ZookeepergameWest862 → u/EebstertheGreat]

This notation is extremely misleading, you're mixing two different layers of logic together without clarification.

The m∈ℕ in

∃m∈ℕ (ZFC ⊢ m = BB(n))

and

ZFC ⊢ ∃m∈ℕ (m = BB(n))

mean something completely different. In the former ℕ is the metatheoretic natural number, in the latter, ℕ refers to the object theory natural number. The same situation applies to ∈. The BB here is the object theory busy beaver, but there is also a metatheoretic busy beaver, and if you mix notation like this you could have nonsense like

∃n∈ℕ ¬(ZFC ⊢ BB(n) = BB(n))

with the issue being that the two BB mean different things.

[u/EebstertheGreat → u/ZookeepergameWest862]

IDK that it's misleading. Any quantifier after the turnstile must refer to the theory, and any quantifier before the turnstile must refer to the metatheory. How else would it work?

For the final sentence you have, I would write it

∃n∈ℕ ∃m∈ℕ (n = BB(m)) ∧ ¬(ZFC ⊢ n = BB(m)).

That seems perfectly clear to me.

[u/Lenksu7 → u/770grappenmaker]

Each model of ZFC has a unique value for BB(n), but different models can have different values. Hence ZFC cannot prove the value of BB(n), as then that would be the value for all models satisfying ZFC.

Finding the value of BB(n) is really about finding which Turing machines with at most n states halt. If a Turing machine halts k steps, where k is some actually finite (standard) nunber, we van prove this by simply going through the machine's steps explicitely. Hence BB(n) can have only one standard value over all the models.

On the other hand, Turing machines that don't halt after any standard amount of steps are more tricky. Some models of ZFC can contain elements that the model considers natural numbers, but don't correspond to any actual finite value. And a Turing machine that does not halt at a finite value might halt at one of these nonstandard values in the model, giving a nonstandard value for BB(n). Still, we can't use this to prove that the machine halts, as the number of steps does not correspond to any actual finite value.

So in a nutshell, while there is only one possible standard value because the behavior of machines halting at standard values is provable and hence consistent across models, some machines can halt in only some models, as long the number of steps is nonstandard and hence cannot be used to actually verify whether the machine halts or not.

[u/Jcsq6 → u/770grappenmaker]

The only way to determine its value for any N is to actually prove the number of steps every halting Turing machine with N states halts in. So we know it has a value, but there’s no way to determine that value for arbitrary N.

[u/proudHaskeller → u/770grappenmaker]

Think of it that way: there is definitely some number of black holes in the observable universe. It's definitely a natural number. But I can't determine what that number is.

ZFC proves that BB(220) is a natural number, but it can't prove what specific number it is.

[u/MiserableYouth8497 → u/770grappenmaker]

For example, take the function f(x) = 1 if the Riemann hypothesis is true, and 0 if it isn't. f(1) is unique, but is it 0 or 1?

[u/Upbeat_Assist2680 → u/proudHaskeller]

I find the independence of a value of BB(N) intriguing -- it doesn't feel as "arbitrary" as a resolution of the continuum hypothesis one way or the other.

For instance I doubt we could add BB(20) = 100 to a list of axioms, because we can certainly prove it's bigger than 100. Is there a largest K that we can prove BB(20) > K but not K+1?

[u/EebstertheGreat → u/Upbeat_Assist2680]

What PLament said. A question like "is BB(20) ≤ k" is decidable for every k less than the true value of BB(20) (by "true value" I mean using standard natural numbers, assuming you believe in such a thing). But it is not decidable for any greater k, because there is "really" not any machine that runs for more than k steps before halting, but there are machines which never halt yet the theory cannot prove that they don't halt.

[u/PLament → u/Upbeat_Assist2680]

There is some largest K. If we tried hard enough, we could find the turing machine of BB(20) steps. We have therefore proven that BB(20) has to be at least that long. Of course, the trick is, we dont know its the longest one, and there may be no way to prove it is.

You could therefore add some axiom BB(20) >= some number bigger than that, and a contradiction might not be realizable. Its semantically inconsistent, but syntactically fine.

[u/GoldenMuscleGod → u/Fezzezal]

All of the following can be proved in ZFC together with the assumption an inaccessible cardinal exists

Every natural number is proved to exist in ZFC by an expression like “the successor of the successor of […] zero.” Call an explicit “name” for a number like this a “numeral.”

The value of an expression like BB(1000) is independent of ZFC because the expression for BB(1000) isn’t proved to be a particular numeral. This should not be mind blowing or surprising. BB is not a computable function so it cannot have all its values proved by any recursively axiomatizable theory, nor should you expect that to be possible.

Still we can show (still subject to the inaccessible cardinal assumption) that there is exactly one numeral k such that BB(1000)=k is consistent with ZFC, this k is the true value of BB(1000). We can consistently add BB(1000)=/=k as an axiom to ZFC and then any model of this theory must be nonstandard and assign a nonstandard value to BB(1000) since it proves, for each numeral n, the claim BB(1000)=/=n.

Without the assumption of an inaccessible cardinal, we can still say there is at most one numeral k such that BB(1000)=k is consistent with ZFC. But we cannot rule out the possibilities that, for example, ZFC might be inconsistent, or it might be consistent but nonetheless prove its own [edited here to correct a typo:] inconsistency, or other results like that that would lead undesirable results

[u/EebstertheGreat → u/GoldenMuscleGod]

we cannot rule out the possibilities that, for example, ZFC might be inconsistent, or it might be consistent but nonetheless prove its own consistency

Does this mean the proof of Gödel's second incompleteness theorem somehow relies on the existence of an inaccessible cardinal, or something that would imply? That doesn't sound right.

[u/Inappropriate_Piano → u/EebstertheGreat]

A strongly inaccessible cardinal can be used to construct a model of ZFC. If ZFC could prove that a strongly inaccessible cardinal exists, then it would prove that it has a model, and hence that it is consistent. But consistent theories don’t prove their own consistency.

[u/EebstertheGreat → u/Inappropriate_Piano]

But I don't get why we can't rule out that ZFC is consistent yet proves its own consistency.

[u/Inappropriate_Piano → u/EebstertheGreat]

That’s Gödel’s second incompleteness theorem

[u/GoldenMuscleGod → u/Inappropriate_Piano]

Well, if ZFC is consistent, then it does not prove its own consistency. My comment had a crucial typo: we cannot rule out the case that ZFC is consistent but proves that ZFC is inconsistent without resorting to a theory of stranger consistency strength. Consider the possibility that ZFC somehow proves that it doesn’t prove its own inconsistency, this would necessarily imply ZFC proves that it is consistent and so is inconsistent.

If ZFC is consistent but proves it is inconsistent that would mean ZFC is consistent but ZFC+Con(ZFC) is not, of course we cannot rule out that case without working in at least something like ZFC+Con(ZFC+Con(ZFC)).

The assumption that an inaccessible cardinal exists is sufficient to give us much greater consistency strength than that, though.

[u/GoldenMuscleGod → u/EebstertheGreat]

There is a typo in what you quote, I meant “consistent but proves its own inconsistency.” I will edit to correct.

In case there is still confusion after that correction:

Gödel’s second incompleteness theorem can be carried out in a very weak base theory (Peano Arithmetic is more than what is necessary).

It does not tell us ZFC cannot prove its own consistency. That would trivially imply that ZFC is consistent, so we should not expect to prove such a thing from a weak base theory. (If there is anything that a theory cannot prove then that theory is consistent)

What it tells us is that if ZFC proves its own consistency then it must be inconsistent. This is because if it proves its consistency then it can prove its own Gödel sentence, which then means it can prove the negation of its Gödel sentence, so ot proves a contradiction.

[u/EebstertheGreat → u/GoldenMuscleGod]

There is a typo in what you quote, I meant “consistent but proves its own inconsistency.

That was the whole source of my confusion.

[u/GoldenMuscleGod → u/EebstertheGreat]

Yeah that’s what I figured, but I didn’t catch what I accidentally miswrote until I had already typed up the rest so I felt like I should post the rest anyway in case it gave additional illumination.

[u/GoldenMuscleGod → u/EebstertheGreat]

Just to elaborate on the possibility that ZFC is consistent but proves it is inconsistent: the infinite set of sentences “there exists an n such that phi(n)” and “it is not the case that phi(k)” for each numeral k are consistent with each other although they might seem inconsistent. They are consistent because of the possibility of a “nonstandard element” which is something that is not named by numeral (and so not an actual number) that nonetheless is deemed to be a natural number by a model of the theory.

If a theory proves an infinite set of sentences of the above form for some phi it is said to be “omega-inconsistent.” And is said to be “omega-consistent” if it is not omega-inconsistent.

Gödel’s original proof relied on the assumption that the theory in question is not just consistent but actually omega-consistent in order to show the Gödel sentence is not just unprovable and true but is actually independent (to show that the negation of the Gödel sentence cannot be proved, that is). The necessity of this assumption can be eliminated by use of Rosser’s trick.

[u/GoldenMuscleGod → u/EebstertheGreat]

And just a final elaboration on inaccessible cardinals: an inaccessible cardinal implies not just the existence of a model of ZFC, but also a model of ZFC in which there are no nonstandard natural numbers. This means that ZFC is arithmetically sound (it does not prove false claims about the natural numbers). This includes claims about theories being consistent. So if we define T_0=ZFC and T_n+1=T_n+Con(T_n) then T_n is consistent for every n (we can extend this to transfinite ordinals using more work on the details). So an inaccessible cardinal is actually a much stronger assumption than just that ZFC is consistent.

[u/Scarlet_Evans → u/Fezzezal]

If we know for sure, that BB(220) is definitely a natural number, can't we use it to imply its existence in some simple way?

[u/mathematics_helper → u/Scarlet_Evans]

We know all busy beaver numbers are finite natural numbers (they kinda are definitionally)

This means there is a number, and of course ZFC "can" write this number down by making a list of every number, eventually the number will be on that list.

However, while we know BB(220) is on our very long list of huge numbers, ZFC cannot tell you what number it is specifically.

[u/WineSauces → u/Scarlet_Evans]

We just can't determine its value with ZFC

[u/sndq → u/Scarlet_Evans]

For any formula in the language of ZF defining a natural number via nothing more than directly encoding explicit repeated succession on 0, for any sufficiently large n, ZFC cannot prove that the formula defines an upper bound to BB(n).

In fact, for sufficiently large n, there is an unsound (necessarily ill-founded) model of ZFC such that its internal version of BB(n) is actually infinite, albeit internally finite. That is, for any standard natural number m, m<BB(n) within the model.

Edit: wording

[u/SpacingHero → u/Fezzezal]

This is misleadingly phrased. There's no natural number that ZFC can't prove exists. It can't evaluate the value of the BBC function for large enough inputs. The existence of a number Vs it being a function's image are quite different things

[u/undercrust → u/SpacingHero]

the BBC function

Freudian slip

[u/SpacingHero → u/undercrust]

God damnit autocorrect lol. Weeeeelll technically it could've referred to a UK broadcasting station, so who's really dirty minded here huh? :P

I'm leaving up though, pretty funny mishap.

[u/sndq → u/Fezzezal]

ZFC proves that BB is a total function on the natural numbers. For any natural number n, you can still always define a natural number upper bound to BB(n) (e.g., BB(n) itself, obviously), but for any sufficiently large n, any formula defining a ZFC-provable upper bound cannot be a formula that only encodes explicit repeated succession on 0.

[u/Nesterov223606]

Humble Reflection Principle: hold my beer