Estoy seguro de que hay maneras fáciles de probar cosas usando, bien... cualquier otro método además de esto! Pero aún así, tengo curiosidad por saber si sería aceptable/si se ha hecho antes?
Respuestas
¿Demasiados anuncios?
Hay un decepcionante manera de responder a su pregunta de manera afirmativa: Si $\phi$ es una afirmación que de Primer orden de la Aritmética de Peano $\mathsf{PA}$ prueba "$\phi$ es demostrable", entonces, en el hecho de $\mathsf{PA}$ también demuestra que $\phi$. Puede reemplazar aquí $\mathsf{PA}$ con $\mathsf{ZF}$ (Zermelo Fraenkel de la teoría de conjuntos) o su costumbre favorita o de primer orden de la formalización de las matemáticas. En un sentido, esto es exactamente lo que pedían: Si podemos demostrar que no es una prueba, entonces no es una prueba. Por otro lado, esto es en realidad insatisfactoria porque no se conocen ejemplos naturales de las declaraciones de $\phi$ para el que es más fácil demostrar que no es una prueba en lugar de encontrar.
(El de arriba tiene una cuidada formal de la contraparte, el teorema de Löb, que establece que si $\mathsf{PA}$ se puede probar "Si $\phi$ es demostrable, entonces $\phi$", entonces, en el hecho de $\mathsf{PA}$ se puede demostrar que $\phi$.)
Hay otras maneras de responder afirmativamente a su pregunta. Por ejemplo, es un teorema de $\mathsf{ZF}$ que, si $\phi$ es $\Pi^0_1 instrucción de$ y $\mathsf{PA}$ no demostrar su negación, entonces $\phi$ es cierto. Sea $\Pi^0_1$ significa que $\phi$ es de la forma "Para todos los números naturales $n$, $R(n)$", donde $R$ es recursivo declaración (es decir, no hay un algoritmo que, para cada entrada $n$, devuelve en una cantidad finita de tiempo si $R(n)$ es verdadero o falso). Muchos naturales y declaraciones interesantes son $\Pi^0_1$: La hipótesis de Riemann, la conjetura de Goldbach, etc. Sería fantástico para verificar algunos de esos $\phi$ de esta manera. Por otro lado, no hay escenario para lograr algo como esto.
La clave para los resultados anteriores es que $\mathsf{PA}$ y $\mathsf{ZF}$, y razonable a la formalización de las matemáticas, son aritméticamente sonido, lo que significa que sus teoremas acerca de los números naturales son en realidad verdaderos en el modelo estándar de la aritmética. El primer párrafo es una consecuencia de la aritmética solidez. El tercer párrafo es una consecuencia del hecho de que $\mathsf{PA}$ se demuestra todos los verdaderos $\Sigma^0_1$-declaraciones. (Mucho menos que $\mathsf{PA}$ es suficiente aquí, por lo general se refiere a la aritmética de Robinson $Q$.) No recuerdo si esta propiedad tiene un nombre estándar.
Aquí hay dos mensajes relacionados con MO:
Mrsonord
Puntos
111
Yo diría que el modelo teórico de la prueba de la Ax-teorema de Grothendieck cae en esta categoría. Puede haber otras formas de probarlo, pero esta es la única prueba de que he visto en la escuela de posgrado, y es bastante natural si sabes el modelo de la teoría.
El teorema establece que para cualquier polinomio de mapa $f:\mathbb{C}^n \to\mathbb{C}^n$, si $f$ es inyectiva (uno a uno), entonces es surjective (a). El teorema de usos varios resultados en el modelo de la teoría, y el argumento es más o menos la siguiente.
Deje de $ACL_p$ denotar la teoría de la algebraicamente cerrado campos de la característica de $p$. $ACL_0$ es axiomatized por los axiomas de un algebraicamente cerrado de campo y el axioma esquema de $\psi_2, \psi_3, \psi_4,\ldots$, donde $\psi_k$ es la declaración "para todo $x \neq 0$, $k x \neq 0$". Tenga en cuenta que la totalidad de los $\psi_k$ son también confirmado por $ACL_p$, si $p$ no dividir $k$.
- El teorema es verdadero en $ACL_p$, $p>0$. Esto puede ser fácilmente demostrado por la contradicción: se supone que un contador de ejemplo, a continuación, tomar el campo finito generado por los elementos de la contra-ejemplo, llamar a ese campo finito $F_0$. Desde $F_0^n\subseteq F^n$ es finito, y el mapa es inyectiva, debe ser surjective así.
- La teoría de la algebraicamente cerrado campos en el carácter $p$ es completa (es decir, el estándar de axiomas probar o refutar todas las declaraciones que se puede expresar en primer lugar el lenguaje de los anillos).
- Para cada grado $d$ y dimensión $n$, restringir Ax-Grothendieck a una instrucción $\phi_{d,n}$, que es expresable como una declaración en el primer fin de lenguaje de los anillos. Entonces $\phi_{d,n}$ es comprobable en $ACL_p$ para todos los caracteres $p > 0$.
- Asumir la $\phi_{d,n}$ es falsa para $p=0$. Luego por la integridad, hay una prueba de $P$ de $\neg \phi_{d,n}$ en $ALC_0$. Por la finitud de las pruebas, existe un subconjunto finito de axiomas para $ACL_0$ que se utilizan en esta prueba. Si ninguno de los $\psi_k$ son $P$, entonces $\neg \phi_{d,n}$ es cierto que de todos los algebraicamente cerrado campos, que no puede ser el caso (2). Deje de $k_0,\ldots, k_m$ la obtención de índices de $\psi_k$ usa en $P$. Escoge un prime $p_0$ que no divida a cualquier de $k_0,\ldots,k_m$. A continuación, todos los axiomas utilizados en $P$ también $ACL_{p_0}$. Mus $ACL_{p_0}$ también demuestra que $\neg \phi_{d,n}$, además de contradecir (2). Contradicción. Por lo tanto, no es una prueba de $\phi_{d,n}$ en $ACL_0$.
Así que la prueba es en realidad a lo largo de las líneas de "para cada grado $d$ y dimensión $n$ no es una prueba de que el Ax-teorema de Grothendieck restringido a ese grado y dimensión". Lo que ninguna de esas pruebas, no tengo idea.
