Esto puede ser un tramo, pero hay ejemplos de pruebas que demuestran que es una prueba de que existe un teorema.
Por ejemplo, si a es un teorema, y es demasiado tedioso para demostrar que es posible demostrar que una prueba de que existe por el teorema A.
Algo a lo largo de las líneas de Andrés comentario:
Suponga que usted se asigne a cada fórmula en la aritmética (por ejemplo, $0 = 0$) un número Natural único en una manera tal que usted podría mecánicamente averiguar qué fórmula correspondieron a que número Natural. A continuación, para cualquier constante (no contradictorio) la teoría de la $T$ que incluye a las 15 reglas básicas de la aritmética de PA- y sólo incluye afirmaciones verdaderas acerca de los números Naturales, habrá alguna fórmula $Prov_T(x)$ lo que representa provability de $T$ bajo esta codificación. En particular, esto significa que si $\varphi_n$ es una fórmula asigna número Natural $n$ bajo nuestro mecánica procedimiento de codificación y $T \vdash Prov_T(n)$ ("T demuestra que $\varphi_n$ es comprobable"), a continuación, $T \vdash \varphi_n$ ("prueba T $\varphi_n$"). La representatividad de provability también significa que si $T \vdash \lnot Prov_T(n)$ ("$T$ demuestra que $\varphi_n$ no es demostrable"), entonces $T \nvdash \varphi_n$ ("$T$ no prueban $\varphi_n$").
Por cierto, Gödel primer teorema de la incompletitud implica que habrá una declaración de $\varphi_n$, de modo que cualquier (constante) de un conjunto de "identificación personal" axiomas $T$ verdadera en los números Naturales que incluye a todos aquellos que se encuentran en el PA- no puede probar la $\varphi_n$ ni $\lnot\varphi_n$. De hecho, esta declaración fue de la forma $\lnot Prov_T(m)$ para algún número Natural $m$. Si $T$ también incluye todos los axiomas de la plena Aritmética de Peano, entonces por Gödel del segundo teorema de la incompletitud, podemos encontrar una declaración utilizando cualquier número Natural $m$ codificación de una declaración de $\lnot\varphi$ donde $\varphi$ es en realidad comprobable de $T$.
Creo que un ejemplo de lo que hablamos es de la constante de aplicaciones del Teorema de la Deducción que están implícitos en la mayoría de las matemáticas; la Deducción del Teorema que dice que si usted puede probar $B$$\Delta\cup\{A\}$, luego de $\Delta$ usted puede probar $A\rightarrow B$: $$\Delta\cup \{A\}\models B \Longrightarrow \Delta\models A\rightarrow B.$$ Hofstadter, en Goedel, Escher y Bach, la llama "la fantasía de la regla", porque en el fin de demostrar que $A\rightarrow B$ mantiene, se llega a fantasear con que usted realmente sabe $A$ es verdadera y, a continuación, probar $B$.
La prueba de la Deducción del Teorema de la realidad le dice a usted cómo tomar una prueba de $B$ $\Delta\cup\{A\}$ y usarlo para producir una prueba de $A\rightarrow B$$\Delta$. El procedimiento es mecánico, pero algo involucrados; una breve prueba de $B$ $\Delta\cup\{A\}$ le suele dar un poco larga la prueba de $A\rightarrow B$$\Delta$.
En un sentido, casi cada vez que se prueba un teorema en realidad no estamos demostrando el teorema; la gran mayoría de los teoremas son de la forma $\Delta\models A\rightarrow B$, pero casi invariablemente demostrar $\Delta\cup\{A\}\models B$ (cuando un teorema que dice algo así como "Si $A$ $B$ son disjuntos, entonces $|A\cup B|=|A|+|B|$", entonces la prueba se suelen empezar con "Supongamos que $A$ $B$ son distintos..."). Cuando lo hacemos, lo que hemos hecho es demostrar que es una prueba de que existe, sin llegar a proporcionar la prueba de la proposición pretendemos estar probando.
No son similares "Metatheorems" para otros típico de las reglas de la prueba de argumentos, como pruebas de los casos de prueba por contradicción, etc.
Si una teoría de la $T$ demuestra una frase $\varphi$ y es lo suficientemente fuerte aritméticamente (es decir que incluye a $PA$), entonces se puede demostrar dentro de $T$ que no es una prueba de $\varphi$.
Por otro lado, una teoría de la $T$ podría ser capaz de demostrar que una fórmula $\varphi$ tiene una "prueba", mientras que la teoría de la $T$ no puede probar la $\varphi$, en el hecho de $T$ podría demostrar que un enunciado tiene una prueba, mientras que no hay ninguna prueba en absoluto (me refiero a que la declaración de que $\varphi$ tiene una prueba de que es falso en el modelo estándar). Sin embargo, esto no sucede en la práctica, porque las teorías que usamos en matemáticas son: 1-consistente (o al menos cree así), es decir, $\Sigma_1$ fórmula demostrable en $T$ es realmente cierto.
También se puede preguntar si hay pruebas de que son demasiado tiempo para escribir, pero podemos prueba de su existencia, y la respuesta es también positivo.
Seguro. Por ejemplo, utilizando el teorema de completitud, mostrando que una declaración es semánticamente cierto es equivalente a que demuestre que cuenta con un sintáctico de la prueba, aunque no tienen que dar un sintáctico de la prueba. Por ejemplo (!), usted puede demostrar que una declaración en cero-el fin de la lógica es una tautología, argumentando por la contradicción, y se sigue por el teorema de completitud de que la tautología tiene una prueba a partir de los axiomas de cero-el fin de la lógica.
Yo no puedo pensar inmediatamente en cualquiera de los ejemplos de "real" teoremas con esta propiedad, pero aquí es una manera de generar una clase de ellos: supongamos que usted puede reducir un infinitary declaración a la comprobación de un número finito de casos. Luego, sin la comprobación de las mismas, usted sabe que el acto de la comprobación de las mismas corresponde a la prueba de algunos teorema pesar de que sabe que ninguno de los dos (todos los pasos) de la prueba ni el teorema! Tal vez usted quiere saber el teorema así, sin embargo.
También existe la idea de un conocimiento cero de la prueba. Esto podría no ser exactamente lo que tenía en mente, aunque, como es interactivo y probabilístico.
Pensándolo bien, sin una clara distinción entre la primera y la segunda de los usos de la palabra "prueba" en su pregunta (como se hace por el primer ejemplo de arriba), no estoy seguro de cuál es la diferencia entre tener una prueba y tener una prueba de que una prueba que existe es.
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
