# A Question on Provability Logic and Co-Necessitation

The provability logic $GL$ has the characteristic axioms:

$K\hspace{15pt}\Box(\alpha\rightarrow \beta)\rightarrow(\Box\alpha\rightarrow\Box\beta)$

$L\hspace{15pt}\Box(\Box \alpha\rightarrow \alpha)\rightarrow\Box \alpha$

In addition $GL$ is equipped with the inference rule of necessitation:

$N\hspace{11pt}\vdash\alpha\Rightarrow\hspace{2pt}\vdash\Box\alpha$

By the De Jong-Sambin Fixed Point Theorem there is a fixed point $\Gamma$ so that $\vdash_{GL}\Gamma\leftrightarrow\lnot\Box\Gamma$.

Is it comme il faut to extend GL with the Co-Necessitation rule

$CN\hspace{11pt}\vdash\Box\alpha\Rightarrow\hspace{2pt}\vdash\alpha$

for $GL+CN$ to capture the Gödelian incompleteness phenomena so that we can conclude that $\nvdash_{GL+CN}\Gamma$ and $\nvdash_{GL+CN}\lnot\Gamma$?

• The CN rule is admissible in GL, but I don't really understand the rest of the question. – Emil Jeřábek Nov 14 '15 at 11:59
• It may be because it really is a sociological question. – Frode Bjørdal Nov 15 '15 at 16:12