Cómo constructivo es Doyle-Conway 'División por tres'?

Question

En el (caprichosamente por escrito) el artículo de la División por tres, Doyle y los Conway describir una prueba, (al parecer) no utilizar Elección, que un isomorfismo $A \times 3 \simeq B\times 3$ de juegos (donde $3$ es un dado de tres element set) le da un isomorfismo $A \simeq B$. El resultado es fácil para bien ordenados $A$ e $B$, pero claramente suponiendo que esto no es constructivo. Sin embargo, los autores parecen (para mí) el uso de medio excluido. También, no sé si estoy totalmente convencido de que evitar todas las formas de elección - puede ser que dependen de alguna forma débil de la opción (aparte de medio excluido).

Alguien ha dado este pensamiento? El artículo es a partir de mediados de los años 90, a pesar de su ArXiV fecha, y pretende haber descubierto una pérdida de la prueba de Lindenbaum de la década de 1920, que es anterior a una diferente de la prueba dada por Tarski en 1949.

Answer 1

(Me voy a cortar y pegar y modificar ligeramente algunas de las observaciones tomadas a partir de un debate sobre este tema que están teniendo lugar actualmente en el nForum. Se basa en mi memoria de su papel, que no tengo en frente de mí, así que es posible que he misremembered algo, o que me estoy proyectando algo en el papel cuando me conjetura de que "constructiva" de Conway y Doyle significa realmente "natural".)

Cerca del principio del papel, Conway y Doyle explicar lo que entendemos por 'constructivo' por medio de un ejemplo:

Si $A$, $B$, y $C$ son conjuntos finitos, muestran que $A + C = B + C$ implica $A = B$ constructivamente.

A continuación, los autores dan a lo que es esencialmente un categorified prueba de que puede haber sido observada por primera vez por Joyal. La idea es que hay una noción general de "traza" (que más tarde fue formalizado por Joyal, de la Calle, y la Verdad en su noción de trazado categoría monoidal: algo así como la estructura que se quedaría si usted tomó toda la estructura presente en un tortile o ribboned categoría y, a continuación, nunca se menciona doble de los objetos). La traza es una transformación

$$\phi_{A, B; C}: \hom(A \otimes C, B \otimes C) \to \hom(A, B)$$

lo cual es natural en $A$ e $B$ y extranatural en $C$, la satisfacción de los axiomas que se espera de un parcial de seguimiento. En particular, el monoidal simétrica de la categoría de conjuntos finitos y bijections (con monoidal producto $+$) admite un trazado monoidal estructura que asigna un bijection $f: A + C \to B + C$ a un bijection $g: A \to B$ obtenido por retroalimentación (feed back de los valores de $f$ el cual la tierra en $C$ nuevo en $f$, e iterar hasta que la tierra de $C$).

Esto me dio la idea de que para Conway y Doyle, 'constructivo' significa realmente "natural", en el sentido técnico de la categoría de teoría. Mi memoria es que "constructivo" para ellos significa "no antinatural opciones" (tales como la elección de un bijection $A \cong $ {1, ..., $n$}), hacer sus pruebas "coordenadas-gratis", por así decirlo, y esto es efectivamente formalizada a través de la categoría de sentido de la connaturalidad.

Entonces, en otras palabras, Conway y Doyle son, en esencia, la definición de una transformación natural de la forma

$$\hom(3A, 3B) \to \hom(A, B),$$

donde $A$ e $B$ son interpretados como objetos en la categoría de conjuntos y bijections, y creo que este es el contenido esencial de la "constructivity" son después.

Estándar de pruebas de el Cantor-Schroeder-teorema de Bernstein, también mencionado por Conway y Doyle, a manera de ilustración, que son naturales en el sentido categórico.

Answer 2

La construcción en el papel parece depender de dos no-constructiva supuestos:

1. Podemos decidir si dos elementos en un conjunto (que participa en la división por 3) son iguales.
2. Una contables subconjunto de $\mathbb{N}$ es infinito o no infinito.

(Por "infinito" que significa "contiene una secuencia infinita de pares de elementos distintos".) En la teoría de la computabilidad la segunda hipótesis corresponde a Turing grado $0''$.

A ver si la segunda hipótesis que se utiliza, considere la posibilidad de la prueba del Lema 2 en la página 26. Allí uno se da una secuencia infinita de 0, 1 y 2 y uno debe decidir si hay infinitamente muchos 0 en la secuencia (y si no, si los hay infinitamente muchos 1). Vamos a mostrar que una decisión de este procedimiento es equivalente a la segunda hipótesis. En una dirección, un ternario secuencia contiene una infinidad de 0 si el conjunto de índices en la que el 0 es infinito. A la inversa, dada una contables subconjunto $A \subseteq \mathbb{N}$ enumerados por $e$, considere la secuencia de $a_0, a_1, \ldots$ donde

$a_k = 0$ si $e$ enumera un nuevo elemento en el paso $k$, y $a_k = 1$ lo contrario.

La secuencia tiene una infinidad de 0 iff $A$ es infinito.

Otro tipo de construcción típica en el papel, se requiere determinar si la órbita de un elemento $x$ bajo un bijection es finito o infinito. Podemos hacer esto a través de nuestros supuestos de la siguiente manera. Dado $x \in A$ y un bijection $f : A \to A$, la construcción de una secuencia $a_0, a_1, \ldots$ como sigue:

