Problems with nesting proof predicates in first order logic. 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?
 A: 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)$.)
