Supongamos que $S, T$ son dos teorías en el lenguaje de la teoría de conjuntos, y supongo que demostrar - mediante relativización de los conceptos, por ejemplo - que $\operatorname{Con}(S) \rightarrow \operatorname{Con}(T)$. Los resultados de esto, me parece, a menos que ambas teorías son finitos, para ser un resultado en la metatheory, en el sentido de que es imposible demostrar que $\mathsf{ZF} \vdash \operatorname{Con}(S) \rightarrow \operatorname{Con}(T)$. Parece que de esta manera porque, dado un modelo de clase de $\mathcal{M}$, $\mathcal{M} \vDash S$ es generalmente una declaración de que no puede ser formalizado en el $\mathsf{ZF}$. ¿Es esto correcto?
Respuestas
¿Demasiados anuncios?
Sí. La consistencia de los resultados son meta-teoremas. No se trata de las implicaciones de las sentencias en el lenguaje, sino más bien acerca de las propiedades de las teorías, que son objetos de la meta-teoría.
Ahora, en los comentarios que expresan una cierta confusión acerca de la meta-teoría que es $\sf PA$ o $\sf ZF$ o algo más. En la práctica esto no importa. Si se puede interpretar de una teoría de la $T$ en una teoría de la $S$, entonces todas las pruebas de $T$ puede ser traducido así. En particular, $\sf PA$ puede ser interpretado en $\sf ZF$, así que cualquier cosa que usted puede hacer en $\sf PA$ como una meta-teoría, puede de hecho hacer en $\sf ZF$. En realidad, $\sf PA$ es demasiado fuerte para la mayoría de las cosas que usted quiere una meta-teoría que hacer, y $\sf PRA$ (Primitiva Recursiva Aritmética) es realmente suficiente.
Pero $\sf ZF$ nos ofrece más. Nos ofrece modelos y semántica, y Gödel integridad del teorema que nos dice que $\operatorname{Con}(S)$ tiene si y sólo si $S$ tiene un modelo. Por lo que nos permite jugar con los objetos, en lugar de con las fórmulas y de las pruebas. Debido a que generalmente el juego con objetos es más fácil que jugar con la sintaxis. La parte importante es que $\sf ZF$ nos permite llevar todos los resultados que hemos obtenido semánticamente, y convertirlos de nuevo en algo que era realmente resultó de $\sf PA$ o algunos subteoría de la misma.
Por supuesto, cuando se utiliza $\sf ZF$ como su meta-teoría por sí mismo, usted no está hablando de modelos de clase, estamos hablando de establecer modelos. Nosotros vamos un paso más hacia abajo el agujero del conejo. Y eso está bien.
spaceisdarkgreen
Puntos
31
Sí, son metatheorems en el sentido de que son teoremas acerca de los sistemas formales. Pero aviso de que existe una difusa línea de lo que se puede llamar a un metatheorem. Si $\phi$ es una oración en el lenguaje de la teoría de conjuntos y $\phi$ es un teorema de ZFC, entonces el (verdadero) declaración de "$\mathsf{ZFC}\vdash \phi$" es un metatheorem que podemos probar en el metatheory, normalmente mediante la producción y verificación formal de ZFC prueba (bueno, lo que realmente hacemos es dar un lenguaje natural argumento matemático que, se supone, más o menos claramente mapa formales de ZFC prueba). Normalmente cuando teoremas son llamados específicamente como metatheorems, son más complicadas de las declaraciones de $"\mathsf{ZFC}\vdash \phi$," por lo que es importante tomar en cuenta de que estamos haciendo algo menos trivial en el metatheory que simplemente la verificación de una prueba.
$\mathrm{Con}(S)\to \mathrm{Con}(T)$ es uno de estos más complicado declaraciones, donde en realidad tenemos dos teorías diferentes, y estamos diciendo que si podemos probar una contradicción de $T$ entonces podemos de $S$ así.
Así que sí, es en la metatheory, pero lo que es el metatheory? Es sólo el lenguaje que estamos usando para estudiar y probar cosas acerca de los sistemas formales en cuestión. Esto lo hacemos en el lenguaje natural normalmente, pero a menudo puede ser de interés para formalizar la metatheory y responder preguntas como las que los axiomas necesarios para demostrar un determinado resultado en ZFC. Para ello necesitamos el código de las ideas de las fórmulas y de las pruebas en algún sistema formal, es decir, Gödel de la codificación. (No voy a decir nada más sobre esto ya que veo que se ha dicho en los comentarios.) Nada se opone a la utilización de ZFC para formalizar la metatheory, aunque normalmente es una exageración para el estudio de las pruebas en los sistemas formales y débiles de las teorías de la aritmética suficiente.
En particular, como Eric dice en los comentarios, que normalmente puede demostrar algo como $\mathrm{Con}(S)\to \mathrm{Con}(T)$ en un sistema mucho más débiles que en ZF, así que sin duda puede resultar en ZF. Tenga en cuenta que este es framable como una media aritmética de las declaraciones sobre ciertos prueba de los números existentes, y ZF puede hablar de la aritmética a través de sus números naturales, por lo que puede muy fácilmente expresar la declaración en ambos sistemas (y gracias a la ZF mayor expresividad que tienen otros más naturales y las opciones de codificación de allí en vez de usar sólo números).
Usted está en lo correcto que $\mathcal M\models S$ y más en general la satisfacción de la relación $\mathcal M\models \phi$ no puede ser expresado en ZFC para $M$ una clase adecuada. Supongo que usted tiene en mente lo que demuestra la premisa de un teorema como "Si para todas las $\phi\in S,$ ZFC puede demostrar $\mathcal M\models \phi$ para algunos $\mathcal M$ (que es una clase adecuada en este caso), a continuación, $\mathrm{Con}(\mathsf{ZFC}) \to \mathrm{Con}(S)$". Pero tenga en cuenta la sutileza aquí con nosotros... no se le pide que muestre $\mathcal M\models \phi,$ nos pide mostrar que ZFC es prueba de esto. En otras palabras, que mantiene en todo (set). modelos de ZFC. Y de la relativización de la clase adecuada para un modelo de conjunto es, por supuesto, un conjunto.
