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$– Andrej BauerApr 20, 2022 at 13:40
-
$\begingroup$ @AndrejBauer sorry i guess it's fixed now. $\endgroup$– asha soroushpoorApr 20, 2022 at 18:28
1 Answer
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