I am having trouble understanding whether proving a formula not forced at one node in Kripke semantics is the same as proving that it is not derivable/invalid in Intuitionistic logic.

For example, consider the following diagram from van Dalan's Logic and Structure. $k_0 \not\Vdash \varphi \lor \lnot \varphi$ because $k_0 \not\Vdash \varphi$ and also $k_0 \not\Vdash \lnot\varphi$ since $\exists y \gt k_0$ st $y\Vdash \varphi$.

What I am not sure of is whether this constitute a proof that the law of excluded middle is invalid in Intuitionistic logic (IL). Because this is only one frame among possibly infinitely many in IL, surely just because we can prove that it is false at one node in a frame does not extend that to all frames surely?

And if this is not the way to do it, how do we do it?

enter image description here

  • 1
    $\begingroup$ What have we proved by using Kripke semantics is the excluded middle is not provable from intuitionistic logic, not the excluded middle is invalid. It is a subtle, but I think we should distinguish them. (In fact, $\lnot\lnot(\phi\lor\lnot\phi)$ is a theorem of intuitionistic logic.) $\endgroup$
    – Hanul Jeon
    Dec 27 '19 at 15:00

In general, a formula is not forced by a given node of a frame does not mean it is not forced by any node of arbitrary frames.

Despite that, just finding a frame which does not satisfy a given formula is sufficient to show the unprovability. This is due to the contraposition of the soundness theorem of Kripke frames:

Soundness Theorem. Let $(P,\le,\Vdash)$ be a frame and $p\in P$ be a node. If $\phi$ be a theorem of intuitionistic logic then $p\Vdash\phi$.

Therefore, if $p\nVdash\phi$ for some frame $(P,\le,\Vdash)$ and a node $p\in P$, then $\phi$ is not a theorem of intuitionistic logic. Of course, we do not need to find any other frames if we have already found a frame witnessing the unprovability.

  • $\begingroup$ Thank you; that soundness theorem did the trick. Is it just called the Kripke soundness theorem? I am trying to Google it but I don't seem to be able to find it in the form as written $\endgroup$ Dec 27 '19 at 22:45
  • $\begingroup$ @DanielMak The word "soundness" can be used for any semantics of a given logic. I think van Dalen's book covers soundness theorem for Kripke models and intuitionistic logic. $\endgroup$
    – Hanul Jeon
    Dec 28 '19 at 6:45

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.