Wikipedia:Reference desk/Archives/Mathematics/2020 June 11

Welcome to the Wikipedia Mathematics Reference Desk Archives
The page you are currently viewing is a transcluded archive page. While you can leave answers for any questions shown below, please ask new questions on one of the current reference desk pages.

June 11

The deduction theorem in provability logic

Does the deduction theorem holds in GL logic? Specifically, when Necessitation is defined as it is here, in that it can only be applied with no assumptions before the $\vdash$ (so from $\{\phi \}\vdash \phi$ one may not deduce $\{\phi \}\vdash \square \phi$). The article indicates the answer might be yes, but I have been told by someone whom I am inclined to believe that the answer is no. For some context, mean that GL logic is in some way the same as talking about provability in PA, which (I believe) does have the deduction theorem. — crh23 (Talk) 08:52, 11 June 2020 (UTC)

(I hope the following is not foot-in-mouth, as I am straying from the areas I'm comfortable with.) For the deduction theorem to be applicable, you need a logic that allows assumptions to the left of the turnstyle. Starting with the assumption $p$, unless we have a perverse logic, it should then be the case that

$p\vdash p.$

From the necessitation rule of GL logic given in the Provability logic article, we obtain

$p\vdash \Box p.$

So, if the deduction theorem holds, we obtain now

$\vdash p\rightarrow \Box p.$

Is this a theorem of GL logic? If not, the deduction theorem does not hold. I see no rule for condition introduction other than the distribution axiom and Löb's axiom, and either one requires a box in the antecedent of the conditional, so if I take the definition of GL logic in the Provability logic article for gospel, this cannot be a theorem.  --Lambiam 11:13, 11 June 2020 (UTC)

I think the normal consensus is that $\vdash p\rightarrow \Box p$ is not a theorem in GL logic. However, the necessitation rule does not allow the deduction you state, since it may only be used when there is no assumption to the left of the $\vdash$: the rule is specifically written

• Necessitation: From $\vdash$ p conclude $\vdash$ □p

rather than

• Necessitation: From p conclude □p

(which is how the rule for modus ponens is denoted) --- see section 2 of .— crh23 (Talk) 13:39, 11 June 2020 (UTC)

If $p\rightarrow \Box p$ means what it looks like, it can't be right, because of incompleteness. 2602:24A:DE47:BB20:50DE:F402:42A6:A17D (talk) 20:49, 11 June 2020 (UTC)

To confirm the argument here: the (proof of the) second incompleteness theorem states that if $G$ is such that $\vdash G\leftrightarrow \neg \square G$ then for any $X$ we have $\square G\rightarrow \square X$. As such, if $\vdash G\rightarrow \square G$ we get $\vdash \neg G$ so $\vdash \square X$, i.e. everything is provable. Is that the full argument? — crh23 (Talk) 21:38, 11 June 2020 (UTC)

The incompleteness theorems do not apply to all logics. For example, propositional calculus and first-order predicate logic are (semantically) complete. For the proof of the incompleteness results tto go through you need to be able to express natural number arithmetic in the logic, something you can’t do here.  --Lambiam 21:45, 11 June 2020 (UTC)

Indeed, but does arithmetic soundness and completeness (which I used very carelessly) not show that it is applicable here? — crh23 (Talk) 08:14, 12 June 2020 (UTC)

These results depend on Peano arithmetic (called "PA" in the article), which depends on natural induction being expressible. That requires higher-order logic. For the completeness of first-order logic (which subsumes propositional calculus), see Gödel's completeness theorem.  --Lambiam 14:36, 12 June 2020 (UTC)

In fact I am pretty sure it is, see this proof (sorry, I couldn't be bothered to turn it into wikitext (I'm much faster at LaTeX)) — crh23 (Talk) 09:42, 12 June 2020 (UTC)

My understanding of completeness is: for every formula $P$ of GL,

$\models _{\mathsf {GL}}P~\rightarrow ~\vdash _{\mathsf {GL}}P.$

I am not sure how to interpret the concept of validity in this context, in particular the interpretation of the added logical constant  $\Box$. The fixed point theorem for GL does not depend on arithmetic and has no resemblance to Gödel's construction. The proof you uploaded appears to show that $\vdash p\rightarrow \Box p$ is not a theorem of GL, but is this an incompleteness result?  --Lambiam 14:36, 12 June 2020 (UTC)

Here is what looks to me like a simple syntactic proof that the deduction theorem does not hold for GL.

In what follows, ${\mathcal {P}}$ stands for the set of propositions of GL, and Greek letters stand for members of ${\mathcal {P}}$. Let ${\mathcal {R}}$ stand for the set of propositions $\phi$ such that $\{\phi \}\vdash _{\mathsf {GL}}\Box p$. We introduce the abbreviation $L$ for the proposition $\Box (\Box p\to p)\to \Box p$, and define a sequence of sets $I_{n}$inductively by

$I_{0}~~~~=\{L\},$

$I_{n{+}1}=\{\phi \to \psi ~|~\phi \in {\mathcal {P}}{\setminus }{\mathcal {R}},~\psi \in I_{n}{\setminus }\{\phi \}~\}.$

For example, a typical member of $I_{3}$ is given by $(p{\to }\Box r)\to (q\to (q\to L))$. Since $L$ is an axiom (Löb's axiom), it is certainly the case that $\vdash _{\mathsf {GL}}L$, and therefore that $\{q\}\vdash _{\mathsf {GL}}L$. If the deduction theorem holds for GL, we should then also have $\vdash _{\mathsf {GL}}q\to L$. Note that $q{\to }L~\in ~I_{1}.$ We endeavour to prove by contradiction that no member of any set $I_{n{+}1}$ is a theorem of GL. So assume we have a proof of some member of some $I_{n{+}1}$. Then somewhere along the proof some step is the first one to conclude to a proposition that is a member of $I_{m{+}1}$ for some value of $m$. This proposition has the shape $\phi \to \psi$, where $\psi \in I_{m}$. It is not a tautology of propositional logic. It is also not an instantiation of either of the axioms of GL. What was the rule that led to this proposition as its conclusion? The proposition does not have the right form to be the conclusion of Necessitation. The only remaining possibility is MP: "From $\chi \to (\phi \to \psi )$ and $\chi$, conclude $\phi \to \psi$". If $\chi ~=~\phi {\to }\psi$, then $\chi \in I_{m{+}1}$. And if $\chi ~\neq ~\phi {\to }\psi$, then $\chi {\to }(\phi {\to }\psi )\in I_{m{+}2}$. This means that one of the propositions needed by that rule is a member of some set $I_{m^{\prime }{+}1}$, which is not possible since this step is the first to conclude to such a proposition.  --Lambiam 16:53, 13 June 2020 (UTC)

A note on modal logic, linked to from a web page for a course on mathematical logic, presents a proof that the deduction theorem does not hold for the modal logic K, which is like GL but without Löb's axiom. The proof is essentially the same as the first one I gave above. The definition of GL logic in that note differs in several respects from that given in our article on provability logic, one of which is a different formulation of the necessitation rule. These changes are such, however, that my second, syntactic proof does not go through. Apparently, seemingly subtle changes in the definitions can make all the difference.  --Lambiam 07:20, 14 June 2020 (UTC)