¿Qué tipo de "conjuntos infinitos" ¿constructivistas uso?

Question

Pregunta Original título: "¿Cómo constructivistas lidiar con diferentes conceptos de infinito?", cambiado en favor de algo menos subjetiva de sonido.

Entiendo que hay razones para querer constructivo de las pruebas. No tengo ningún problema en aceptar que algunas personas no aceptan otros tipos de pruebas, como en el constructivismo. Lo que no entiendo, sin embargo, es cómo uno puede creer firmemente que el Constructivismo es "la" opción de ir cuando hay diferentes conceptos de infinito que sólo puede ser demostrado como el de la igualdad con el axioma de elección, que el uso no está permitido en el constructivismo. Mi razonamiento para la versión subjetiva de la pregunta del título es que creo que el constructivismo está ligada a algún tipo de intuición, sin embargo, todas las definiciones de abajo parecen intuitivamente ser el mismo para mí.

---

Ahora voy a introducir los diferentes tipos de conjuntos infinitos de acuerdo a Oliver Deiser "Einführung in die Mengenlehre" (introducción a la teoría de conjuntos) (2ª edición, Springer, 2004). La definición de estos se pueden encontrar en el capítulo 6 "Unendliche Mengen" (conjuntos infinitos) (a excepción de "cadena" en la página.81).

Deje $M$ ser un conjunto. Una cadena de $C$ $M$ es un subconjunto no vacío de a $\mathcal{P}(M)$ tal que para todos los $A,B\in C$ tenemos $A\subseteq B$ o $B\subseteq A$. $C$ se dice que para tener el máximo de $B\in C$ si para todas las $A\in C$ tiene $A\subseteq B$.

1. $M$ se dice es Dedekind-infinito si existe $N\subsetneq M$ $f:N\to M$ tal que $f$ es bijective.
2. $M$ se dice es Dedekind-infinito-1 si existe $f:A\to A$ tal que $f$ es surjective, pero no inyectiva.
3. $M$ se dice es Dedekind-infinito-2 si existe $f:A\to \mathbb N$ tal que $f$ es surjective.
4. $M$ se dice que la Cadena infinita si existe una cadena de $C$ $M$ sin límite máximo.
5. $M$ se dice que Tarski-infinito si existe un $P\subseteq\mathcal{P}(A)$ no vacíos, tales que para todos los $A\in P$ existe un $B\in P$ tal que $A\subsetneq B$.
6. $M$ se dice $\mathbb N$-infinito si existe no $n\in\mathbb{N}$ $f:M\to\{0,\ldots,n-1\}$ $f$ bijective.

Deiser demuestra que 1.$\Rightarrow$2.$\Rightarrow\ldots\Rightarrow$6. (y 6.$\Rightarrow$5.) puede ser demostrado con primaria (constructiva), los métodos, pero necesitaba algún tipo de elección (no constructivas) para mostrar 5.$\Rightarrow$4.$\Rightarrow\ldots\Rightarrow$1. Señala en la p.107 que

Um die tatsächliche Notwendigkeit der Auswahlakte zu beweisen, braucht hombre viel weitergehende Techniken, es könnte ja ein einfacher Beweis übersehen worden sein.

---

Para demostrar la real necesidad de tener que utilizar una opción, mucho más avanzadas técnicas son necesarias, ya que una simple prueba podría haber sido pasado por alto.

Él no explícitamente que este es el caso de prueba de los cuatro casos, pero para esta pregunta, voy a suponer que al menos uno no se puede hacer sin elección. (Otra cosa implicaría una prueba sin opción para $|\mathbb N|\leq |A|\iff\forall n\in\mathbb N:|\{0,\ldots,n-1\}|\leq |A|$, que sería interesante en sí mismo.)

---

Esto plantea la pregunta: ¿hay un "canónica" del concepto de conjuntos infinitos en el constructivismo o es cada concepto considerado por su propio bien? ¿Qué tipo de "conjuntos infinitos" ¿constructivistas uso?

Answer 1

La pregunta es un poco vaga, porque el término "constructivismo" no está definido correctamente, y de hecho hay varias variedades de este. En el constructivismo, según Errett, la respuesta a tu consulta es probablemente más sencillo de lo que crees: usted probablemente no va a encontrar una aparición de cualquier cosa como "$\mathcal P(M)$" aquí. El único "completado" infinity que ha permitido que se $\mathbb N$, y real, el análisis se desarrolla principalmente mediante el uso de $\mathbb N$ (usted estará de acuerdo en que usted no necesita más que eso para definir una secuencia). Por supuesto, los números reales se producen aquí, pero no tanto para la recogida de los mismos.

