4

When $T\supset PA$ is $\Sigma^0_1$-sound, is it true that $T\vdash Pr(\underline\phi)$ implies $T\vdash \phi $ for any sentence $\phi $? Where $Pr$ is the provability predicate. If not, is it true for $\phi$ which are $\Pi^0_1$?

Any help is appreciated Thanks!

user52534
  • 751

1 Answers1

1

$\newcommand{\nmrl}[1]{\overline{ #1 }}\newcommand{\godel}[1]{\ulcorner #1 \urcorner}\newcommand{\PR}{\mathrm{Pr}_T}\newcommand{\PROOF}{\mathrm{proof}_T}$ This seems to be just following definitions. I'll use the following notations to be somewhat precise:

  • Given a formula $\phi$, by $\godel{\phi}$ I'll denote the Gödel-number of $\phi$ with respect to some fixed arithmetization of the syntax.
  • Given a natural number $n$, by $\nmrl{n}$ I mean the term $\overbrace{S \cdots S}^{n\text{ times}}0$.

Using the standard techniques $\PR ( x )$ is just $( \exists y ) ( \PROOF ( y , x ) )$, where $\PROOF ( y , x )$ means "$y$ is the encoding of a proof of (the formula coded by) $x$ from $T$" If $T$ is a recursive theory, then the standard techniques give that $\PROOF$ is $\Delta_0$, which means that $\PR$ is $\Sigma_1$. Therefore if $T \vdash \PR ( \nmrl{\godel{\phi}} )$ by $\Sigma_1$-soundness it follows that $\PR ( \nmrl{\godel{\phi}} )$ is true in the standard model, and so there is an $n \in \mathbb{N}$ such that $\mathbb{N} \models \PROOF ( n , \godel{\phi} )$. But then $n$ really codes a proof of $\phi$ from $T$, so we can decode $n$ to get a sequence $\phi_1 , \ldots , \phi_n$ of formulae which serves as a proof of $\phi$ from $T$: $T \vdash \phi$.

Note, in particular, that $\PR ( \nmrl{\godel{\phi}} )$ is $\Sigma_1$ regardless of what the formula $\phi$ is (since we just translate it into a term).

user642796
  • 52,188