La fórmula que expresan la consistencia de una teoría

Question

He leído en algún conjunto el libro de la teoría de que la consistencia de una teoría, decir $T$ puede ser expresado como: $$\exists \mathcal{M} (\mathcal{M} {\rm \; is \; a \; model\; and \;} \mathcal{M} \models T)$$ donde todo (modelo, teoría, etc...) ha sido formalizado. ¿Cuál es el estado de dicha declaración (es decir,$\Sigma^1_2$?)

Gracias

Answer 1

Depende de la complejidad de $T$:

• Si $T$ es recursivamente enumerable e interpreta la aritmética, a continuación, el sintáctico declaración de consistencia es $\Pi^0_1$ ("no $n$ códigos de una prueba de $0=1$"). Que $T$ interpreta la aritmética no es esencial, proporcionar un canónica significado frase "$T$ es consistente". En general, usted sólo tiene que fijar una frase $\phi$ en el idioma de $T$, y la consistencia de $T$ se puede expresar diciendo que "no $n$ códigos de una prueba de $\phi\land\lnot\phi$". (Por supuesto, diferentes $\phi$ dar fórmulas diferentes, como resultado, es por eso que mencionar la falta de "canonicity".)
• Si queremos ir más allá y eliminar el supuesto de recursivas enumerability de $T$, mientras $T$ es contable, podemos pensar en ella como un real (codificación de una teoría), y expresar el anterior como $\Pi^0_1$ declaración, que ahora utiliza el parámetro $T$, lo que nos suele escribir como $\Pi^0_1(T)$.
• Si en lugar de la sintaxis de la versión que se desea que el modelo teórico (semántica), para una media aritmética de la teoría de $T$, a la afirmación de que existe un modelo de $M$ que satisface $T$$\Sigma^1_1$: podemos suponer que $M$ es contable, gracias a la tendencia a la Löwenheim-Skolem teorema. Podemos decir, entonces, que un contable $M$ satisface $T$ al afirmar que no es una codificación real de un modelo de $M$, y la formalización de la satisfacción, que se puede hacer en un $\Sigma^1_1$ manera.
• Más allá de esto, para los contables de teorías se haría necesario el uso de $T$ como parámetro, y la semántica de la versión de la declaración se $\Sigma^1_1(T)$.

En cualquier caso, estas declaraciones son definitivamente absoluta entre transitiva modelos suficiente de la teoría de conjuntos (habiendo $T$ como un elemento).

Detalles de la formalización puede ser encontrado en Devlin, el libro de constructibility (y probablemente también en el tesoro de Drake libro sobre los grandes cardenales). En particular, Devlin del libro presenta el argumento en una buena cantidad de detalles, ya que esto es relevante para el cómputo de la complejidad de $0^\sharp$.