Pruebas cuya longitud depende de la entrada

Question

Esto puede ser una pregunta de la teoría de la prueba, pero no estoy seguro, ya que no conozco ninguna teoría de la prueba. Lo que voy a preguntar es lo que sucede, si la longitud de una prueba no es fijo: Voy a presentar una estructura de una prueba, donde esto sucede:

Supongamos que tengo $n$ objetos $O_1,\ldots,O_n$ que están relacionados entre sí por alguna relación $R$ (que es independiente del orden de estos objetos) y quiero demostrar que puedo reemplazar estos $n$ objetos por algún otro $n$ objetos $O'_1,\ldots,O'_n$ que satisfacen la misma relación $R$ y que la prueba está estructurada de la siguiente manera:

Primero pruebo que puedo sustituir el primero de los objetos originales por el nuevo objeto, de forma que el $O'_1,O_2,\ldots,O_n$ por lo que obtenidos también satisfacen $R$ .

Entonces sostengo, que en el curso de la obtención de $O'_1,O_2,\ldots,O_n$ de $O_1,\ldots,O_n$ Sólo he utilizado el hecho de que satisfacen $R$ y no utilizó ninguna de las propiedades un singular $O_i$ tiene. Esto me permite copiar la primera prueba, donde obtuve la secuencia $O'_1,O_2,\ldots,O_n$ de objetos y reemplazarlos (renombrarlos) de la siguiente manera: $O'_1 \rightarrow O_2 $ , $O_2 \rightarrow O_3 $ , $\ldots$ , $O_n \rightarrow O'_1 $ es decir $O'_1,O_2,\ldots,O_n$ se convierte en $O_2,\ldots,O_n,O'_1$ . Esto sustituiría el primer objeto de esta secuencia por uno nuevo, de modo que obtendría la secuencia $O'_2,O_3,\ldots,O_n,O'_1$ .

Entonces digo que "repetimos este proceso otro $n-2$ veces" para obtener $O'_n,O'_1,\ldots,O_{n-1}$ Satisfaciendo a $R$ Reordenarla para que sea $O'_1,O_2,\ldots,O'_n$ y se hicieron.

El problema que tengo con esta prueba es que su longitud depende de $n$ ya que a cada paso, en el que me consigo un nuevo objeto $O'_i$ En este caso, añado una porción de texto a la prueba escrita hasta ahora, que explica cómo obtengo este nuevo objeto en la secuencia. Esto me parece problemático, ya que estoy acostumbrado a que las pruebas tengan una longitud fija, pero el hecho de que la porción de texto que añado a mi prueba se obtenga de forma totalmente mecánica/algorítmica a partir de las partes de texto anteriores (sólo se cambian los nombres de algunos símbolos), me tranquiliza un poco.

Así que pregunto lo siguiente: 1) ¿Están permitidas las pruebas de este tipo? 2) Si la respuesta es afirmativa, ¿qué pasaría si la prueba no se expandiera de forma mecánica/algorítmica, y sólo hubiera que sustituir los símbolos antes de añadir la nueva parte de la prueba (como se ha explicado anteriormente)? (Sea lo que sea, esta segunda pregunta es más bien un experimento mental). 3) ¿Hay alguna manera de hacer que esta prueba sea de longitud fija?

Answer 1

Ha descubierto la diferencia entre un teorema y un esquema del teorema . Lo que tenemos aquí es un esquema con infinitos teoremas e infinitas pruebas, parametrizado por el entero positivo $n$ . Esto no garantiza que haya una única prueba que cubra todos los casos. Su argumento utiliza externo inducción en $n$ para demostrar que existe una prueba para cada número entero positivo $n$ . La inducción se llama "externa" porque se realiza en la metateoría y no en la propia teoría. Es posible que la teoría en la que estás trabajando ni siquiera tenga números enteros positivos y, aunque los tenga, puede que no sea capaz de formalizar esta inducción internamente.

A menudo se ignora la sutil diferencia entre la inducción externa y la interna en las matemáticas cotidianas, pero la diferencia se vuelve importante en los entornos formales y esos resultados pueden ser muy confusos. El sitio web Teorema de la reflexión en la teoría de conjuntos es un ejemplo de ello. Este esquema dice que para cada fórmula $\phi(v_1,\dots,v_k)$ en el lenguaje de la teoría de conjuntos lo siguiente es demostrable en ZFC:

Para todos los conjuntos $x_1,\dots,x_k$ si $\phi(x_1,\dots,x_k)$ es verdadera, entonces hay un ordinal $\alpha$ tal que $x_1,\dots,x_k \in V_\alpha$ y $V_\alpha \vDash \phi(x_1,\dots,x_k)$ .

Nótese que se trata de un teorema para cada fórmula $\phi(v_1,\dots,v_k)$ . No se puede probar en ZFC que:

Para cada fórmula $\phi(v_1,\dots,v_k)$ todos los conjuntos $x_1,\dots,x_k$ si $\phi(x_1,\dots,x_k)$ es verdadera, entonces hay un ordinal $\alpha$ tal que $x_1,\dots,x_k \in V_\alpha$ y $V_\alpha \vDash \phi(x_1,\dots,x_k)$ .

De hecho, si esto fuera cierto, entonces toda lista finita de axiomas de ZFC sería satisfacible y, por tanto, por la Teorema de la compacidad ZFC sería satisfacible (y por tanto consistente). Pero sabemos que ZFC no puede demostrar su propia consistencia mediante Teorema de Incompletitud de Gödel Por lo tanto, el esquema de reflexión no puede ser internalizado en ZFC, incluso si ZFC puede internalizar la mayoría de los usos comunes de la inducción.