1
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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

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

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.