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$?
