4 votos

$\Sigma^0_1$-solidez de $T\supset PA$

Al $T\supset PA$ $\Sigma^0_1$- sonido, es cierto que $T\vdash Pr(\underline\phi)$ implica $T\vdash \phi $ para cualquier frase,$\phi $? Donde $Pr$ es el provability predicado. Si no, es verdad para $\phi$ se $\Pi^0_1$?

Cualquier ayuda es muy apreciada Gracias!

1voto

user27515 Puntos 214

$\newcommand{\nmrl}[1]{\overline{ #1 }}\newcommand{\godel}[1]{\ulcorner #1 \urcorner}\newcommand{\PR}{\mathrm{Pr}_T}\newcommand{\PROOF}{\mathrm{proof}_T}$ Este parece ser justo siguientes definiciones. Voy a utilizar las siguientes notaciones para ser algo preciso:

  • Dada una fórmula $\phi$ , $\godel{\phi}$ voy a indicar el Gödel-número de $\phi$ con respecto a algunos fijos arithmetization de la sintaxis.
  • Dado un número natural $n$, $\nmrl{n}$ me refiero a que el plazo $\overbrace{S \cdots S}^{n\text{ times}}0$.

Utilizando las técnicas estándar $\PR ( x )$ es sólo $( \exists y ) ( \PROOF ( y , x ) )$ donde $\PROOF ( y , x )$ "$y$ es la codificación de la prueba de (la fórmula codificado por) $x$ $T$ " Si $T$ es una teoría recursiva, entonces el estándar de técnicas que $\PROOF$$\Delta_0$, lo que significa que $\PR$$\Sigma_1$. Por lo tanto, si $T \vdash \PR ( \nmrl{\godel{\phi}} )$ $\Sigma_1$- solidez de ello se sigue que $\PR ( \nmrl{\godel{\phi}} )$ es verdadera en el modelo estándar, y por lo que hay un $n \in \mathbb{N}$ tal que $\mathbb{N} \models \PROOF ( n , \godel{\phi} )$. Pero, a continuación, $n$ realmente códigos de una prueba de $\phi$$T$, por lo que podemos decodificar $n$ para obtener una secuencia $\phi_1 , \ldots , \phi_n$ de las fórmulas que sirve como una prueba de $\phi$ a partir de $T$: $T \vdash \phi$.

Nota, en particular, que $\PR ( \nmrl{\godel{\phi}} )$$\Sigma_1$, independientemente de lo que la fórmula $\phi$ es (ya que acaba de traducir en un plazo).

i-Ciencias.com

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.

Powered by:

X