# Have axioms / axiom schemata of this flavour been proposed or otherwise considered?

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.

-
You set up uniqueness as part of the distinction, but in the examples you give of type (2) (Union and Powerset), the sets asserted are unique; and one of your examples for (1), Replacement, is often given in a equivalent form (Collection) which does not satisfy uniqueness. –  Peter LeFanu Lumsdaine Apr 20 at 13:40
@PeterLeFanuLumsdaine, okay but what are you getting at? –  goblin Apr 20 at 14:16
Do you consider noncanonical objects whose existence is proven with AC to be not "genuinely" existing? –  Monroe Eskew Apr 20 at 15:31
"Or an axiom asserting that a particular class of self-referential definitions do indeed define unique functions." Are you wanting to go outside first order logic? –  Monroe Eskew Apr 20 at 15:33
@user18921: I guess it’s that I find your classification rather un-compelling — particularly the suggestion that “more complicated sets from less” axioms tend to satisfy uniqueness properties, while “bigger from smaller” tend not to. –  Peter LeFanu Lumsdaine Apr 20 at 15:50

Axiom: $0^\sharp$ exists.

$0^\sharp$ is a pivotal principle in the large cardinal hierarchy, but it is actually a set of natural numbers. If it exists, it is unique.

-
How about, "For all $x$, $x^\sharp$ exists?" –  Monroe Eskew Apr 20 at 19:23
Yep it definitely fits the bill, although I'll leave the question open for a few days to see if any other suggestions come through. –  goblin Apr 20 at 19:31

I like to use the following very mild extension of ZFC. Add a predicate "Sat"; add axioms saying that this predicate satisfies the expected inductive clauses to define "satisfaction of $\in$-formulas in the full universe of sets"; and add replacement (or separation and collection) axioms for formulas in which Sat occurs. (By $\in$-formulas, I mean formulas in the usual language of ZFC, whose only non-logical symbol is $\in$; thus these formulas do not involve Sat, and so this theory does not run afoul of Tarski's theorem on undefinability of truth.)

This extension of ZFC proves the consistency of ZFC; just show that all the ZFC axioms are true in the universe, and first-order deduction preserves truth. In fact, this extension of ZFC proves the existence of what Montague and Vaught called natural models of ZFC, i.e., models of the form $V_\alpha$ (an initial segment of the cumulative hierarchy) with the standard membership relation. That implies also the existence of countable standard models of ZFC.

Where most set-theorists work with countable elementary submodels of $H_\theta$, the collection of sets of hereditary cardinality $<\theta$, for some unspecified but sufficiently large $\theta$, this extension of ZFC allows me to work with countable elementary submodels of the universe --- which is what one usually really wants anyway, $\theta$ being just a circumlocution to avoid using Sat.

Basically, the use of this extension of ZFC as my metatheory removes most of the headaches that arise when I want to work with proper classes but feel compelled (by honesty) to say things that make sense in ZFC.

-
So just to confirm, the schema for $\mathrm{Sat}$ is $\varphi \leftrightarrow [G(\varphi) \in \mathrm{Sat}]$ for all first-order formulae $\varphi$ in the language $\{\in\}$? Where $G(\varphi)$ is the Godel code of $\varphi$ and $G$ is a function in the metatheory. –  goblin Apr 21 at 4:30
By "the expected inductive clauses", I meant clauses saying things like "a conjunction is satisfied (by an assignment of values to the variables) iff both conjuncts are" and "a universal quantification is satisfied iff all its instances are" and "$x\in y$ is satisfied iff the value assigned to $x$ is a member of the value assigned to $y$." This will involve some coding, but it needn't be Gödel numbering; it would be OK to represent formulas by set-theoretic tuples. [continued in next comment] –  Andreas Blass Apr 21 at 13:47
This set-up will imply all instances of the schema you described, by induction on the complexity of $\varphi$, but I think the greater generality (applicability to all $\in$-formulas as defined in ZFC, without assuming they're standard) is needed when one shows that formal deduction preserves satisfiability. –  Andreas Blass Apr 21 at 13:49