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 https://github.com/metamath/set.mm/issues/2579#issuecomment-1099532847 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.