I'm starting to learn modal logic and there is something that's bothering my mind for a while.
we know from deduction theorem that $((\vdash q) \rightarrow (\vdash p)) \Leftrightarrow(\vdash (q \rightarrow p))$
and also from soundness we know that $\vdash\Box q \rightarrow \vdash q$
so here's my problem, why can't we deduce that $\vdash \Box q\rightarrow q$ if we do that with lob's theorem ($\vdash(\Box q \rightarrow q) \leftrightarrow \vdash q$) we can contravene second incompleteness so it is a wrong thing to do but why ? don't we proof all these sentences in meta so what's the difference ?

  • $\begingroup$ Please insert some parentheses, or better still, a lot of them. The formulas are unreadable. $\endgroup$ Apr 20, 2022 at 13:40
  • $\begingroup$ @AndrejBauer sorry i guess it's fixed now. $\endgroup$ Apr 20, 2022 at 18:28

1 Answer 1


We know from deduction theorem that $(\vdash q\rightarrow\vdash p)\iff (\vdash p\rightarrow q)$

This is false. If $\not\vdash q$ then the clause $(\vdash q)\rightarrow(\vdash p)$ (re-parenthesized for clarity) is vacuously true, regardless of what $p$ is. So just take $q$ to be some independent sentence and set $p=\neg q$; we trivially have $\not\vdash p\rightarrow q$ but $(\vdash q)\rightarrow(\vdash p)$, a counterexample to your claim.

The issue is with your interpretation of the deduction theorem. The deduction theorem says $$\{p\}\vdash q\quad\iff\quad\vdash p\rightarrow q,$$ or more generally $$T\cup\{p\}\vdash q\quad\iff\quad T\vdash p\rightarrow q,$$ but that's very different from what you've written. In particular, the deduction theorem manipulates individual sequents (turning "$\{p\}\vdash q$" into "$\vdash p\rightarrow q$" or similar) rather than hypothetical comparisons of different sequents (such as your "$(\vdash q)\rightarrow(\vdash p)$").

  • 1
    $\begingroup$ this really cleared up my mind thanks, i wrote my interpretation wrong at first and i fixed it now but i got your point i guess. $\endgroup$ Apr 20, 2022 at 22:54
  • $\begingroup$ i just found out wrote my interpretation wrong at first and i fixed it now but i got your point i guess. my problem was that if $\vdash q$ is correct and we can deduce $\vdash p$ from that then $\{q\} \rightarrow p$ is correct too. but i guess $\vdash q \rightarrow \vdash p$ has nothing to with ${q} \rightarrow p$ because $\vdash p$ might be related to other sentences in our logic and it certainly is in case of soundness. $\endgroup$ Apr 20, 2022 at 23:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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