Proving unprovability in some normal modal logics
Valentin Goranko · 1991
The present communication suggests deductive systems for the operator ⊣ of unprovability in some particular propositional normal modal logics. We give thus complete syntactic characterization of these logics in the sense of ̷Lukasiewicz: for every formula φ either ⊢ φ or ⊣ φ (but not both) is derivable. In particular, purely syntactic decision procedure is provided for the logics under considerations. All background in modal logic, necessary for this paper can be found in the initial chapters of [1], [3] or [5]. Henceforth we shall informally read S ⊣ φ as “φ is unprovable in S”. All systems presented here will contain the “minimal ” ⊣ ⊢ system ̷L consisting of the axiom: F: ⊣ ⊥ and the rules: