1 Propositional modal logic