Almost Duplication-Free Tableau Calculi for Propositional Lax Logics

In this paper we provide tableau calculi for the intuitionistic modal logics LAX and LAX1, where the calculus for LAX1 is duplication-free while among the rules for LAX 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. LAX and LAX1 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.