Hay dos diferentes nociones de la prueba de que otras respuestas no se distingue.
Las pruebas de 'sin'
Una de ellas es cuando estamos en un meta-sistema, y hablando de pruebas dentro de un sistema formal. Por ejemplo, el teorema de completitud de la lógica de primer orden, dice que para cualquier conjunto $S$ de fórmulas y la fórmula de $f$, tenemos $S \vdash φ$ si y sólo si $S \vDash φ$, lo que en inglés dice que tenemos desde $S$ derivar $ø$ si y sólo si cada modelo de la satisfacción de $S$ también satisface $f$. Esto es sorprendente a primera, ya que establece que cada lógicamente consecuencia necesaria de la $S$ (que es una cuestión semántica), en realidad es derivable (que es un sintáctica de la materia). Esto de alguna manera responde a su pregunta, porque la prueba de la integridad es el teorema de no-constructiva en algún sentido (usa débil Konig del lema).
El teorema de completitud tiene importantes consecuencias obvias, y es que si $S \vDash \bot$, entonces $S \vdash \bot$, lo que en inglés dice que si $S$ es unsatisfiable (cualquier modelo), a continuación, a partir de $S$ en realidad podemos derivar una contradicción. Esto es útil porque derivaciones son siempre finitos secuencias de pasos deductivos, cada uno de los cuales el uso de un número finito dado anteriormente o derivados de sentencias, por lo que cualquier derivación de $S$ usa sólo un número finito de oraciones a partir de $S$. Por lo tanto, si $S \vdash \bot$ entonces no es en realidad un subconjunto finito de $T$ de $S$ que $T \vdash \bot$. Ahora desde nuestras reglas deductivas son el sonido, también sabemos que $T \vDash \bot$. Por lo tanto, cualquier unsatisfiable conjunto de oraciones tiene un subconjunto finito que ya es unsatisfiable. Este es el teorema de compacidad, que es una muy útil herramienta para probar los hechos acerca de la lógica de primer orden.
Por supuesto, hay también los resultados en la lógica sobre cómo realizar pruebas de una estructura a otra. Por ejemplo, dada cualquier isomorfo estructuras sobre el mismo idioma, cualquier frase es comprobable por uno si y sólo si es comprobable por el otro. Esto puede ser usado para mostrar, por ejemplo, que $i$ no es definible por una de primer orden de la fórmula de más de $\mathbb{C}$, es decir, que no hay ninguna fórmula $ø$ tal que para todo $x \in \mathbb{C}$ tenemos que $f(x)$ es verdadera si y sólo si $x = i$, ya que el complejo de la conjugación es un isomorfismo que asigna $i$ a $-i$.
$\def\nn{\mathbb{N}}$
$\def\imp{\rightarrow}$
Pruebas 'desde dentro'
La otra noción de la prueba surge cuando el sistema formal bajo consideración es agradable, lo que significa que es lo suficientemente fuerte como para manipular finito de cadenas, y uno mediante algoritmos puede verificar si una cadena es una prueba válida. Cualquier buen sistema formal puede razonar (en cierta medida) acerca de las pruebas en sí mismo, y uno tan bonito sistema formal es la Aritmética de Peano, porque hay trucos para codificar cadenas de caracteres como números naturales y extraer de una codificación de una cadena el símbolo en cualquier posición arbitraria. Un excelente libro gratis en linea es Gödel sin lágrimas, que describe todos estos como los preliminares necesarios para probar la incompletitud de Gödel teoremas.
Todavía tenemos que trabajar en exteriores, en un meta-sistema, que ya se sabe que $\nn$ en el fin de definir "$\square_T φ$", como algunos de primer orden de la fórmula través de un sistema formal de $T$ que es cierto en $\nn$ si y sólo si $T \vdash φ$, lo que la fórmula es construido por decir en el idioma de $T$ "Hay una cadena que representa una prueba de $f$.". Tenga en cuenta que esta construcción es totalmente constructivo y puede ser realizado por un equipo dado cualquier entrada de la forma $f$, a pesar de que la fórmula resultante es gigantesca para algunos sistemas formales como $PA$ y $ZFC$.
Por comodidad vamos a escribir "$T \vdash \cdots \square φ \cdots$" en lugar de "$T \vdash \cdots \square_T φ \cdots$". Resulta que cada buen sistema formal de $T$ satisface las siguientes 4 condiciones:
-
(F) Modal de punto fijo axioma: Para cualquier formula $P$, con sólo uno libre proposicional variable, no es una fórmula de $α$ tales que $T \vdash α \leftrightarrow P(\square α)$.
-
(D1) Derivability condición 1: Para cualquier fórmula de $α$, si $T \vdash α$ entonces $T \vdash \square α$.
-
(D2) Derivability condición 2: Para cualquier fórmula de $α,β$ tenemos $T \vdash \square α \de la tierra \square( α \imp β ) \imp \square β$.
-
(D3) Derivability condición 3: Para cualquier fórmula de $α$ tenemos $T \vdash \square α \imp \square \square α$.
El uso de "$\square$" es explícitamente la captura de las propiedades de derivability en la forma de una lógica modal, en el sentido de que ya no tenemos a la atención de lo exacto de primer orden de la fórmula "$\square_T φ$" denota, y, de hecho, puede extender $T$ a un nuevo sistema formal $T'$ "$\square$" como un nuevo símbolo interno como "$\forall$" y "$\exists$". De esta manera podemos, en cierto sentido, decir que $T'$ en realidad puede que internamente se refieren a la noción de provability en $T$.
La consistencia de $T$ es equivalente a "$T \nvdash \bot$", que puede representarse internamente dentro de los $T$ "$\neg \square_T \bot$", y de esta fórmula está en la meta-lógica denotado por $Con(T)$. Gödel demostró que si $T$ es un buen primer orden formal del sistema que es el omega-consistente (hay un modelo que tiene exactamente los mismos números naturales (equivalentemente, cadenas) como el meta-sistema), luego $Con(T)$ es independiente de $T$, lo que significa que $T \nvdash Con(T)$ y también $T \nvdash \neg Con(T)$. Por el teorema de completitud, esto implica entonces que $( T + Con(T) )$ es consistente, y $( T + \neg Con(T) )$ es también coherente.
Es esto sorprendente? Esto no contradice el teorema de completitud, pero implica que existen diferentes modelos de $T$, algunas satisfacciones $Con(T)$ y algunas satisfacciones $\neg Con(T)$. Por ejemplo, en el meta-sistema $\nn$ es el llamado modelo estándar de $PA$, que satisface $Con(PA)$, pero hay también modelos estándar de $PA$, algunos de los cuales satisfacer $\neg Con(PA)$ en su lugar.
Lo anterior es conocido como el Gödel teorema de la incompletitud. Rosser mostró que incluso si dejamos caer la condición de que $T$ es el omega-de acuerdo, todavía hay alguna frase que es independiente de $T$, aunque $Con(T)$ no pueden ser independientes ya que, como veremos en un ejemplo posterior.
Curiosamente, una versión interna puede ser probada utilizando sólo (F) y (D1) y (D3), es decir, $T \vdash Con(T) \imp \neg \cuadrado Con(T)$, equivalente a $T \vdash \cuadrado Con(T) \imp \neg Con(T) dólares, o el uso de sólo los cuadros, $T \vdash \square \neg \square \bot \imp \square \bot$. Si tenemos que volver a escribir equivalentemente como $T \vdash \square( \square \bot \imp \bot ) \imp \square \bot$, entonces es claramente un caso especial de la unidad de negocio del teorema, es decir, que para cualquier oración que $f$ tenemos $T \vdash \square( \square φ \imp φ ) \imp \square φ$, lo que también puede ser demostrado a partir de las 4 condiciones solo.
Con las bases en su lugar, ahora nos podemos preguntar preguntas interesantes. Es a la inversa (D1) cierto? Sí si $T$ es satisfecho por $\nn$, por la construcción de $\square_T$, pero no necesariamente en general, incluso si $T$ es constante. Por ejemplo, supongamos $PA' = PA + \neg Con(PA)$. Entonces $PA'$ es constante, equivalente a $PA' \nvdash \bot$. Pero $PA' \vdash \square_{PA} \bot$ y por lo tanto (después de un poco de trabajo) $PA' \vdash \square_{PA'}\bot$. Extraño, $PA'$ parece decir que sí es incoherente, aunque no lo es! La razón es que cada modelo de $PA'$ es un no-modelo estándar de $PA$. Cada modelo de $PA$ tiene un elemento estándar para cada término de la forma "$1+1+\cdots+1$", pero no estándar de los modelos de tener más elementos no convencionales. En cualquier modelo de $PA'$ la frase existencial $\square_{PA'} \bot$ es presenciado por una no-estándar elemento, y nunca se puede encontrar un estándar testimonio de que podemos decodificar para obtener una prueba real de la contradicción en $PA'$.
En resumen, las consideraciones anteriores muestran que $PA'$ es constante sino que deriva de "la existencia de una prueba de la contradicción", pero en realidad no hay tal prueba si $PA$ es constante. Este es un tipo diferente de respuesta a su pregunta, pero puede ser vale la pena pensar. Esto también implica que la consistencia de un sistema formal no es en absoluto suficiente para justificarlo, ya que no quieren "probar sí mismas, incompatibles'.
A continuación, es el 'conversar' de (D3) verdadero, es decir, es cierto que $T \vdash \square \square φ \imp \square φ$ para cualquier frase φ? Resulta que también es falso, porque $PA \nvdash \square \square \bot \imp \square \bot$, de lo contrario por parte de la unidad de negocio del teorema de $PA \vdash \square \bot$, lo cual es imposible porque el modelo estándar de PA no satisface "$\square \bot$".
Por último, observe que (D1) y (D3) estaría implicado por una regla (C), que indica que $T \vdash α \imp \square α$ para cualquier fórmula de $α$. Sin embargo, (C) no es válido para cualquier agradable omega consistente en el sistema formal de $T$, porque de lo contrario $T \vdash Con(T) \imp \cuadrado Con(T)$ y por tanto $T \vdash \neg Con(T)$, contradiciendo teorema de la incompletitud de Gödel.
Todos estos nos muestran que lo que un sistema formal puede "saber" acerca de las pruebas en sí mismo es muy limitada, y que siempre se necesita para trabajar en un meta-sistema, que "sabe" más en algún aspecto si uno quiere una imagen completa de provability.
