Is the converse of the first Hilbert-Bernays Derivability Condition true?

Question

The first Hilbert-Bernays Derivability Condition is (⊢P) → (⊢◻P). What I'd like to know is, is the converse true? That is, is (⊢◻P) → (⊢P) valid? I know from Löb's Theorem that ⊢(◻P → P) is not valid in general (and when it is, it suffices to prove P), but I'd like to know whether it's also true that (⊢◻P) → (⊢P) isn't valid in general.

Answer 1

There are some unclear aspects to the question, so I'll make the following plausible assumptions: (1) You use both "true" and "valid" to mean the same thing, namely "true in the standard model of arithmetic". (2) $\square$ refers to a formalization of provability in the same theory, say $T$, that $\vdash$ refers to. (3) $T$ is a recursively enumerable theory, and its formalization is done straightforwardly (not with any Feferman-style tricks).

Under these assumptions, if $T$ is true (or even just $\Sigma^0_1$-correct), for example, if $T$ is Peano atrithmetic (PA), then $\vdash\square P$ does imply $\vdash P$, simply because "$P$ is provable" is a $\Sigma^0_1$ statement, so if $T$ proves it then it must be true.

On the other hand, if we merely assume that $T$ is consistent, then we might well have $\vdash\square P$ but not $\vdash P$. For example, let $T$ be PA plus the sentence formalizing "PA is inconsistent". This $T$ is consistent, by the second incompleteness theorem. But it proves that $\square(0=1)$ (i.e., it proves its own inconsistency) without also proving $0=1$ (i.e., without actually being inconsistent).