# How does negation operate in modal logic?

I was mulling over this proposition: Just because something is provable doesn't mean that it is important; and wanted to consider its contrapositive. How would I write this in formal (modal) logic?

P is provable =>Possibly [not (P important)]

But the contrapostive ( as in formal logic) ought to give is:

not (Possibly [not (P important)])=> not (P is provable)

What does this simplify into?

Your original statement "P provable => not(P important)" would mean that we can only prove unimportant things: if P is provable then P is not important. This isn't the meaning you want, which is why you don't like the contrapositive!

You can fix this using modal logic, as in Mauro's answer. Or you could use quantifiers:

"It is not the case that for all P, (P provable => P important)."

Equivalently:

"There exists some P such that P is provable and unimportant."

You are saying something like :

¬□(Provable(x) → Important(x))

which is :

◊¬(Provable(x) → Important(x)) i.e. ◊(Provable(x) & ¬Important(x)).