Intuitionistic Trilattice Logics

摘要

We take up a suggestion by Odintsov (2009, Studia Logica, 91, 407-428) and define intuitionistic variants of certain logics arising from the trilattice SIXTEEN} introduced in Shramko and Wansing (2005, Journal of Philosophical Logic, 34, 121-153 and 2006, Journal of Logic, Language and Information, 15, 403-424). In a first step, a logic I_(16) is presented as a Gentzen-type sequent calculus for an intuitionistic version of Odintsov's Hilbert-style axiom system L_t (Kamide and Wansing, 2009, Review of Symbolic Logic, 2, 374-395; Odintsov, 2009, Studia Logica, 91, 407-428). The cut-elimination theorem for I_(16) is proved using an embedding of I_(16) into Gentzen's LJ. The completeness theorem with respect to a Kripke-style semantics is also proved for I_(16), The framework of I_(16) is regarded as plausible and natural for the following reasons: (i) the properties of constructible falsity and paraconsistency with respect to some negation connectives hold for I_(16) and (ii) sequent calculi for Belnap and Dunn's four-valued logic (Anderson et al., 1992, Entailment: The Logic of Relevance and Necessity; Belnap, 1977, A useful four-valued logic, In Modern uses of Multiple Valued Logic, pp. 5-37; Dunn, 1976, Philosophical Studies, 29, 149-168) and for Nelson's constructive four-valued logic (Almukdad and Nelson, 1984, Journal of Symbolic Logic, 49, 231-233) are included as natural subsystems of I_(16). In a second step, a logic IT_(16) is introduced as a tableau calculus. The tableau system IT_(16) is an intuitionistic counterpart of Odintsov's axiom system for truth entailment |=_t in SIXTEEN_3, and of the sequent calculus for |=_t, presented in Wansing (2010, Journal of Philosophical Logic, to appear). The tableau calculus is also shown to be sound and complete with respect to a Kripke-style semantics. A tableau calculus for falsity entailment can be obtained by suitably modifying the notion of provability.