5
$\begingroup$

In Zermelo-Fraenkel axiomatics, one does not need to use the axiom of choice to resolve unique existential quantifiers, the axiom of replacement is enough for this.

But it seems that Type theory does not allow that: if you have a family of singletons, there is no way to get the family of its members. If it is true, that can be proven by constructing a model of Type theory in which this does not hold.

I suspect that “homotopic” models can be useful there — there are families of contractible spaces which have no section, but I have no clue about how to do it for real.

$\endgroup$
5
  • 1
    $\begingroup$ If you have a family of judgemental singletons, then indeed, and the syntactic model is enough. But for instance using the existential in HoTT (which is also proof irrelevant, but propositionally so) unique choice is simply provable. The only problem here is that judgemental things are all dealt with by the machine, but "being a singleton" generally isn't decidable. $\endgroup$
    – Trebor
    Oct 13, 2022 at 9:08
  • $\begingroup$ "If it is true, that can be proven by constructing a model of Type theory in which this does not hold." Can you elaborate on this? $\endgroup$
    – Couchy
    Oct 13, 2022 at 13:19
  • $\begingroup$ AUC may not be the best way to accomplish what you want. You may be interested in a stronger definite description operator. But definite description is very confusing TBH. $\endgroup$ Oct 16, 2022 at 0:32
  • $\begingroup$ @Couchy This sentence is related to my comment on Andrej Bauer's answer: if some axiomatic theory does not allow to prove a result, there exists (by completeness of first order logic, that should suffice) a model of that axiomatic theory (eg, of CIC) where this result is false. $\endgroup$
    – ACL
    Oct 17, 2022 at 6:35
  • $\begingroup$ That's probably true, but CIC is not a first order logic so you can't conclude that from completeness $\endgroup$
    – Couchy
    Oct 17, 2022 at 20:41

1 Answer 1

8
$\begingroup$

Let $\exists! z \in C . P(z)$ be shorthand for $\exists z \in C . (P(z) \land \forall w \in C . P(w) \to z = w)$.

Your question is related to the axiom of unique choice (AUC): given a relation $R : A \to B \to \mathsf{Prop}$ satisfying $$\forall x \in A . \exists! y \in B . R(x, y), \tag{1}$$ is there a map $f : A \to B$ such that $\forall x \in A . R(x, f x)$? Indeed, $R$ can be thought of as a singleton in $B$ parameterized by $A$, and $f$ is the unique element of $B$ (still parameterized by $A$).

A relation satisfying (1) is called a functional relation.

Another way to state AUC is this: the graph of $f : A \to B$ is the relation $\Gamma_f : A \to B \to \mathsf{Prop}$ defined by $$\Gamma_f \, a\, b \mathrel{{:}{=}} (f a = b).$$ Then AUC states that every functional relation is the graph of a function.

Whether AUC holds depends on how precisely we set up foundations.

In toposes AUC holds, so in particular it holds in ZFC and other set theories.

In Martin-Löf type theory AUC holds if we write (1) as $$\textstyle \prod_{x : A} (\sum_{y : B} R(x,y) \times \prod_{z : B} R(x,z) \to \mathsf{Id}(y,z)) $$ That's because we used $\Sigma$ in place of $\exists$, so we can extract the witness $y$. (Of course, for the same reason MLTT validates the full axiom of choice.)

In homotopy type theory AUC holds. Note that $$ \textstyle \exists z \in C . (P(z) \land \forall w \in C . P(w) \to z = w) $$ is defined to be $$ \textstyle \|\sum_{z : C} (P(z) \times \prod_{w : C} P(w) \to z = w) \| $$ Because the type inside the truncation is a proposition, we may apply Lemma 3.9.1 of HoTT book to extract $z : C$.

In the Calculus of Inductive Constructions, i.e., the type theory of Coq, AUC does not hold when we use $\mathsf{Prop}$. This is so because we cannot eliminate from the proposition $\exists! y \in B . R(x, y)$ to $B$, unless $B$ itself is a proposition.

So the question really is: which formalism are you using?

$\endgroup$
8
  • 1
    $\begingroup$ Perfect answer in general, but I’d say it boils down to a slightly more specific question at the end: What definition/axiomatisation of $\exists$ are you using? $\endgroup$ Oct 13, 2022 at 19:15
  • 1
    $\begingroup$ I believe equality also plays a role. $\endgroup$ Oct 13, 2022 at 23:13
  • $\begingroup$ @PeterLeFanuLumsdaine: Can you explain what you meant? Consider CIC and in IHOL: $\mathsf{Prop}$ and $\Omega$ are both complete lattices, and hence axiomatize $\exists$ the same way, but IHOL validates AUC and CIC doesn't. The difference between the two is in how $\mathsf{Prop}$ and $\Omega$ are situated within the rest of the foundation. $\endgroup$ Oct 16, 2022 at 12:35
  • 1
    $\begingroup$ Right, I think the present discussion just reinforces the last line of my answer. $\endgroup$ Oct 16, 2022 at 15:09
  • 1
    $\begingroup$ @ACL: the discussion about AUC in Yannick Forster's PhD thesis is pretty detailed and it explains the relationship between AUC and CIC. $\endgroup$ Oct 17, 2022 at 7:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.