Whenever I start nesting proof predicates, I always seems to run into these bizarre situations. I was wondering if anyone knows about this and could shed some light on it or provide me with some references. Thank you!


Let's define a set S as follows.

$$ S := \begin{cases} \mathtt{ZF} & \text{ if $\mathtt{Con}(\mathtt{ZF})$} \\ \emptyset & \text{ otherwise} \end{cases} $$

Although we can't determine whether S is $\mathtt{ZF}$ or S is $\emptyset$, we can still define $S$.

Consider the predicate $\phi_S(x)$ which abbreviates: $\mathtt{Con}(\mathtt{ZF}) \rightarrow x=\mathtt{ZF} \wedge \neg \; \mathtt{Con}(\mathtt{ZF}) \rightarrow x=\emptyset$.

The predicate $\phi_S(x)$ acts as a definition for S and we have $\mathtt{ZF} \vdash \exists! x \; \phi_S(x).$

----Proof Predicates----

For any set X of Godel numbers for first order formulas, in a standard manner, one can formally define a proof predicate $\mathtt{Pf}_{X}$. (I can elaborate if necessary.)

We will consider both $\mathtt{Pf}_{\mathtt{ZF}}$ and $\mathtt{Pf}_{S}$.

It seems reasonable that we can nest $\mathtt{Pf}_{\mathtt{ZF}}$, but how do we nest $\mathtt{Pf}_{S}$?

To do so, $\mathtt{Pf}_{S}(\mathtt{Pf}_{S}(\ulcorner \psi \urcorner))$ will abbreviate $\exists x \; \phi_S(x) \wedge \mathtt{Pf}_{x}(\ulcorner \exists x \; \phi_S(x) \wedge \mathtt{Pf}_{x}(\ulcorner \psi \urcorner)\urcorner)$.

In other words, we include $S$'s definition each time we nest to a lower level.

Note: $\mathtt{Con}(X)$ will just abbreviate $\exists \ulcorner \psi \urcorner \; \neg \; \mathtt{Pf}_X(\ulcorner \psi \urcorner)$.


1) First, I notice that $\mathtt{ZF} \vdash \mathtt{Con}(\mathtt{ZF}) \rightarrow S=\mathtt{ZF} \wedge \mathtt{Con}(S)$.

2) And, $\mathtt{ZF} \vdash \neg \; \mathtt{Con}(\mathtt{ZF}) \rightarrow S=\emptyset \wedge \mathtt{Con}(S)$.

3) From these two, we get: $\mathtt{ZF} \vdash \mathtt{Con}(S)$.

4) Further, we get: $\mathtt{ZF} \vdash \mathtt{Pf}_{\mathtt{ZF}}(\ulcorner \mathtt{Con}(S) \urcorner)$.

(I can elaborate on the standard properties of these proof predicates if necessary.)

Consider $\mathtt{Pf}_{S}(\ulcorner \mathtt{Con}(S) \urcorner)$. This could not happen if $S = \emptyset$. Also, it does happen if $S = \mathtt{ZF}$ as we just showed.

5) Therefore, $\mathtt{ZF} \vdash \mathtt{Con}(\mathtt{ZF}) \leftrightarrow \mathtt{Pf}_{S}(\ulcorner \mathtt{Con}(S) \urcorner)$.

For any $\ulcorner \psi \urcorner$, consider $\mathtt{Pf}_{S}(\mathtt{Pf}_{S}(\ulcorner \psi \urcorner))$. This implies that $S = \mathtt{ZF}$ and $\mathtt{Con}(\mathtt{ZF})$ because otherwise we have the empty set which can't prove anything.

6) $\mathtt{ZF} \vdash \mathtt{Pf}_{S}(\mathtt{Pf}_{S}(\ulcorner \psi \urcorner)) \rightarrow \mathtt{Con}(\mathtt{ZF})$.

So we have $\mathtt{Pf}_{\mathtt{ZF}}(\mathtt{Pf}_{S}(\ulcorner \psi \urcorner))$. For the same reasons, at the lower level we have $S = \mathtt{ZF}$ and $\mathtt{Con}(\mathtt{ZF})$ i.e. $\mathtt{Pf}_{\mathtt{ZF}}(\ulcorner S = \mathtt{ZF} \urcorner)$ and $\mathtt{Pf}_{\mathtt{ZF}}(\ulcorner \mathtt{Con}(\mathtt{ZF}) \urcorner)$.

However, $\mathtt{Pf}_{\mathtt{ZF}}(\ulcorner \mathtt{Con}(\mathtt{ZF}) \urcorner)$ is equivalent to $\neg \; \mathtt{Con}(\mathtt{ZF})$.

7) Therefore, $\mathtt{ZF} \vdash \mathtt{Pf}_{S}(\mathtt{Pf}_{S}(\ulcorner \psi \urcorner)) \rightarrow \neg \; \mathtt{Con}(\mathtt{ZF})$.

Combining both 6) and 7), we get:

8) $\mathtt{ZF} \vdash \neg \; \mathtt{Pf}_{S}(\mathtt{Pf}_{S}(\ulcorner \psi \urcorner))$.

If we picked $\ulcorner \psi \urcorner$ to be $\ulcorner \mathtt{Con}(S) \urcorner$, then we would have:

9) $\mathtt{ZF} \vdash \neg \; \mathtt{Pf}_{S}(\mathtt{Pf}_{S}(\ulcorner \mathtt{Con}(S) \urcorner))$.


In the end, this is a bizarre situation because we have both of the following:

$\mathtt{ZF} \vdash \mathtt{Con}(\mathtt{ZF}) \leftrightarrow \mathtt{Pf}_{S}(\ulcorner \mathtt{Con}(S) \urcorner)$, and $\mathtt{ZF} \vdash \neg \; \mathtt{Pf}_{S}(\mathtt{Pf}_{S}(\ulcorner \mathtt{Con}(S) \urcorner))$.

How can the proof predicates $\mathtt{Pf}_{S}$ and $\mathtt{Pf}_{S}\mathtt{Pf}_{S}$ say the opposite of each other?

  • 1
    $\begingroup$ Are you sure that the formula Con(ZF)→x=ZF∧¬Con(ZF)→x=∅ is "meaningful", i.e. well-formed ? From x=∅, it seems that the variable $x$ range over set; if so, what is ZF ? $\endgroup$ Commented Sep 3, 2014 at 19:09
  • 1
    $\begingroup$ ┌ψ┐ is a number, nit a variable. Thus, how you can quantify it into ; ∃┌ψ┐ ? $\endgroup$ Commented Sep 3, 2014 at 19:10
  • 1
    $\begingroup$ I haven't thought this through carefully, but I'm suspicious about how much of the standard machinery you can salvage for your $\texttt{Pf}_S$. Unlike in Gödel's proof, your $S$ is not recursive (the $\texttt{Con}$ used in its definition is $\Pi_1$), and you won't be able to refer to $\Sigma_1$ completeness, which seems a key ingredient. $\endgroup$
    – user138530
    Commented Sep 6, 2014 at 1:32
  • 1
    $\begingroup$ @MichaelWehar: I'm not totally sure how relevant this is, but I had in the back of my mind the (standard?) proof of Gödel's 2nd incompleteness theorem through the Bernays-Lob derivability conditions (in a Peano arithmetic setting perhaps). The 3rd condition is usually obtained from the fact that PA (and hence ZFC as well) proves all true $\Sigma_1$ sentences, and perhaps this is where things go wrong in your setting. $\endgroup$
    – user138530
    Commented Sep 6, 2014 at 4:00
  • 1
    $\begingroup$ @MichaelWehar: My "3rd" condition is in fact the 2nd condition at the link you gave. $\endgroup$
    – user138530
    Commented Sep 7, 2014 at 3:36

1 Answer 1


I think it might be helpful to get clear on exactly what $Pr_S(\ulcorner\phi\urcorner)$ says. In ZF it is provably equivalent to saying the following informal thing:

