I am working on a proof of ~◻p → ~p in System K. It says "If it is not the case that p is necessarily true, then p is not true". I have turned all the abbreviated symbols into their primitive ones so I get:

(◻p → ⊥) → (p → ⊥)

I have made partial progress, but I cannot seem to finish the proof:

◻p → ⊥
p → ⊥

Am I on the right track, or is this not a provable statement?

  • 1
    You cannot prove that. It has a countermodel in which p is false at some accessible possible world, but true at the actual world.
    – Bumble
    Oct 2, 2021 at 7:49

1 Answer 1


Am I on the right track, or is this not a provable statement?

I'm going to go further than that. Not only is this statement not provable in K, but in fact there is no reasonable set of axioms under which a proof should exist.

We can see this by taking the contrapositive. If you can prove ~◻p → ~p, then you can also prove p → ◻p. And since we know nothing at all about p, you should be able to write the same proof for every proposition in the domain of discourse. Therefore, the only models which satisfy this property are models in which all accessible worlds are identical (have the same truth values for all propositions) to the actual world. But that renders the whole modal logic system trivial. If all accessible worlds are identical to the actual world, then you might as well not bother with modal logic at all, and go back to first-order logic. There's no situation where it makes sense to import all the semantical complexity of modal logic, and then structure your axioms in such a way that this complexity is rendered useless.

I imagine that you might have intended to write ~♢p → ~p, which is at least true in system T (because it's equivalent to ◻~p → ~p, which is just axiom T with ~p instead of p). But it's still not provable in system K, because K does not require that the actual world is accessible.

  • Thanks for the explanation. The contrapositive explanation made it very clear. To be clear, I wrote what I intended, and I do not think there is anything bad about being wrong about it. I learnt something new.
    – Josh
    Oct 4, 2021 at 1:32

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