Almost duplication-free tableau calculi for propositional lax logics

Abstract

In this paper we provide tableau calculi for the intuitionistic modal logics PLL and PLL1, where the calculus for PLL1 is duplication-free while among the rules for PLL there is just one rule that allows duplication of formulas. These logics have been investigated by Fairtlough and Mendler in relation to the problem of Formal Hardware Verification. In order to develop these calculi we extend to the modal case some ideas presented by Miglioli, Moscato and Ornaghi for intuitionistic logic. Namely, we enlarge the language containing the usual sings T and F with the new sign Fc. PLL and PLL1 logics are characterized by a Kripke-semantics which is a “weak” version of the semantics for ordinary intuitionistic modal logics. In this paper we establish the soundness and completeness theorems for these calculi.