Variation on Lob's Theorem Lob's theorem is, of course, if $P(y)$ is a provability predicate for $S$, $S$ diagonalisable, then if $(P(A) \rightarrow A)$ is provable in $S$ then $A$ is provable in $S$. I understand the proof of this. I am interested in the question: > Suppose $P(A) \rightarrow B$ and $P(B) \rightarrow A$ are provable in $S$. Does it then follow that $A$ and $B$ are both provable in $S$? Is this true? If so, why? I've tried proving it via variations on the proof of Lob's Theorem, and by trying to show that $P(A) \rightarrow A$ and $P(B) \rightarrow B$ are provable in $S$ given the assumptions, and thus that I can apply Lob's Theorem to get the conclusion. But I cannot seem to get anything to work.

There's no need to dive into the proof - this can be directly reduced to a single application of Lob's theorem.

From $P(A)\rightarrow B$ and $P(B)\rightarrow A$, we get $P(A)\wedge P(B)\rightarrow A\wedge B$. But trivially we have $P(A)\wedge P(B)\leftrightarrow P(A\wedge B)$, so in fact from $P(A)\rightarrow B$ and $P(B)\rightarrow A$ we can conclude $$P(A\wedge B)\rightarrow A\wedge B.$$ Now apply Lob's theorem to $A\wedge B$.

* * *

In fact, even _that's_ written more inefficiently than it needs to be - just observe that $P(A\wedge B)\rightarrow P(A)\wedge P(B)$ so under the hypotheses gives $B\wedge A$ \- but the "backwards" way I've written it above might be more helpful in terms of seeing how we whipped it up: see how large a proposition we need to have a proof of in order to trigger every hypothesis, and then see if that lets us "catch our tail."