Así que el tema de la comparación de los diferentes infinitos realmente no surgir, ya que no se considera, a pesar de que hay una versión constructiva de Cantor del diagonalisation argumento.

Answer 2

Hay muchos tipos de constructivismo.

Un tipo es el no-clásica tipo, pero a mí me parece que si una colección es en realidad bien definida, a continuación, todas las formas posibles de expresar que es finito tendría una bien definida de valor de verdad así, filosóficamente hablando. Puede ser que las diferentes definiciones de "finito" no son equivalentes, pero todas las declaraciones de los involucrados deben tener clásica de la verdad-valores si tienen significado bien definido.

Esto no significa que no la lógica clásica es inútil. Así por ejemplo, los intuitionistic lógica está ligada a los programas de modal y la lógica a través de la BHK interpretación y marcos de Kripke. Pero no se debe confundir la verdad con el conocimiento o la constructibility. Por ejemplo, sabemos que la detención problema no puede ser resuelto. Este es un valor booleano hecho. Sí, hay un programa de ordenador que permitan generar un contra-ejemplo (programa de entrada) par a cualquier afirmó detener oracle, pero la mera noción de la detención problema en sí requiere que el (clásico) suposición de que cualquier programa que se ejecuta en una entrada de cualquiera de frenar o no frenar.

También, a partir de una lógica de la perspectiva, de manera razonable fundamentales del sistema de la lógica en sí misma debe interpretar clásicos PA (discrete ordenó semi-anillo de los axiomas más de inducción) para lo más básico sintáctica conceptos como provability de ser significativo. Es entonces filosóficamente justificada para ampliarlo a los de ACA, que no es más que la adición de conservadores de extensión, además de la inducción completa el esquema. Resulta que un montón de análisis real se puede hacer dentro de ACA.

Uno podría extender a predicativo de orden superior de la aritmética, al tener una base de tipo $nat$ $bool$ y una especie $S \to T$ para todas las funciones de$S$$T$, para cualquier tipo $S,T$. (Tenga en cuenta que un conjunto de ACA puede ser considerado como un miembro de $nat \to bool$.) El orden de $S \to T$ es uno más que el orden máximo de $S,T$. Se permite la construcción de un objeto de orden de $k$ sólo si su definición de la fórmula cuantifica sólo a través de clases con el fin de menos de $k$, lo que haría conservador sobre la PA. Después de que se le agrega la inducción completa el esquema (que puede ser justificado meta-lógicamente), y esto hace que sea mucho más fuerte que la PA y de la ACA. Basta para prácticamente todos concreto de las matemáticas (aunque, por supuesto, es incompleta).

Dentro de ACA, es fácil definir un conjunto $S$ ser infinito (7) iff $\forall x \in S\ \exists y \in S\ ( y>x )$. Tenga en cuenta que todas tus seis definiciones excepción de Tarski-infinito puede ser expresado en ACA, a través de una adecuada codificación. Para expresar Tarski-infinito necesita ser tener al menos (predicativo) 3-el fin de la aritmética. Lado comentario: Su definición (4) debe decir "no vacía cadena".

Resulta que cuando se limita a la lengua de ACA, todos los 5 expresable definiciones son equivalentes, debido a que cada conjunto de ACA es un subconjunto de a $nat$ y tenemos buen orden de $nat$, lo que elimina la necesidad de cualquier elección.

Es cuando se mueve a la de tercer orden, que las cosas se ponen interesantes. Desde el punto de vista de ZFC, de orden superior de la aritmética tiene un modelo con plena powersets, y multitud de juegos pueden ser muy extraño. No tenemos una buena ordenación del conjunto de los subconjuntos de los naturales, a menos que tengamos algún tipo de elección axioma.

La elección puede justificarse fácilmente si el modelo es contable, porque entonces se podría interpretar como el uso de el buen orden de la intención de modelo. Esta es la razón por la elección es a menudo considerado aceptable en el tipo constructivo de las teorías (pero no intuitionistic tipo de teorías). Pero si el modelo es no contables, como con ZFC, entonces es más difícil justificar la elección, salvo que, literalmente, se cree en la platónica de la existencia de la plena powersets, en cuyo caso, 'obviamente' choice tiene.

---

En general, es cierto que muchos de los conceptos matemáticos dividida en múltiples variantes en la construcción de las fundaciones. Bien ordenar es otra, donde la definición ( no estrictamente disminución de la secuencia ) es equivalente a ( todos los no-vacío subconjunto tiene un mínimo ), en general, sólo en la presencia de una débil forma de elección. Pero no debería ser sorprendente que no tenemos elección para demostrar la equivalencia entre las contables bien ordenamientos.