History

Please fill in your query. A complete syntax description you will find on the General Help page.
Intuitionistic trilattice logics. (English)
J. Log. Comput. 20, No. 6, 1201-1229 (2010).
Summary: We take up a suggestion by {\it S. P. Odintsov} [Stud. Log. 91, No.~3, 407‒428 (2009; Zbl 1170.03014)] and define intuitionistic variants of certain logics arising from the trilattice $SIXTEEN_{3}$, introduced by {\it Y. Shramko} and {\it H. Wansing} [J. Philos. Log. 34, No.~2, 121‒153 (2005; Zbl 1094.03012); J. Logic Lang. Inf. 15, No.~4, 403‒424 (2006; Zbl 1159.03302)]. 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}$ [{\it N. Kamide} and {\it H. Wansing}, Rev. Symb. Log. 2, No.~2, 374‒395 (2009; Zbl 1174.03008); Odintsov, loc. cit.]. 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 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 and for Nelson’s constructive four-valued logic 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 $\vDash_{t}$ in $SIXTEEN_{3}$ and of the sequent calculus for $\vDash_{t}$ presented in [{\it H. Wansing}, J. Philos. Log. 39, No.~4, 369‒393 (2010; Zbl 1200.03019)]. 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.