19
$\begingroup$

Being a new member, I am not yet sure whether my question will be taken as a research level question (and thus, appropriate for MO). However, I have seen similar questions on MO, couple of which led me asking mine, and I seem to not be able to find many resources except discussion on FOM and MO. So, any references to resolve the question and fix my possible confusion would be appreciated.

As the title suggests, I want to understand the relation between $ZFC \vdash \varphi$ and $ZFC \vdash\ 'ZFC \vdash \varphi'$. Let me give my motivation (and some partial answers) asking this question so that what I'm trying to arrive at is understood.

We know that if $ZFC \vdash \varphi$, then $ZFC \vdash\ 'ZFC \vdash \varphi'$ for we could write down the Gödel number of the proof we have for $\varphi$ and then check that the formalized $\vdash$ relation holds. I believe even more can be checked to be true for this provability predicate (Hilbert-Bernays provability conditions).

Is the converse true in general? Not necessarily. (Just to make sure that it will be pointed out sooner if I am doing any mistakes, I will try to write down everything unnecessarily detailed using less English and more symbols!)

Let us assume only that $ZFC$ is consistent (However, I am not assuming the formal statement $Con(ZFC)$, that is $\ 'ZFC \nvdash \lceil 0=1 \rceil'$). Then, it is conceivable that $ZFC \vdash\ \ 'ZFC \vdash \lceil 0=1 \rceil'$ but $ZFC \nvdash 0=1$. It might be that in reality ZFC is consistent but $\omega$-inconsistent.

Indeed, if I am not missing a point, it is consistent to have this situation:

$ZFC \vdash Con(ZFC) \rightarrow Con(ZFC+\neg Con(ZFC))$ (Gödel) $ZFC \vdash Con(ZFC) \rightarrow\ \exists M\ M \models ZFC+\neg Con(ZFC)$ (Gödel) $ZFC \vdash Con(ZFC) \rightarrow\ \exists M\ M \models\ ZFC+\ 'ZFC \vdash \lceil 0=1 \rceil'$ $ZFC \vdash Con(ZFC) \rightarrow\ \exists M\ M \models\ ZFC+\ 'ZFC \vdash\ 'ZFC \vdash \lceil 0=1 \rceil\ '\ '$ (Soundness and the second provability condition here) $ZFC \vdash Con(ZFC) \rightarrow Con(ZFC+\ 'ZFC \vdash \neg Con(ZFC)\ ')$

So we cannot hope to have $ZFC \vdash\ 'ZFC \vdash \varphi'$ implying $ZFC \vdash \varphi$ for an arbitrary formula without requiring an additional assumption. At least, we know this for $\varphi: 0=1$ (this is not because of the consistency argument above, but because consistency and $\omega$-inconsistency of ZFC is a possibility).

If you believe that ZFC's characterization of natural numbers coincides with what we have in mind and agree that ZFC should not be $\omega$-inconsistent, then you might want to throw in the assumption $Con(ZFC)$.

Now imagine a universe where $Con(ZFC)$ holds but all the models of ZFC is $\omega$-nonstandard and believe $\neg Con(ZFC)$. I do not know whether this scenario is even possible (which is another question I am wondering) but if it is possible, then it would be the case that $'ZFC \vdash \neg Con(ZFC)\ '$, by completeness since $\neg Con(ZFC)$ is true in all models. Then if the implication in title (or should I say, an informal version of it: $V \models ZFC \vdash \varphi$ implies $V \models \varphi$) held, then $\neg Con(ZFC)$ which contradicts our assumption that there are models at all. The point is arbitrary models of ZFC may not be sufficient to have existence of ZFC-proofs implying existence of actual proofs.

However, if we add a stronger assumption $\psi$ that there is an $\omega$-model, then whenever we have an arithmetic sentence $\varphi$, if

$ZFC \vdash\ 'ZFC \vdash \lceil \varphi \rceil'$

then

$ZFC+\psi \vdash \exists M\ \omega^M=\omega \wedge M \models ZFC+\ \varphi$

and because $\omega$ in the model is the real one, by taking care of quantifiers one by one we can deduce $ZFC+\psi \vdash \varphi$. Thus, existence of an $\omega$-model solves our problem for arithmetical sentences. I cannot see any reason to make this work for arbitrary sentences without strengthening the assumption. Here is a thought:

We know, by the reflection principle, that we can find some limit ordinal $\alpha$ such that $\varphi \leftrightarrow \varphi^{V_{\alpha}} \leftrightarrow V_{\alpha} \models \varphi$. Thus, if we could make sure somehow that $V_{\alpha}$ is a model of ZFC while we reflect $\varphi$, then we would be done. But I could not modify the proofs of reflection in such a way that this can be done and am not even sure that this could be done.

