Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.
Sign up to join this community
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
.
.
.
⊥
p → ⊥
Am I on the right track, or is this not a provable statement?
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.
