# How to translate classical logic to basic Kripkean logic?

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

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.

• 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 '18 at 16:23
• @guest1806 I mean the former: that it's not the case that ⊨k 򪪪(P → Q). – Eliran Oct 18 '18 at 16:29