Axioma de Elección de Tipo Teórico (Prueba)

Question

De fondo

En Intuitionistic Tipo de Teoría (p. 27-28), Martin Löf ofrece una prueba de que el axioma de elección, es decir, de manera constructiva válido. Esta versión es considerablemente más débil que el ordinario de la teoría de conjuntos versión, ya que no hay cociente tipos. Ahora, los cocientes puede en cierta medida ser simulado utilizando setoids, y por lo tanto el axioma de elección pueden ser reinterpretados a lo que Martin Löf (2004) llama Zermelo del axioma de elección. Este axioma no es constructiva, ya que implica PEM (Diaconescu del teorema). Sin embargo, hay casos especiales de Zermelo del axioma de elección, que son demostrables en el tipo de teoría. He oído que uno de estos es el llamado axioma de la dependiente de la elección, que puede ser enunciada como:

Para cada conjunto $A$, y para cada relación binaria $R$$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}

Ahora, mi pregunta es ¿cómo se podría ir sobre probar este resultado de manera constructiva? Sería de ninguna ayuda para utilizar la versión del axioma de elección, que Martin Löf demostrado en Intuitionistic Tipo de Teoría?

Answer 1

Queremos encontrar una prueba de plazo para el siguiente tipo: $$ (\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)))$$

Deje $h: \forall x: A. \exists y: A. R(x, y)$, e $x : A$. Tenemos que exhiben una función de $f: \mathbb{N} \to A$ y una prueba de plazo para la propiedad requerida. Intuitivamente, queremos $f$ tal que

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

por lo tanto dejamos $f = \lambda n: \mathbb{N}. \mathsf{natrec}(n,\,x,\, \lambda n': \mathbb{N}. \lambda y: A. \pi_1 (h(y)))$. Entonces usted tiene que $f(0)$ normaliza a $x$, y por lo $\mathsf{id}(x)$ es una prueba de $f(0) = x$. Ahora, vamos a $n: \mathbb{N}$. Queremos demostrar que $R(f(n),f(\mathsf{succ}(n)))$. Pero esto se da precisamente por $\pi_2 (h(f(n)))$, ya que el $f(\mathsf{succ}(n))$ normaliza a $\pi_1 (h(f(n)))$. En conclusión, una prueba de plazo para la proposición sería:

$$\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 $$