Extensible structures whose components are proper classes?

[zwang123]

Is it possible to define extensible structures whose components are proper classes (e.g., large categories)?

The current definition is incompatible with such structures presumably due to the fact that a proper class cannot be included in an ordered pair. However, I envision that this might be resolved by putting the elements of the proper classes into the ordered pair instead. For example, instead of

$$ \{ \langle1, {\color{purple} B} \rangle, \langle ;14,{\color{purple} H} \rangle, \langle ;15, {\color{purple} O} \rangle \} $$

being an extensible structure, why don't we have

$$ (( \{ \langle 1, {\color{red} b} \rangle| {\color{red} b} \in {\color{purple} B} \} \cup \{ \langle ;14, {\color{red} h} \rangle| {\color{red} h} \in {\color{purple} H} \} ) \cup \{ \langle ;15, {\color{red} o} \rangle| {\color{red} o} \in {\color{purple} O} \} ) $$

or equivalently

$$ ((( \{ 1 \} \times {\color{purple} B} ) \cup ( \{ ;14 \} \times {\color{purple} H} )) \cup ( \{ ;15 \} \times {\color{purple} O} )) $$

defined as an extensible structure? The definition change might necessitate a large amount of changes, for example, the new slot function should be

$$ \mathrm{Slot} {\color{purple} A} = ({\color{red} x} \in \mathrm{V} \mapsto ({\color{red} x}``{\color{purple} A})) $$

But I assume construction-agnostic theorems do not need adjustments? (For example, one does not want theorems on complex numbers depend on the construction from ZF)

Note: I saw a thread of discussions elsewhere but I am not sure whether this was going any further.

(Also, I am confused why empty set is allowed as an element of an extensible structure...)

[tirix]

