The first example of an intuitively meaningful propositional logic without the finite model property, and still the simplest one in the literature. The question of its decidability appears still to be open.

Complete deductive systems are constructed for the non-valid (refutable) formulae and sequents of some propositional modal logics. Thus, complete syntactic characterizations in the sense of Lukasiewicz are established for these logics and, in particular, purely syntactic decision procedures for them are obtained. The paper also contains some historical remarks and a general discussion on refutation systems.