I need to prove the aforementioned formula in modal logic system K, which I am having trouble to do.

Of course, this should be easy to prove if I had access to axiom T, but since it's system K, we can use axioms of necessity and K, the axiom of distribution.

I'd be thankful if someone provided help!

2 Answers 2


Here is a direct proof:

1. ⊢ P → ¬¬P                    A tautology of classical logic 
2. ⊢ □(P → ¬¬P)                 From 1, by the N rule. 
3. □(P → Q) → (□P → □Q)         K axiom. 
4. □(P → ¬¬P) → (□P → □¬¬P)     From 3, by substituting ¬¬P for Q. 
5. □P → □¬¬P                    From 2 and 4, by modus ponens. 
  • This is what I was looking for!
    – l0ner9
    Jun 22 at 18:07

1.¬(◻¬¬P),n (Assuming Indirect Proof)

2.◇¬¬¬P, n (Model Necessity Rule P1)

nAk (This symbolizes access relation of 'n' world to 'k' world

3.¬¬¬P, k((Model Possibility Rule P1)

4.¬P,k(Double Negation P3)

5.P, k(Model Necessity Rule P0)

Closed therefore valid

You must log in to answer this question.

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