¿Por qué las pruebas no pueden tener infinitos pasos?

Question

Recientemente vi la prueba de lo finito axioma de elección de los axiomas de ZF. La idea básica de la prueba es la siguiente (voy a cubrir el caso en que estamos eligiendo entre tres sets, pero la idea general es evidente): Supongamos que tenemos $A,B,C$ no vacío, y nos gustaría mostrar que el producto Cartesiano $A \times B \times C$ no está vacía. Entonces $\exists a \in A$, $\exists b \in B$, $\exists c \in C$, todo debido a que cada conjunto es no vacío. A continuación, $a \times b \times c$ es un elemento deseado de $A \times B \times C$, y hemos terminado.

En el caso de que hayamos infinitamente (en este caso, countably) muchos conjuntos, decir $A_1 \times A_2 \times A_3 \times \cdots$, podemos tratar de la misma prueba. Pero en el fin de utilizar sólo los axiomas de ZF, la prueba requiere la infinidad de pasos $\exists a_1 \in A_1$, $\exists a_2 \in A_2$, $\exists a_3 \in A_3$, $\cdots$

Mi pregunta es, ¿por qué no podemos hacer esto? O una redacción mejor, ya sé que los matemáticos trabajan normalmente en sistemas lógicos en los que sólo finita pruebas son permitidas, es: ¿hay algún tipo de forma de hacer la lógica en la que infinitamente largo pruebas como estas están permitidas?

Una objeción válida a tal sistema sería que nos permitan demostrar el Último Teorema de Fermat como sigue: Considerar cada par $(a,b,c,n)$ como un paso en las pruebas, y luego usamos countably muchos pasos para mostrar que el teorema es verdadero.

Yo podría argumentar que esto realmente es una prueba válida - simplemente no es posible en nuestro universo donde sólo podemos hacer finitely-muchos cálculos. Así que podría sugerir un sistema de lógica en el que una prueba como esta es válida.

Por otro lado, creo que la "prueba" de Último Teorema de Fermat, que utiliza una infinidad de pasos es muy diferente de la "prueba" de AC de ZF que utiliza una infinidad de pasos. En la prueba de CA, sabemos cómo cada paso funciona, y sabemos que va a tener éxito, incluso sin tener en cuenta que el paso de forma individual. En otras palabras, sabemos lo que queremos decir por la concatenación de pasos $(\exists a_i \in A_i)_{i \in \mathbb{N}}$. Por otro lado, no podemos, antes de hacer todo el infinitamente muchos de los pasos de la prueba de la FLT, saber que cada paso se va a trabajar. Lo que estoy sugiriendo en este párrafo es un sistema de lógica en la cual la prueba de la CA de arriba es una prueba aceptable, mientras que la prueba de la FLT descrito anteriormente no es aceptable.

Por eso me pregunto si el sistema de la lógica ha sido considerada, o si alguno de los expertos aquí tiene una idea de cómo podría funcionar, si no ha sido considerado. Y, por supuesto, no podría ser un mejor término de "sistema de lógica", y otros pueden dar sugerencias para que.

Answer 1

Incluso si la lógica se extiende a permitir infinitamente larga pruebas, su intento de prueba de los contables axioma de elección sería todavía tiene un hueco o dos. Después de la infinidad de pasos afirmar que existe una $a_i$ en $A_i$ (un paso por cada una de las $i$), usted todavía necesita para justificar la afirmación de que hay una función de asignación, para cada una de las $i$, el correspondiente $a_i$. El problema inmediato es que su infinidad de pasos no exactamente especificado que (de las muchas posibles) $a_i$'s son los correspondientes; el $a_i$'s en sus fórmulas son sólo variables vinculadas. Peor aún, incluso si el significado de "el correspondiente $a_i$" eran perfectamente clara, por lo que no hay duda acerca de que los pares ordenados $(i,a_i)$ desea tener en su función de elección, usted todavía necesita para demostrar que existe un conjunto que consta de sólo los pares ordenados. No ZF axioma hace ese trabajo. Creo que sería necesario un infinitamente larga axioma diciendo: "para todos los $x_1,x_2,\dots$, existe un conjunto cuyos miembros son exactamente $x_1,x_2,\dots$."

