Is it possible to obtain a contradiction from provability logic GL + inference rule ($\square P$ ==> $P$)

Question

Is it possible to obtain a contradiction from provability logic GL + inference rule ($\square P$ ==> $P$) ?

I suspect that answer is "No".

If I am right, then there is a model of such logic.

And the model is just the classical propositional logic. (i.e. all tautologies)

Because then the part of inductive definition of true(under some evaluation) modal formulas is $Truth(\square f) := Truth(f)$.

Is everything correct in the proof? (Maybe some inaccuracies?)

Does that mean, that if we have some deductive system(let it be first-order set theory), and a model of that system inside it, than we can safely add inference the rule $\square P$ ==> $P$ to the system? (Or not necessary then, maybe, there is a finer logical connection?)

p.s. broad question: What kind of applictions adding of such extension can have? One of ideas is to prove and use, for example, the deduction theorem.

Answer 1

Using that rule, we presumably have a theorem like:

$$ \dfrac{ \dfrac{\dfrac{\dfrac{}{\square P ⊢ \square P}}{\square P ⊢ P}}{⊢ \square P → P} }{ ⊢ \square (\square P → P) } $$

Then:

$$ \dfrac{\dfrac{}{⊢ \square (\square P → P)} \qquad \dfrac{}{⊢ \square(\square P → P) → \square P}}{\dfrac{⊢ \square P}{⊢ P}} $$

Answer 2

There's an interesting subtlety here, around the deduction theorem.

Certainly accepting each sequent of the form $$\vdash \Box P\rightarrow P$$ is fatal for $\mathsf{GL}$ due to its combination with necessitation and Lob's rule. However, the sequents $$\Box P\vdash P$$ are a bit less dangerous: we only wind up with a contradiction if we also throw in the deduction rule (usually a theorem) as an inference rule to our new system. Usually the deduction theorem is rather fundamental, but this is a situation where there's a real tension between it and (a version of) the new rule under consideration.

Answer 3

I think the following is true:

$\mathrm{GL}\vdash A$ $\;\Leftrightarrow\;$ $\mathrm{GL}\vdash \square A\quad$ for any modal formula $A$.

The proof is by Solovay's theorem: $\mathrm{GL}\vdash A$ iff for every realisation $*$ of the propositional variables of $A$, $\mathrm{PA}\vdash A^*$.

(In fact Solovay's theorem holds also for any elementary-recursive, $\Sigma_1$-sound theory $T$ that contains elementary arithmetic; we only need to use $\Sigma_1$-soundness here.)

Note that by $\Sigma_1$-soundness, if $\mathrm{PA}\vdash \mathrm{Prov}_{\mathrm{PA}}(\ulcorner\phi\urcorner)$ where $\mathrm{Prov}_{\mathrm{PA}}$ is the PA-provability predicate, then $\mathrm{Prov}_{\mathrm{PA}}(\ulcorner\phi\urcorner)$ is true in the standard model $\mathbb{N}$, and so there exists some $y$ such that $\mathbb{N}\models \mathrm{Proof}_{\mathrm{PA}}(y,\ulcorner\phi\urcorner)$, i.e. $y$ codes a real proof of $\phi$ from PA, hence $\mathrm{PA}\vdash \phi$ by looking at the proof $y$.

Now if $\mathrm{GL}\vdash \square A$, then for all realisations $*$, $\mathrm{PA}\vdash (\square A)^*$. This implies that for all realisations $*$, $\mathrm{PA}\vdash A^*$. Thus $\mathrm{GL}\vdash A$ by Solovay.

I don't think one can apply deduction theorem arbitrarily in modal logic.