Proof of □P ⊢ □¬¬P in modal logic system K

Question

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!

Answer 1

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. 

Answer 2

0.◻P,n
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

---