Si usted está dispuesto a aceptar no sólo las pruebas de que consta de una infinidad de declaraciones, pero también las declaraciones de longitud infinita, y si usted está dispuesto a añadir algo de infinito de declaraciones como nuevos axiomas, entonces creo que se puede "probar" el contable axioma de elección (y más elegante elección principios, si usted permite que incluso los más nuevos axiomas). Pero, como el tiempo necesario para agregar algunos axiomas de ZF para este propósito, parece más sencillo añadir la de contable axioma de elección. Es de un número finito de instrucción, de modo que usted puede razonar con él mediante las habituales reglas de la lógica.

Uno podría ver el axioma de elección como una especie de finitary (y por lo tanto utilizable) sustituto para el infinitamente larga axiomas y las pruebas que vendrían en su enfoque. De hecho, algunos de Zermelo la obra posterior (él introdujo el axioma de elección en 1904, y el trabajo que yo estoy pensando en las fechas de finales de la década de los 20's o principios de los 30's) toma un "infinitary lógica" aproximación a los fundamentos de la teoría de conjuntos (y es, en mi opinión, no está del todo claro).

Answer 2

Andreas Blass tiene muy bien explicado por qué no es útil para su uso infinitary lógica en un intento de demostrar el axioma de elección.

Cabe agregar que la aparentemente similares idea, de considerando countably infinito pruebas en la teoría de los números, es útil en una forma (aunque no para probar FLT!). El llamado $\omega$-regla - de las pruebas de $\varphi(0),\varphi(1), \varphi(2),\ldots$ to infer $\forall n\varphi(n)$ -- fue utilizado por Schütte alrededor de 1950 para simplificar Gentzen 1936 consistencia la prueba de la aritmética de Peano, PA.

Asumiendo $\varepsilon_0$-inducción, resulta ser más fácil para probar la consistencia de un sistema de PA$_\omega$ con el $\omega$-regla de probar la consistencia del sistema de PA que contiene.

Answer 3

Su ejemplo sobre el teorema de Fermat muestra por qué no podemos hacer infinitas pruebas: su prueba de la estrategia es comprobar infinitamente muchos casos, que un ser humano puede hacer en una cantidad finita de tiempo. Por lo tanto, sólo aceptamos pruebas tratar con infinitamente muchos casos si tenemos algunos finito (finitistic) manera de razonar acerca de todas estas instancias, por ejemplo, mediante la inducción.

El hecho de que AC no se sigue el Zermelo-Fraenkel axiomas, CA contables para las familias de conjuntos, muestra que en primer orden la lógica no podemos hacer infinitary pruebas como usted sugiere. Pero primero el fin de la lógica es bastante único con respecto a sus propiedades atractivas.

Richard Borcherds menciona infinitary lógica, lo que sin duda tiene sus usos, pero no la puedo ver cómo usted puede utilizar infinitary lógica para demostrar casos de CA, si la base de su teoría es, digamos, ZF.
(Todos los de primer orden de la frase es también una frase en infinitary lógica.)
Infinitary lógica podría hablar, por ejemplo, acerca de la infinidad de clases al mismo tiempo, pero si usted comienza a partir de ZF, el infinitary lógica (es decir $L_{\omega_1,\omega_1}$ para ser específicos) generados a partir tendrá los mismos modelos como de costumbre, de la lógica de primer orden. Si agrega infinitary axiomas que permitan acreditar más instancias de CA, esto significa que usted acaba de añadir instancias de CA a su axiomas (posiblemente instancias que no podía formular por finitary de primer orden de los axiomas).

Answer 4

James Brotherston y Alex Simpson trabajado en la no-bien fundado de las pruebas, ver

J. Brotherston y A. Simpson: Sequent cálculos para la inducción y el descenso infinito. J Lógica De La Computación (2010)

así como el hablar "En la Prueba por el Descenso Infinito" por Alex Simpson en "Álgebra y Coalgebra cumplir con la Prueba de la Teoría" en Berna, abril de 2012.

Answer 5

http://en.wikipedia.org/wiki/Infinitary_logic