My question to MO is to what extent (and under which assumptions) can we get the implication in the title?

Edit: After reading Emil Jerabek's answer, I realized I should clarify some details.

Firstly, I want to treat ZFC only as a formal system (meaning that if you are claiming some assumption $\psi$ does what I want, I want to have a description of how that proof would formally look. This is why I kept writing all the leftmost $ZFC \vdash$'s all the time). Then, it is clear by the above discussions that even if we could prove $ZFC \vdash \varphi$ within our system, we may not prove $\varphi$ without additional assumptions on our system.

One solution could be that our system satisfies the "magical" property that whenever we have $ZFC \vdash \exists x \in \omega\ \varphi(x)$, say for some arithmetic sentence, then we have $ZFC \vdash \varphi(SSS...0)$ for some numeral. This of course is not available by default setting for we know that the theory $ZFC$+ $c \in \omega$ + $c \neq 0$ + $c \neq S0$ +... is consistent if $ZFC$ is consistent. Thus, that magical property seems like an unreasonably strong assumption.

To make my question very precise, what I want is some assumption $\psi$ so that for some class of formulas, whenever I have $ZFC \vdash ZFC \vdash \varphi$, then $ZFC + \psi \vdash \varphi$. For arithmetic sentences, existence of an $\omega$-model is sufficient.

I agree that $\Sigma^0_1$ soundness should be sufficient for arithmetic sentences if what you mean by $\Sigma^0_1$ soundness is having $ZFC \vdash ZFC \vdash \varphi$ requiring (maybe even as a derivation rule, attached to our system!) $ZFC \vdash \omega \models \phi$, where $\phi$ is the translated version of $\varphi$ into the appropriate language, since I can again go through quantifier by quantifier and prove the sentence itself, that is $ZFC \vdash \varphi$.

However, I see no reason why $\Sigma^0_1$ soundness should be enough for arbitrary sentence $\varphi$. It seems to me that what we need is some structure for which we have the reflection property that formal truth in the structure is provably equivalent to $\varphi$ and that structure being model of all the ZFC-sentences used in the ZFC-proof of $\varphi$.

I believe existence of $\Sigma_n$-reflecting cardinals which are inaccesible is more than sufficient for sentences up to $n$ in the Levy hiearchy. By definition of those, we have the equivalence $\varphi \leftrightarrow V_{\kappa} \models \varphi$ and then provability of $\varphi$ in ZFC implies $V_{\kappa} \models \varphi$. However, I am not sure if we had to go that far. ${}{}$

Improve this question
$\endgroup$
5
  • $\begingroup$ By Löb's theorem, if $ZFC \vdash Bew(\ulcorner\varphi\urcorner) \rightarrow \varphi$ then $ZFC \vdash \varphi$. $\endgroup$
    – Benedict Eastaugh
    Commented Apr 12, 2013 at 8:36
  • 1
    $\begingroup$ I don't see how that should help in this case since what I am looking for is if $ZFC \vdash Bew(\varphi)$, then $ZFC \vdash \varphi$. $\endgroup$
    – Burak
    Commented Apr 12, 2013 at 8:49
  • 1
    $\begingroup$ Dear Burak, you can edit your question as much as you want but at some point it's simply better to ask another one, especially if you want more answers. $\endgroup$
    – François G. Dorais
    Commented Apr 12, 2013 at 23:24
  • $\begingroup$ Dear François, the reason for so many edits is that after posting the original question, I realized some of my statements were faulty and while trying to fix those I began partially answering my own question and thus, editing continuously. And here comes the latest edit... $\endgroup$
    – Burak
    Commented Apr 13, 2013 at 2:10
  • 2
    $\begingroup$ Don't worry, we get asked a lot of beginner questions about logic. I explain this to myself in terms of a typical mathematician having little or no training in logic, so it's all research level to him. But that is ok, this forum is here to enlighten people. $\endgroup$
    – Andrej Bauer
    Commented Sep 24, 2013 at 13:59

2 Answers 2

Reset to default
23
$\begingroup$

$\def\zfc{\mathrm{ZFC}}\def\pr{\operatorname{Prov}\nolimits}$The statement

$\zfc\vdash\pr_\zfc(\ulcorner\varphi\urcorner)$ implies $\zfc\vdash\varphi$ for every sentence $\varphi$ in the language of $\zfc$

is equivalent to the statement that $\zfc$ is either inconsistent or $\Sigma^0_1$-sound: the latter means that every $\Sigma^0_1$-sentence provable in $\zfc$ is true in standard integers. One direction is obvious as $\pr_\zfc(\ulcorner\varphi\urcorner)$ is a $\Sigma^0_1$-sentence, and its truth in $\mathbb N$ says exactly that $\varphi$ is provable in $\zfc$. The converse follows from the Friedman–Goldfarb–Harrington principle: if $T$ is a recursively axiomatized theory containing Robinson’s arithmetic and $\sigma$ a $\Sigma^0_1$-sentence, there exists a sentence $\varphi$ (that can also be taken $\Sigma^0_1$) such that

$$I\Delta_0+\mathit{EXP}\vdash\pr_T(\ulcorner\varphi\urcorner)\leftrightarrow(\sigma\lor\pr_T(\ulcorner0=1\urcorner)).$$

$\Sigma^0_1$-soundness is stronger than consistency, but weaker than $\omega$-consistency. If you are wondering about foundational issues, it is best to consider it as a separate assumption on its own.

Improve this answer
$\endgroup$
7
  • $\begingroup$ Thank you very much for your answers. Just to make sure, you don't actually mean "for every formula", do you? I understood that part as "for every arithmetical formula". If so, what about other formulas not expressing arithmetical statements? In any case, I'm guessing my naive approach, that there are $\omega$-models of ZFC, was a complete overkill. $\endgroup$
    – Burak
    Commented Apr 12, 2013 at 10:41
  • 6
    $\begingroup$ No, I meant for every formula. The provability predicate is $\Sigma^0_1$ irrespective of what kind of formulas (or rather, Gödel numbers) are plugged inside. It turns out this does not actually make a difference (the formulas arising from the FGH principle are in fact arithmetical $\Sigma^0_1$, so if the statement holds for these, it holds for all formulas). $\endgroup$
    – Emil Jeřábek
    Commented Apr 12, 2013 at 11:43
  • $\begingroup$ I made it a bit more explicit in the answer. $\endgroup$
    – Emil Jeřábek
    Commented Apr 12, 2013 at 13:45
  • $\begingroup$ There is a more-or-less standard way to formalize $\Sigma_1^0$ soundness for ZFC: Given a formula $\tau$ enumerating the axioms of ZFC, construct the proof-predicate $Pr_\tau(x)$. Now construct the theory T. T has all axioms of ZFC and a schema of all sentences of the form $Pr_\tau(\varphi)\rightarrow \varphi$ where $\varphi$ is any formula in the language of ZFC. Sometimes T includes as an axiom "< is a well-ordering of $\omega$."Working in T, any proof of $Pr_\tau(\phi)$ can be transformed into a proof of $\phi$ in a simple way: copy the T-proof of $Pr_\tau(\phi)$, concatenate the $\endgroup$
    – Everett Piper
    Commented Apr 14, 2013 at 18:35
  • $\begingroup$ particular instance of the reflection principle $Pr_\tau(\phi)\rightarrow\phi$ and then concatenate $\phi$. The penultimate line of this proof is justified since we merely appended an axiom of T to the original T-proof of $Pr_\tau(\phi)$ and the last line follows from a single application of modus ponens. So it's actually straight-forward to produce a number witnessing a T-proof of $\phi$ given a number witnessing T-proof of $Pr_\tau(\phi)$. $\endgroup$
    – Everett Piper
    Commented Apr 14, 2013 at 18:38
16
$\begingroup$

With regard to your sub-question,

Now imagine a universe where $\text{Con}(\text{ZFC})$ holds but all the models of $\text{ZFC}$ are $\omega$-nonstandard and believe $\neg \text{Con}(\text{ZFC})$. I do not know whether this scenario is even possible...

Indeed this is possible, assuming that $\text{ZFC}+\text{Con}(\text{ZFC})$ is consistent. The reason is that by the incompleteness theorem, if this theory is consistent, then there is a model of $\text{ZFC}+\text{Con}(\text{ZFC})+\neg\text{Con}(\text{ZFC}+\text{Con}(\text{ZFC}))$. In this model, we have that $\text{Con}(\text{ZFC})$ holds, but there is no model of $\text{ZFC}+\text{Con}(\text{ZFC})$, and so all models of $\text{ZFC}$ in this model satisfy $\neg\text{Con}(\text{ZFC})$. In particular, all models of $\text{ZFC}$ in this model are also $\omega$-nonstandard from the perspective of this model.

Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ In the last line, "$\omega$-standard" was meant to be "$\omega$-nonstandard", I fixed that. $\endgroup$
    – Ali Enayat
    Commented Apr 12, 2013 at 16:19

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .