The goal of this page is to prove that a non-extensional choice operator is conservative over a theory without AC. I’ll take the theory without AC to be SEAR, for definiteness and since that’s where I'm most comfortable.
For the theory with a non-extensional choice operator, consider the following theory, which is a variant of the version of SEAR without fundamental equality described at SEAR. There are four basic sorts: pre-sets, pre-relations, elements, and operations (or pre-functions). Each element belongs to a pre-set, and each pre-relation and operation has a source and target which are pre-sets. For a prerelation and , , we have the assertion , and for an operation and we have an element . There is no predefined notion of equality of anything. Axioms 0 and 1 of SEAR are unmodified, except that the uniqueness clause of the latter is interpreted as a definition of when two parallel pre-relations are called “equal”. We also impose
If is a pre-relation such that for every there exists a with , then there exists an operation such that for all .
A set is defined to be a pre-set equipped with an equivalence pre-relation . A relation between sets is a pre-relation which is extensional, i.e. if , , and , then . Likewise, a function between sets is an operation which is extensional, i.e. if then . We define two functions to be equal if for all . Note that we have no notion of equality for arbitrary operations between pre-sets.
For any operation between sets, we have a pre-relation (its graph) defined by , which is entire in the sense that for any , there is a with . This pre-relation is extensional in , but not in unless is actually a function (in which case is a functional relation in the usual sense). Conversely, Axiom says that any entire pre-relation induces an operation, and for an entire and functional relation between sets, this induced operation is a function (and is unique, in the sense of equality of functions defined above).
Now Axiom 2 can be taken to read: For any sets and any relation , there exists a pre-set and operations and such that iff there exists with and . We can then define iff and to make into a set and into functions that are jointly injective. Axioms 3, 4, and 5 are easy to translate.
We call this theory . Clearly the sets, elements (with defined equality), and relations in any model of satisfy the axioms of SEAR. Conversely, from any model of SEAR-C we can construct a model of by taking the pre-sets, pre-relations, and operations to be the SEAR-C sets, relations, and functions respectively. With this interpretation axiom is precisely the SEAR-C axiom of choice. The question is whether we can get without assuming or implying choice.
Our goal is to prove that is conservative over SEAR. But since I haven’t quite figured out how to do that (or, to be fair, even whether it’s true), as a warm-up let’s prove that the same thing is true when we add COSHEP, a choice-like axiom notably weaker than full AC, to both sides.
Suppose we have a model of SEAR satisfying COSHEP, call it . Recall that COSHEP means that in , every set admits a surjection from a projective one. We define a model of as follows.
We will continue to qualify the notions in the old model , using unqualified words such as “set” for the new notions defined above.
Axiom 0 of is obviously true. For Axiom 1, we need to translate a first-order formula in the language of into a formula in the language of SEAR in order to apply Axiom 1 of , but the above dictionary tells us exactly how to do that. Axiom is true because we have chosen the pre-sets to be the projective sets in , so any entire -relation between them contains a -function.
Now a set in our putative model of is a -set equipped with an equivalence relation , so in particular it has a quotient . Now any relation , meaning extensional relation, induces a -relation , and conversely any such -relation induces a relation , setting up a meta-bijection. The same is true of functions and -functions . It follows that we have meta-functors and given by “take quotients” that are fully faithful.
I claim that in fact these functors are essentially surjective as well. For given any -set , by COSHEP there is a projective set and a surjection . Since is a regular category, it follows that is the quotient set of the kernel pair of . But that means that if we call this kernel pair , then becomes a new-style set which maps onto under the quotient functor; hence this functor is essentially surjective.
It follows that the meta-categories and (in the new sense) are equivalent to the old meta-categories and . Since the remaining axioms of SEAR are essentially just statements about these categories, their truth in the “new world” follows immediately from their truth in . (There’s no need to worry about a meta-axiom-of-choice, since these axioms are just statements about finite numbers of objects and morphisms, so “fully faithful and essentially surjective” is a perfectly sufficient notion of “equivalence.”)
Thus, we have constructed a model of . Furthermore, its underlying SEAR-model is equivalent to . (The notion of “equivalence” here means “(weak) equivalence of categories of sets,” as above. But since SEAR speaks no evil, this suffices to show that exactly the same first-order statements are true in both.) It follows that the statements in the language of SEAR which are true in this new model of are precisely those which are true in .
Therefore, any statement in the language of SEAR which is true in all models of SEAR that underlie models of is, in fact, true in all models of SEAR+COSHEP. This is the conservativity result we were looking for. Its practical upshot is that if you want to work in SEAR+COSHEP, you might as well work in if it’s more convenient to have a choice operator, since the theorems you can prove in either case will be exactly the same.
Note that the model of we’ve just constructed also satisfies COSHEP (as it must, given its equivalence to ). In fact, if a model of admits an “identity” equivalence pre-relation on every pre-set, and relative to which all pre-relations and operations are extensional, then it must satisfy COSHEP—for then every set is the surjective image of the set , which is projective by Axiom .
Now I step in to say: .
The reason is that every preset does admit an identity prerelation as in the last paragraph above; let if for every reflexive prerelation (or even for every equivalence prerelation). This will work also in by quantifying over prefunctions and using the kernel of (relative to the standard equality on truth values) as the equivalence relation. (Of course, is capable of using this method too.) It will still work in versions with intuitionistic logic, but not (as far as I can see) in (following Palmgren), where one cannot take power sets or quantify over subsets.
Mike Shulman: Ah, you’re right. I actually thought of that briefly, but then I didn’t immediately see how to prove the following.
Define if for every equivalence pre-relation . Then every operation and every pre-relation is extensional with respect to these identity relations.
Suppose is an operation. Define by iff . Then is an equivalence pre-relation, so if , then , and hence .
Similarly, suppose is a pre-relation. Define by iff for all . Then is an equivalence pre-relation, so if , then and so for all .
Of course, as you point out, this is very impredicative. Does that mean that your original suggestion would only acceptable be for someone who either (1) accepts COSHEP or (2) doesn’t accept (quantification over) powersets?
Toby: That may be so; I hadn't thought through all of the implications, so I was hoping otherwise. However, I'm not sure that has to work as in Axiom ; how about this?
Add a symbol (actually several symbols) to the language for an operation that assigns to each set :
then add the axiom that belongs to the image of if (hence iff) is inhabited.
With excluded middle, this is a theorem with for as in the discussion at choice operator. But even this may be too strong; I really want to say that takes values in (the set of subsingleton subsets of ) with an inhabited subsingleton if (hence iff) is inhabited, but the existence of is itself impredicative (in the presence of function sets) since is the set of truth values.
Okay, second try. Define constructive SEAR to use intuitionistic logic and consist of Axioms 0, 1B, 2, and 4 of SEAR (no power sets) together with
Now modify it as above, removing basic equality and adding a basic notion of “operation,” to obtain CSEAR+. Note that the axiom of quotient sets becomes redundant, given the definition of “set” as a preset with an equivalence prerelation.
The same argument as above should show that CSEAR+ is conservative over CSEAR+COSHEP. (Just as Bounded SEAR is equivalent to ETCS, CSEAR+COSHEP is equivalent to Palmgren’s CETCS.) However, the converse argument above fails since we cannot define by quantifying over relations (note that avoiding this requires not only throwing out powersets, but restricting axiom 1 to bounded quantification).
Now: is CSEAR+ conservative over CSEAR?