10
$\begingroup$

Background

In Intuitionistic Type Theory (p. 27-28), Martin Löf provides a proof of the axiom of choice that is constructively valid. This version is considerably weaker than the ordinary set theory version, since there are no quotient types. Now, quotients can to a certain extent be simulated using setoids, and thus the axiom of choice may be reformulated to what Martin Löf (2004) calls Zermelo's axiom of choice. This axiom is non-constructive, as it implies PEM (Diaconescu's theorem). Nonetheless, there are special cases of Zermelo's axiom of choice, which are provable in type theory. I have heard that one of these is the so-called axiom of dependent choice, which can be stated as:

For every set $A$ and for every binary relation $R$ on $A$: \begin{equation} (\forall x:A)(\exists y:A)R(x,y) \supset (\forall x:A)(\exists f:N \to A)I(A,\text{Ap}(f,0),x) \land (\forall n:N)R(\text{Ap}(f,n),\text{Ap}(f,S(n))) \end{equation}

Now, my question is how exactly would one go about proving this result constructively? Would it be to any help to use the version of axiom of choice which Martin Löf proved in Intuitionistic Type Theory?

$\endgroup$
5
  • 1
    $\begingroup$ The relationship between AC and DC in type theoretic systems tends to be very delicate. It is not even true in classical second-order arithmetic that AC implies DC. So any proof in constructive systems will have to use some method that cannot be formalized in that setting. $\endgroup$
    – Carl Mummert
    Dec 18, 2013 at 21:39
  • $\begingroup$ @CarlMummert . Understood. My initial idea was to use the axiom of choice (as presented in Intuitionistic Type Theory p. 27-28) to obtain a function $f:N \to A$ such that $(\forall n:N)R(n,\text{Ap}(f,n))$, which I then would work on to obtain the desired result. But this you say is a futile method, correct? $\endgroup$
    – user116234
    Dec 19, 2013 at 12:13
  • 1
    $\begingroup$ I have not looked at it in that setting (the setting of intuitionistic type theory). The availability of full AC for higher types may save you after all, in that context. For example, the proof of DC from AC in ZFC uses higher types compared to the instance of DC being proved, and so that proof may be emulatable in ITT as well. As you say, it works by simply iterating a choice function starting with $x$. But the problem is in the details, and I don't have the experience to know whether it would work out in this setting. $\endgroup$
    – Carl Mummert
    Dec 19, 2013 at 12:35
  • $\begingroup$ Where does one read up on type theory? $\endgroup$
    – Maxwell
    Dec 19, 2013 at 14:27
  • $\begingroup$ @Maxwell That entire depends on which type (pun intended) of type theory you are interested to learn more about. If this is Intuitionistic Type Theory, then the following link is of great interest csie.ntu.edu.tw/~b94087/ITT.pdf . $\endgroup$
    – user116234
    Dec 19, 2013 at 14:58

1 Answer 1

Reset to default
3
+500
$\begingroup$

We want to find a proof term for the following type: $$ (\forall x: A. \exists y: A. R(x,y)) \to \forall x: A. \exists f: \mathbb{N} \to A. f(0) = x \,\land\, \forall n: \mathbb{N}. R(f(n), f(\mathsf{succ}(n)))$$

Let $h: \forall x: A. \exists y: A. R(x, y)$, and $x : A$. We need to exhibit a function $f: \mathbb{N} \to A$ and a proof term for the required property. Intuitively, we want $f$ such that

$$\left\{\begin{array}{l} f(0) = x\\ f(\mathsf{succ}(n)) = \pi_1 (h(f(n))) \end{array}\right.$$

therefore we let $f = \lambda n: \mathbb{N}. \mathsf{natrec}(n,\,x,\, \lambda n': \mathbb{N}. \lambda y: A. \pi_1 (h(y)))$. Then you have that $f(0)$ normalizes to $x$, and so $\mathsf{id}(x)$ is a proof of $f(0) = x$. Now, let $n: \mathbb{N}$. We want to prove that $R(f(n),f(\mathsf{succ}(n)))$. But this is given precisely by $\pi_2 (h(f(n)))$, since $f(\mathsf{succ}(n))$ normalizes to $\pi_1 (h(f(n)))$. In conclusion, a proof term for the proposition would be:

$$\lambda h: \forall x: A. \exists y: A. R(x, y). \lambda x: A.\\ \langle \lambda n: \mathbb{N}. \mathsf{natrec}(n,\,x,\, \lambda n': \mathbb{N}. \lambda y: A. \pi_1 (h(y))),\\ \langle \mathsf{id}(x), \lambda n: \mathbb{N}. \pi_2 (h(\mathsf{natrec}(n,\,x,\, \lambda n': \mathbb{N}. \lambda y: A. \pi_1 (h(y))))) \rangle \rangle $$

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .