Problems with nesting proof predicates in first order logic.

Question

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!

----Definition----

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)$.

----Proofs----

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))$.

----Conclusion----

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?

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)$.)