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

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!

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! Commented Jun 22, 2023 at 18:07

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