SEAR plus epsilon




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.

Defining SEAR+ε\varepsilon

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 ϕ:AB\phi:A\looparrowright B and xAx\in A, yBy\in B, we have the assertion ϕ(x,y)\phi(x,y), and for an operation f:ABf:A\rightsquigarrow B and xAx\in A we have an element f(x)Bf(x)\in B. 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

Axiom 1+ε1+\varepsilon (Choice operator)

If φ:AB\varphi:A\looparrowright B is a pre-relation such that for every xAx\in A there exists a yBy\in B with φ(x,y)\varphi(x,y), then there exists an operation ε φ:AB\varepsilon_\varphi :A\rightsquigarrow B such that φ(x,ε φ(x))\varphi(x,\varepsilon_\varphi(x)) for all xAx\in A.

A set is defined to be a pre-set AA equipped with an equivalence pre-relation = A=_A. A relation between sets is a pre-relation which is extensional, i.e. if φ(x,y)\varphi(x,y), x= Axx'=_A x, and y= Byy'=_B y, then φ(x,y)\varphi(x',y'). Likewise, a function f:ABf:A\to B between sets is an operation f:ABf:A\rightsquigarrow B which is extensional, i.e. if x= Axx' =_A x then f(x)= Bf(x)f(x')=_B f(x). We define two functions f,g:ABf,g:A\to B to be equal if f(x)= Bg(x)f(x)=_B g(x) for all xAx\in A. Note that we have no notion of equality for arbitrary operations between pre-sets.

