4

If $n$ is the Godel number of $\phi$, then some formula $\chi(n)$ states "ZFC proves $\phi$". One might then think if ZFC $\vdash \chi(n)$, then ZFC $\vdash \phi$, but this seems not necessarily the case. For instance, if $\phi$ is $1 = 0$, then $\chi(n)$ is $\neg$ Con(ZFC). $\neg$ Con(ZFC) is not provable from ZFC, but it is consistent with it, so this seems to be a scenario where ZFC + $\neg$ Con(ZFC) proves "I prove $1=0$", when it does not.

$\textbf{Question}$: When does ZFC $\vdash \chi(n)$ imply ZFC $\vdash \phi$?

$\textbf{Update}\ (1/1/2024)$: I realized there is a possible contradiction with the statement "ZFC $\vdash \chi(n)$ implies ZFC $\vdash \phi$". Tarski's Theorem states if $\Phi$ is consistent and allows representations, then $\Phi^\vdash$ is not representable in $\Phi$. That is, there does not exist a "truth relation" $g(x)$ such that for any formula $\phi$ with Godel number $n$, $\Phi \vdash g(n)$ iff $\Phi \vdash \phi$.

It appears the $\chi(n)$ which states "ZFC proves $\phi$", has the property $\chi(n')$ states "ZFC proves $\phi'$" whenever $n'$ is the Godel number of $\phi'$. Thus if "ZFC $\vdash \chi(n)$ implies ZFC $\vdash \phi$" for all $n$, it appears $\chi(x)$ would contradict Tarski's theorem.

Pictures of Tarski's Theorem. From Logic by Ebbinghaus.

Stephen Harrison
  • 1,421
  • 2
    You're likely looking for Löb's theorem https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem – ac15 Dec 31 '23 at 03:46
  • Because we're starting with Prov(P), if $\text{Prov}(P) \rightarrow P$ is proved, one immediately get $P$. It seems the application would become the trivial statement "PA $\vdash \text{Prov}(P)$ implies PA $\vdash P$ when PA $\vdash \text{Prov}(P) \rightarrow P$. – Stephen Harrison Dec 31 '23 at 04:01
  • If ZFC is $\omega$-consistent (or $\Sigma_1^0$-sound), then this implication holds for all formulas. – spaceisdarkgreen Dec 31 '23 at 04:46

1 Answers1

4

Probably yes, but it's hard to prove!

Under (what are generally considered) very mild hypotheses, this statement is true for all $\phi$. Specifically, the hypothesis needed is $\Sigma_1$-soundness: this is stronger than mere consistency - consider the consistent theory $\mathsf{ZFC}+\neg Con(\mathsf{ZFC})$ - but weaker than $\omega$-consistency.

Precisely, there is a principle I will call "$Sound_{\Sigma_1}(\mathsf{ZFC})$," no messier to articulate than the better-known $Con(\mathsf{ZFC})$, with the property that $$\mathsf{ZFC}+Sound_{\Sigma_1}(\mathsf{ZFC})\vdash \forall\phi\color{red}{[\mathsf{ZFC}\vdash\phi\iff\mathsf{ZFC}\vdash(\mathsf{ZFC}\vdash\phi)]}$$ (allowing for minor abuses of notation for simplicity).

On the other hand, if left to its own devices $\mathsf{ZFC}$ can prove no interesting instances of the clause in red: for any particular sentence $\phi$, if $\mathsf{ZFC}\vdash [\mathsf{ZFC}\vdash\phi\iff\mathsf{ZFC}\vdash(\mathsf{ZFC}\vdash\phi)]$ then $\mathsf{ZFC}\vdash\phi$ outright. This is Lob's theorem, and - as usual - none of the foregoing is specific to $\mathsf{ZFC}$. In fact, the universally-quantified red clause above is equivalent over $\mathsf{ZFC}$ to $Sound_{\Sigma_1}(\mathsf{ZFC})$.

Noah Schweber
  • 245,398
  • I added an update. Are you able to take a look? – Stephen Harrison Jan 02 '24 at 04:12
  • By the completeness theorem $\Phi^\vdash = \Phi^\models$. I have a book right beside me which states there does not exist a $g(x)$ which represents $\Phi^\vdash$. How is my statement wrong? – Stephen Harrison Jan 02 '24 at 04:16
  • I'll upload pictures to the question. – Stephen Harrison Jan 02 '24 at 04:19
  • @StephenHarrison I figured it out! My bad - I was misreading your statement, specifically I read "definable" in place of "representable." Your issue is that $\chi(-')$ is not in fact a representation, for the same reason that $\chi$ itself is not a representation: there will be models of $\mathsf{ZFC}$ which think $\chi(n')$ holds even when in reality $\chi(n')$ fails. E.g. if $\mathcal{M}$ is a model of $\mathsf{ZFC}$ which thinks that $\mathsf{ZFC}$ is inconsistent, then $\mathcal{M}$ thinks that $\chi(n')$ holds for every $n$, even though that's not the case. – Noah Schweber Jan 02 '24 at 04:27
  • How is $\chi$ not a representation? If ZFC $\vdash \chi(n)$ iff ZFC $\vdash \phi$, isn't that the definition of a representation? What do you mean by a model which "thinks" $\chi(n)$ holds when it doesn't? Do you mean $\cal{M} \models \chi(n)$ for all $n$? (I do not know what it means for "$\chi(n)$ to not hold in reality"). – Stephen Harrison Jan 02 '24 at 04:41
  • 1
    @StephenHarrison We would also need $\mathsf{ZFC}\vdash\neg\chi(n)$ iff $\mathsf{ZFC}\not\vdash\phi$. Note that that's not implied by what you've written, since "$\not\vdash$" is not equivalent to "$\vdash\neg$." – Noah Schweber Jan 02 '24 at 05:10