With the exception of a few miscellaneous cases, the axioms (and/or schemeta) of ZFC can roughly be divided into two kinds:

1. Those that guarantee the existence of more complicated sets, given that simpler sets are already around (e.g. separation, replacement schema). Also, uniqueness of these entities immediately follows, which is very satisfying.

2. Those that guarantee the existence of larger sets, given that smaller sets are already around (e.g. powerset, union).

Of course, this is a gross oversimpification (e.g. replacement is needed to prove the existence of $\beth_\omega,$ a kind of "large" cardinal, albeit a very small one). Anyway, the point is that we can also apply the above categorization scheme to $\in$-sentences that aren't theorems of ZFC, especially to proposed axioms for set theory. In particular, large cardinal axioms are (by definition) of the latter variety.

Question. Have any axioms or axiom schemata of the former variety (i.e. those guaranteeing the existence of more complicated sets) been proposed or otherwise considered?

I'm especially interested in:

• axioms and/or schemata that legitimize non-mainstream ways of defining and/or constructing things. For example, I'd be interested to hear of a schema asserting that certain definable (proper-class) functions always have greatest and/or least fixed points. Or an axiom asserting that a particular class of self-referential definitions do indeed define unique functions. etc.

• axioms or axiom schemata that guarantee not only the existence of entities, but also their uniqueness. For example, I don't really consider Martin's axiom to be an example of the kind of axioms I'm looking for, since it doesn't guarantee uniqueness, which makes it hard to take seriously the "genuine" existence of the kinds of entities that are posited to exist.

With the exception of a few miscellaneous cases, the axioms (and/or schemeta) of ZFC can roughly be divided into two kinds:

1. Those that guarantee the existence of more complicated sets, given that simpler sets are already around (e.g. separation, replacement schema). Also, uniqueness of these entities immediately follows, which is very satisfying.

2. Those that guarantee the existence of larger sets, given that smaller sets are already around (e.g. powerset, union). These also tend to satisfy uniqueness properties; in particular, powersets and unions are indeed unique.

Of course, this is a gross oversimpification (e.g. replacement is needed to prove the existence of $\beth_\omega,$ a kind of "large" cardinal, albeit a very small one). However, the point is that we can also apply the above categorization scheme to $\in$-sentences that aren't theorems of ZFC, especially to proposed axioms for set theory. In particular, large cardinal axioms are (by definition) of the latter variety.

Question. Have any axioms or axiom schemata of the former variety (i.e. those guaranteeing the existence of more complicated sets) been proposed or otherwise considered?

I'm especially interested in:

• axioms and/or schemata that legitimize non-mainstream ways of defining and/or constructing things. For example, I'd be interested to hear of a schema asserting that certain definable (proper-class) functions always have greatest and/or least fixed points. Or an axiom asserting that a particular class of self-referential definitions do indeed define unique functions. etc.

• axioms or axiom schemata that guarantee the existence of entities whose uniqueness can then be proved (or which assert not only existence but also uniqueness). For example, Martin's axiom does not have this property.

With the exception of a few miscellaneous cases, the axioms (and/or schemeta) of ZFC can roughly be divided into two kinds:

1. Those that guarantee the existence of more complicated sets, given that simpler sets are already around (e.g. separation, replacement schema).
2. Those that guarantee the existence of larger sets, given that smaller sets are already around (e.g. powerset, union).

Of course, this is a gross oversimpification (e.g. replacement is needed to prove the existence of $\beth_\omega,$ a kind of "large" cardinal, albeit a very small one). Anyway, the point is that we can also apply the above categorization scheme to $\in$-sentences that aren't theorems of ZFC, especially to proposed axioms for set theory. In particular, large cardinal axioms are (by definition) of the latter variety.

Question. Have any axioms or axiom schemata of the former variety (i.e. those guaranteeing the existence of more complicated sets) been proposed or otherwise considered?

I'm especially interested in axioms and/or schemata that legitimize non-mainstream ways of defining and/or constructing things. For example, I'd be interested to hear of a schema asserting that certain definable (proper-class) functions always have greatest and/or least fixed points. Or an axiom asserting that a particular class of self-referential definitions do indeed define unique functions. etc.

To clarify what I'm looking for a little: I don't really consider Martin's axiom to be an example of the kind of axioms I'm looking for, since it doesn't guarantee uniqueness. I really want not just existence, but also uniqueness, so that the constructed entities can feel like legitimate constructions, as opposed to these very exotic things that are very hard to imagine.

With the exception of a few miscellaneous cases, the axioms (and/or schemeta) of ZFC can roughly be divided into two kinds:

1. Those that guarantee the existence of more complicated sets, given that simpler sets are already around (e.g. separation, replacement schema). Also, uniqueness of these entities immediately follows, which is very satisfying.

2. Those that guarantee the existence of larger sets, given that smaller sets are already around (e.g. powerset, union).

Of course, this is a gross oversimpification (e.g. replacement is needed to prove the existence of $\beth_\omega,$ a kind of "large" cardinal, albeit a very small one). Anyway, the point is that we can also apply the above categorization scheme to $\in$-sentences that aren't theorems of ZFC, especially to proposed axioms for set theory. In particular, large cardinal axioms are (by definition) of the latter variety.

Question. Have any axioms or axiom schemata of the former variety (i.e. those guaranteeing the existence of more complicated sets) been proposed or otherwise considered?

I'm especially interested in:

• axioms and/or schemata that legitimize non-mainstream ways of defining and/or constructing things. For example, I'd be interested to hear of a schema asserting that certain definable (proper-class) functions always have greatest and/or least fixed points. Or an axiom asserting that a particular class of self-referential definitions do indeed define unique functions. etc.

• axioms or axiom schemata that guarantee not only the existence of entities, but also their uniqueness. For example, I don't really consider Martin's axiom to be an example of the kind of axioms I'm looking for, since it doesn't guarantee uniqueness, which makes it hard to take seriously the "genuine" existence of the kinds of entities that are posited to exist.