$a_k = 0$ si no es $m \leq k$ tal que $x = f^m(x)$, y $a_k = 1$ lo contrario.

Aquí se supone que $A$ ha decidable la igualdad. La secuencia de $a_k$ contiene un cero iff que contiene una infinidad de ceros (por lo que sólo requieren de un $0'$ oracle para realizar los pasos siguientes). Si contiene un cero, decir $ak = 0$, entonces la órbita $\lbrace x, f(x), f^2(x), \ldots \rbrace$ es finito con en la mayoría de las $k$ elementos. Si no contiene un cero, entonces la órbita es infinito porque $f^k(x) \neq f^j(x)$ para todos los $k \neq j$, ya que de lo contrario tendríamos $f^{|k-j|+1}(x) = x$.

Permítanme comentar que uno podría estar tentado a considerar la posibilidad de un no-constructiva de la asunción, tales como:

Un grupo generado por un solo elemento es infinita o finita.

(Este sería sin duda nos permiten determinar si las órbitas de los elementos bajo bijections son finitos o infinitos.) De hecho, la división por 3, pero por una extraña razón, a saber, que tal principio implica la ley de medio excluido. Supongamos $p$ es arbitraria thruth valor, y considerar el grupo Abelian $G$ libremente generada por los generadores $p$ e $\top$ (true). Considerar el subgrupo de $G$ generado por el elemento $\top - p$. Si es infinito, no es $n \in \mathbb{N}$ tal que $n \top \neq n p$, por lo tanto $\top \neq p$ e lo $\lnot p$ mantiene. Si el subgrupo es finito entonces no es $n > 0$ tal que $n \top = n p$, por lo tanto $\top = p$ e $p$ mantiene. (Espero que me de este derecho, tenemos que ser cuidadosos porque finito de conjuntos no tiene definido tamaños).

Es de esperar que nos da una idea acerca de cómo no-constructivas son las técnicas empleadas en la prueba de la división por tres (esencialmente se ve como un $0''$ oracle). Parece difícil de cuantificar cómo no-constructivo el teorema en sí es. Sabiendo que no se puede dividir por 3 evidentemente no me permite derivar de la no-constructiva consecuencias. Para todos los que me conocen, algunos adecuadamente constructivized versión de la división por 3 podría ser en realidad de manera constructiva válido.

Puedo tener una bandera verde ahora, por favor?

Answer 3

Yo no vencer a cada detalle, pero se ve constructivo para mí (hay uno b, la cual debe ser B). Hay consideraciones como: Cada componente (en un grafo dirigido con outdegree 1 y el máximo de indegree 1) es un ciclo, un camino infinito trayectoria o un bi-infinito dirigida ruta para hacer a,b o c según el caso. Que es una especie de medio excluido, sino simplemente muestra que el construido bijection (en este caso construido a partir de inyecciones de A->B y B->a para el Cantor–Bernstein–Schroeder teorema) son tan explícitas como en los ingredientes, pero no más (no estoy seguro si lo que capta tu pregunta).

El artículo bien escrito

La producción de Nuevas Bijections de Edad por Feldman, D.; J. Propp en los Avances en Matemáticas, Volumen 113, Número 1, junio de 1995 , pp 1-44(0)

(disponible en postscript de http://faculty.uml.edu/jpropp/articles.html)

Da una descripción cuidadosa del tipo de construcción deseada . Un asesino ejemplo de que el papel: Si P es el permutaciones de un conjunto y L lineal órdenes de que se establece a continuación no es natural bijection de L a P (incluso si el conjunto tiene 3 elementos) porque no es un distinguido permutación (la identidad), pero no se distingue orden lineal. Sin embargo, hay una natural bijection de LxL a PxL el uso de la línea 2 de la notación.

El artículo está escrito en un estilo relajado y tiene una nota de pie de página indicando que Conway podría no ser cometido cada observación y el detalle de la exposición.

En realidad, la observación de que

• desde 3a=3b implica a=b en la aritmética finita...para finito de conjuntos de un bijection de Ax3 a Bx3 debe ceder a uno de a a B

es sospechoso para mí (porque en el ejemplo de arriba).

Answer 4

La prueba es que no constructivo, se hace en algo como ZF (con la lógica clásica). Por ejemplo, la prueba de Tarski del Lexema en la página 27 se inicia con:

"Si $A \succeq B$ (hay una inyección de $B \to A$), entonces no es $C$ tal que $A \cong B + C$ (hay un bijection $A \to B + C$), es decir, el complemento de la imagen de $B$ en algunas de inyección de $B$ a $A$."

Se trata de un fondo clásico paso, como puede ocurrir fácilmente intuitionistically que hay una inyección de $B \to A$ de manera tal que el complemento de su imagen está vacío, pero no hay bijection entre el $B$ e $A$. Todo el papel tiene muchas de esas clásicas pasos. No estoy de acuerdo con Aaron declaración de que la prueba "se muestra que la construyó bijections (...) son tan explícitas como en los ingredientes, pero no más". No se puede parametrizar clásicas pruebas como de, al menos no fácilmente.