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."

• D'oh. Of course! – Henning Makholm Apr 2 at 20:42
• So beautifully simple! Thanks – Atlas Apr 3 at 8:07

If the Hilbert-Bernays conditions hold and $$P\to Q$$ is provable, then $$\Box P\to\Box Q$$ is also provable.

Apply this to the proof of $$\Box A \to B$$ to get $$\Box\Box A \to \Box B$$, and combine this with $$\Box B \to A$$, to get $$\Box \Box A \to A$$.

Now repeat the usual proof of Löb's theorem with $$\Box\Box$$ instead of $$\Box$$ everywhere.