Either ZF is consistent and $\ulcorner\phi\urcorner$ is provable in ZF, or ZF isn't consistent and $\ulcorner\phi\urcorner$ is provable from nothing.

And since the second disjunct is provably false in ZF it just says: ZF is consistent and $\ulcorner\phi\urcorner$ is provable in ZF. In other words, $Pr_S(\ulcorner\phi\urcorner)$ is provably equivalent in ZF to $Con(ZF)\wedge Pr_{ZF}(\ulcorner\phi\urcorner)$.

(I assume $Pr_{\emptyset}$ means "provable from nothing", and not "provable from nothing apart from the axioms of first order logic"? At one point you said "the empty set can't prove anything". A similar diagnosis goes through on the other interpretation though.)

So I think the issue is, once you've spelt out the definition explicitly the result doesn't bear any straightforward resemblance to a provability predicate. It's also pretty clear why we get that $Pr_S(\ulcorner\phi\urcorner)$ and $Pr_S(Pr_S(\ulcorner\phi\urcorner))$ say different things, according to ZF.

$Pr_S(\ulcorner\phi\urcorner)$ says:

ZF is consistent and ZF proves $\ulcorner\phi\urcorner$

Which is true of many $\ulcorner\phi\urcorner$, assuming ZF is consistent. $Pr_S(Pr_S(\ulcorner\phi\urcorner))$ just says the following:

ZF is consistent and ZF proves that "ZF is consistent and ZF proves $\ulcorner\phi\urcorner$"

Which is, of course, is true of no $\ulcorner\phi\urcorner$, assuming ZF is consistent.

(Note that technically $Pr_S(Pr_S(\ulcorner\phi\urcorner))$ says: ZF is consistent and ZF proves $Pr_S(\ulcorner\phi\urcorner)$. However I noted above that $Pr_S(\ulcorner\phi\urcorner)$ is provably equivalent in ZF to $Con(ZF)\wedge Pr_{ZF}(\ulcorner\phi\urcorner)$.)

  • $\begingroup$ I think this is a pretty good response! Formally, for any set $X$ of Godel numbers, I would define $Th(X)$ recursively where $Th(X)$ is the minimum set of Godel numbers for formulas that includes $X$ and is closed under the inference rules applied to the Godel numbers. Then, $\mathtt{Pf}_X(\ulcorner \psi \urcorner)$ will just mean $\ulcorner \psi \urcorner \in Th(X)$. Now, what you are saying is that from this definition, you can prove that $\mathtt{Pf}_S(\ulcorner \psi \urcorner)$ is equivalent to $\mathtt{Con}(\mathtt{ZF}) \wedge \mathtt{Pf}_{\mathtt{ZF}}(\ulcorner \psi \urcorner)$. $\endgroup$ Commented Sep 6, 2014 at 20:47
  • $\begingroup$ I think your response is a great explanation for what is going on here, but I still feel uneasy and am confused on how we can define sets like S and on how statements like $\mathtt{Pf}_S(\mathtt{Pf}_S(\ulcorner \psi \urcorner))$ don't mean what we might think they mean. Would you be willing to talk further about this? I have another example that I'm trying to understand and I think your input would be quite helpful. Thank you! :) $\endgroup$ Commented Sep 6, 2014 at 21:02
  • 1
    $\begingroup$ Certainly. You may already know this, but there is some work on non-standard provability predicates that seems related. For example there is a formula in the language of arithmetic which is true of the Godel number of a sentence in the standard model if and only if the sentence is provable in PA, but such that the claim corresponding to Con(PA) using that formula is provable in PA. (See for example matwbn.icm.edu.pl/ksiazki/fm/fm49/fm4915.pdf) $\endgroup$ Commented Sep 6, 2014 at 21:40
  • $\begingroup$ Great! Thank you for the reference. I will contact you. :) $\endgroup$ Commented Sep 6, 2014 at 22:59

You must log in to answer this question.

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