For any operation f:ABf:A\rightsquigarrow B between sets, we have a pre-relation (its graph) defined by Γ f(x,y)(f(x)= By)\Gamma_f(x,y) \Leftrightarrow (f(x)=_B y), which is entire in the sense that for any xAx\in A, there is a yBy\in B with Γ f(x,y)\Gamma_f(x,y). This pre-relation is extensional in yy, but not in xx unless ff is actually a function (in which case Γ f\Gamma_f is a functional relation in the usual sense). Conversely, Axiom 1+ε1+\varepsilon 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 A,BA,B and any relation φ:AB\varphi:A\looparrowright B, there exists a pre-set |φ||\varphi| and operations p:|φ|Ap:{|\varphi|}\rightsquigarrow A and q:|φ|Bq:{|\varphi|}\rightsquigarrow B such that φ(x,y)\varphi(x,y) iff there exists z|φ|z\in {|\varphi|} with p(z)= Axp(z)=_A x and q(z)= Byq(z)=_B y. We can then define z= |φ|zz=_{|\varphi|} z' iff p(z)= Ap(z)p(z)=_A p(z') and q(z)= Bq(z)q(z)=_B q(z') to make |φ||\varphi| into a set and p,qp,q into functions that are jointly injective. Axioms 3, 4, and 5 are easy to translate.

We call this theory SEAR+εSEAR+\varepsilon. Clearly the sets, elements (with defined equality), and relations in any model of SEAR+εSEAR+\varepsilon satisfy the axioms of SEAR. Conversely, from any model of SEAR-C we can construct a model of SEAR+εSEAR+\varepsilon by taking the pre-sets, pre-relations, and operations to be the SEAR-C sets, relations, and functions respectively. With this interpretation axiom 1+ε1+\varepsilon is precisely the SEAR-C axiom of choice. The question is whether we can get SEAR+εSEAR+\varepsilon without assuming or implying choice.

Conservativity over COSHEP

Our goal is to prove that SEAR+εSEAR+\varepsilon 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 VV. Recall that COSHEP means that in VV, every set admits a surjection from a projective one. We define a model of SEAR+εSEAR+\varepsilon as follows.

  • The pre-sets are the projective VV-sets.
  • The elements are the VV-elements.
  • The pre-relations are the VV-relations.
  • The operations are the VV-functions.

We will continue to qualify the notions in the old model VV, using unqualified words such as “set” for the new notions defined above.

Axiom 0 of SEAR+εSEAR+\varepsilon is obviously true. For Axiom 1, we need to translate a first-order formula in the language of SEAR+εSEAR+\varepsilon into a formula in the language of SEAR in order to apply Axiom 1 of VV, but the above dictionary tells us exactly how to do that. Axiom 1+ε1+\varepsilon is true because we have chosen the pre-sets to be the projective sets in VV, so any entire VV-relation between them contains a VV-function.

Now a set AA in our putative model of SEAR+εSEAR+\varepsilon is a VV-set equipped with an equivalence relation = A=_A, so in particular it has a quotient A/= AA/{=_A}. Now any relation ABA\looparrowright B, meaning extensional relation, induces a VV-relation (A/= A)(B/= B)(A/{=_A}) \looparrowright (B/{=_B}), and conversely any such VV-relation induces a relation ABA\looparrowright B, setting up a meta-bijection. The same is true of functions ABA\to B and VV-functions (A/= A)(B/= B)(A/{=_A}) \to (B/{=_B}). It follows that we have meta-functors SetSet VSet\to Set_V and RelRel VRel\to Rel_V given by “take quotients” that are fully faithful.

I claim that in fact these functors are essentially surjective as well. For given any VV-set AA, by COSHEP there is a projective set PP and a surjection e:PAe:P\to A. Since Set VSet_V is a regular category, it follows that AA is the quotient set of the kernel pair of ee. But that means that if we call this kernel pair = P=_P, then PP becomes a new-style set which maps onto AA under the quotient functor; hence this functor is essentially surjective.

It follows that the meta-categories SetSet and RelRel (in the new sense) are equivalent to the old meta-categories Set VSet_V and Rel VRel_V. 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 VV. (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 SEAR+εSEAR+\varepsilon. Furthermore, its underlying SEAR-model is equivalent to VV. (The notion of “equivalence” here means “(weak) equivalence of categories of sets,” as above. But since SEAR intrinsically aheres to the principle of equivalence, 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 SEAR+εSEAR+\varepsilon are precisely those which are true in VV.

Therefore, any statement in the language of SEAR which is true in all models of SEAR that underlie models of SEAR+εSEAR+\varepsilon 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 SEAR+εSEAR+\varepsilon 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 SEAR+εSEAR+\varepsilon we’ve just constructed also satisfies COSHEP (as it must, given its equivalence to VV). In fact, if a model of SEAR+εSEAR+\varepsilon admits an “identity” equivalence pre-relation A\equiv_A on every pre-set, and relative to which all pre-relations and operations are extensional, then it must satisfy COSHEP—for then every set (A,= A)(A,{=_A}) is the surjective image of the set (A, A)(A,{\equiv_A}), which is projective by Axiom 1+ε1+\varepsilon.

Without COSHEP

Now I step in to say: SEAR+εCOSHEP\mathbf{SEAR} + \varepsilon \vDash COSHEP.

The reason is that every preset does admit an identity prerelation as in the last paragraph above; let x Ayx \equiv_A y if x Ryx \sim_R y for every reflexive prerelation R:AAR: A \looparrowright A (or even for every equivalence prerelation). This will work also in ETCSAC+ε\mathbf{ETCS} - AC + \varepsilon by quantifying over prefunctions f:A𝒫1f: A \to \mathcal{P}1 and using the kernel of ff (relative to the standard equality on truth values) as the equivalence relation. (Of course, SEAR\mathbf{SEAR} 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 CETCSCOSHEP+ε\mathbf{CETCS} - COSHEP + \varepsilon (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 x Ayx \equiv_A y if R(x,y)R(x,y) for every equivalence pre-relation R:AAR: A \looparrowright A. Then every operation and every pre-relation is extensional with respect to these identity relations.


Suppose f:ABf:A\rightsquigarrow B is an operation. Define K f:AAK_f:A\looparrowright A by K f(x,x)K_f(x,x') iff f(x) Bf(x)f(x)\equiv_B f(x'). Then RR is an equivalence pre-relation, so if x Axx\equiv_A x', then K f(x,x)K_f(x,x'), and hence f(x) Bf(x)f(x)\equiv_B f(x').

Similarly, suppose φ:AB\varphi:A\looparrowright B is a pre-relation. Define R φ:AAR_\varphi:A\looparrowright A by R φ(x,x)R_\varphi(x,x') iff φ(x,y)φ(x,y)\varphi(x,y)\Leftrightarrow\varphi(x',y) for all yBy\in B. Then R φR_\varphi is an equivalence pre-relation, so if x Axx\equiv_A x', then R φ(x,x)R_\varphi(x,x') and so φ(x,y)φ(x,y)\varphi(x,y)\Leftrightarrow\varphi(x',y) for all yBy\in B.

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 ε\varepsilon has to work as in Axiom 1+ε1 + \varepsilon; how about this?

Axiom ε\varepsilon (Global Choice Operator)

Add a symbol (actually several symbols) to the language for an operation that assigns to each set AA:

  • a set AA',
  • an injective function i A:AAi_A: A \to A',
  • and an element ϵ A\epsilon_A of AA';

then add the axiom that ϵ A\epsilon_A belongs to the image of i Ai_A if (hence iff) AA is inhabited.

With excluded middle, this is a theorem with A+0 AA + 0^A for AA' as in the discussion at choice operator. But even this may be too strong; I really want to say that ϵ A\epsilon_A takes values in A A_\bot (the set of subsingleton subsets of AA) with ϵ A\epsilon_A an inhabited subsingleton if (hence iff) AA is inhabited, but the existence of A A_\bot is itself impredicative (in the presence of function sets) since 1 1_\bot is the set of truth values.

Without COSHEP, predicatively

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+ε\varepsilon. 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+ε\varepsilon 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 A\equiv_A by quantifying over relations (note that avoiding this requires not only throwing out powersets, but restricting axiom 1 to bounded quantification).

Now: is CSEAR+ε\varepsilon conservative over CSEAR?

Last revised on October 4, 2021 at 09:38:39. See the history of this page for a list of all contributions to it.