2
$\begingroup$

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

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.