I think the relevant thread of discussion is this one: #2579 .
Basically, categories ( Cat ` U ) are relative to a universe U:

To handle large categories, we relativize to a set U and have U-small and U-large categories. I defined "weak universes" in set.mm as a universe-like concept (a set closed under lots of operations) such that ZFC can prove the existence of a proper class of them. In most cases you can work with Set(U) for any set U, but if you need any closure conditions you can restrict to weak universes. You will need to be doing some rather advanced stuff to actually need Tarski-Grothendieck universes, but ax-groth is there if you need it.

[metakunt]

Now that I think about it #2579 (comment)
How do we know that Tarski-Grothendieck is relatively consistent to ZFC?
I have tried searching for it but could have found no result.

[tirix]

As the comment mentions, that's what the Tarski-Grothendieck axiom is for.
The TG axiom extends ZFC to grant the existence of even more sets.

[metakunt]

Yeah, I am aware of that.
The comment mentions the following:

In any case, the category of all U-small categories is not U-small: you have to "climb the ladder" and need another universe V such that P(U) \in V (or something close to that), and then the category of all U-small categories is V-small. This is why the Tarski--Grothendieck axiom is often assumed for convenience, since it is relatively consistent with ZFC.

I am not aware of a proof that Tarski-Grothendieck is relatively consistent to ZFC. I assumed that the existence of inaccessible cardinals allows to prove the consistency of ZFC and by Gödel, we can't prove that ZFC+TG is relatively consistent to ZFC.

[benjub]

I am not aware of a proof that Tarski-Grothendieck is relatively consistent to ZFC. I assumed that the existence of inaccessible cardinals allows to prove the consistency of ZFC and by Gödel, we can't prove that ZFC+TG is relatively consistent to ZFC.

You're right, we should remove that part of the comment.

[tirix]

Oh, sorry, I did not understand you were referring to the comment.
I guess the statement that TG is consistent with ZFC is from @digama0, maybe he has some pointers?

Otherwise yes, simplest action is to remove that part.

[benjub]

Or you can fix the comment by writing:

... since it is relatively consistent (actually, equiconsitent) with ZFC with a proper class of (strongly) inaccessible cardinals.

[metakunt]

Yeah, but I guess my point is that ZFC+existence of a proper class of inaccessible cardinals is not equiconsistent to just ZFC alone.

I always wonder why inaccessible cardinals are useful to add to ZFC.

[benjub]

Yeah, but I guess my point is that ZFC+existence of a proper class of inaccessible cardinals is not equiconsistent to just ZFC alone.

Yes, which is why I proposed to either remove this from the comment, or to replace it with the correction above.

I always wonder why inaccessible cardinals are useful to add to ZFC.

They make it possible to iterate constructions such as "take the category of all U-small..." without worrying about size issues. Basically, they provide nested models of ZFC.

Even though they cannot be proved consistent from ZFC, it would seem arbitrary to outright forbid such sets, and their study lead to interesting results.

I know close to nothing about large cardinals, but it shouldn't be hard to find more profound motivation for their study, beginning with wikipedia and its references, or anything Kanamori.

[jkingdon]

(Also, I am confused why empty set is allowed as an element of an extensible structure...)

This strikes me as an odd decision as well. The explanation is at https://us.metamath.org/mpeuni/df-struct.html and it has to do with whether the payload classes are known to be sets (not so much whether using a proper class does anything useful, more just which theorems need some kind of sethood hypothesis).

In iset.mm we need the sethood hypotheses anyway, so among other consequences this decision adds to the divergence between set.mm and iset.mm on extensible structures (divergence isn't bad in all circumstances, but this one seems like a technical detail more than anything which gets at the heart of what excluded middle does).

There's a decent amount of discussion at #3008 although I think it touches on the empty set question only in passing.

[digama0]

Oh, sorry, I did not understand you were referring to the comment. I guess the statement that TG is consistent with ZFC is from @digama0, maybe he has some pointers?

Otherwise yes, simplest action is to remove that part.

Belated response to this: Yes, the comment is nonsense, TG has strictly more consistency strength than ZFC, so it is relatively consistent with ZFC iff it is consistent outright.

[metakunt]

I don't understand that one. Is it possible that ZFC is consistent, while ZFC+TG is not?
I always assumed that ZFC+TG shows that ZFC is consistent, but this leaves still the possibility that TG makes ZFC inconsistent.
I never could find any good literature on that except the fact that both lean4 and HOL use inaccessible cardinals in some sense.
Also I never could even find one useful lemma or proof sketch that illustrates the usefulness of TG, which makes it even weirder that it is an axiom in any popular interactive theorem prover

[digama0]

Yes, it is possible, although I don't think they are particularly different in terms of people's quick takes on whether it is a reasonable axiom system to assume (except that not many people know about TG).

The origin of metamath's TG axiom is actually from Mizar, which is based on TG set theory and uses the TG axiom to prove several of the other laws of ZFC (IIRC choice and replacement follow from it), so it really is baked into the foundations of the library. Lean 4 uses a weaker assumption, of omega many inaccessibles instead of a proper class of inaccessibles, and HOL has no inaccessible assumptions and indeed has a model in $V_{\omega 2}$, much weaker than ZFC.

The usual justification for TG stems from needing Grothendieck universes for doing category theory, and TG suggests itself when you want to do that in set theory. I don't believe this justification is bogus, but you need to be doing somewhat advanced category theory for the requirement to arise, and set.mm currently has a scheme which avoids the need for TG as long as you don't have too strong requirements on the category of sets. So currently ax-groth is basically vestigial, there was a successful effort to remove it as a dependency of essentially all of main set.mm and no one is doing the kind of work that would need it.

[jkingdon]

Also, if the whole concept of Grothendieck universes is hard to get your head around, I'd suggest a talk by Andrej Bauer and Mario Carneiro: https://mathstodon.xyz/@andrejbauer/112515353890527954 and https://www.youtube.com/watch?v=f4yYkuTMoLw

Whether that talk is the best way to get a handle on it probably depends on your mathematical background, but at least for me it was at roughly the right level.

[metakunt]

Ah ok, thank you very much. I have watched the video.

Quick summary as far as I've understood:

• Sometimes it is useful to have certain closure condition that lead to Grothendieck universes
• TG is a good axiom that allows for the modeling of Grothendieck universes
• Lean has universes, but not necessarily TG
• Universes in Lean just make sure that arbitrary definitions are well-formed

I guess regarding metamath, the existence of Grothendieck universes implies sethood right. Did I understand that correctly? For example given a class that contains $$\mathbb{N}$$ and dependent $$\Pi$$-types I can substitute the class for values where I need sethood. Also I could also in principle construct this set and use it in theorems that need sethood or quantify over it.

For example in this theorem
https://us.metamath.org/mpeuni/sticksstones12a.html I needed sethood to use fvmptd. I assume with the existence of inaccessible cardinals I can define those maps, prove that they exist and compute values in theory.