I'm trying to semantically prove the following argument (sorry about the formatting - I'm new to stackexchange):

if P ⊨c Q then ⊨k 򪪪(P → Q)

However, I don't know how to translate or relate the classical logic on the left to the Kripke logic on the right. Can anyone help?

1 Answer 1


There's really no translation to be done. Here's an outline of a proof.

Assume P ⊨c Q. To show ⊨k 򪪪(P → Q), assume for contradiction that 򪪪(P → Q) is not valid. This means that there's a world which falsifies P → Q, that is, in which P is true but Q is false. But that contradicts the assumption that Q follows classically from P.

  • 1
    Is what you want to assume to obtain the contradiction ~⊨{sub}k{/sub} 򪪪(P → Q) or ~ 򪪪(P → Q) ? (I'm not familiar w/ Kripke logic so I'm not sure whether "assume X is not valid" is supposed to refer to the entailment or the implication)
    – guest1806
    Oct 18, 2018 at 16:23
  • 2
    @guest1806 I mean the former: that it's not the case that ⊨k 򪪪(P → Q).
    – E...
    Oct 18, 2018 at 16:29

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .