Truth and Falsehood pp 143-170 | Cite as

# Intuitionistic Trilattice Logics

## Abstract

We will take up a suggestion by Odintsov
(Studia Logica 93:407–428, 2009) and define intuitionistic variants of certain logics arising from the trilattice \(SIXTEEN_3.\) In a first step, a logic \(\hbox{I}_{16}\) is presented as a Gentzen-type sequent calculus
for an intuitionistic version of Odintsov’s Hilbert-style axiom system
\(L_{T}\) from Chap. 5. The cut-elimination theorem for \(\hbox{I}_{16}\) is proved using an embedding of \(\hbox{I}_{16}\) into Gentzen’s sequent system *LJ* for intuitionistic logic. The completeness theorem with respect to a Kripke-style semantics is also proved for \(\hbox{I}_{16}.\) The framework of \(\hbox{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 \(\hbox{I}_{16},\) and (ii) sequent calculi for Belnap
and Dunn’s
four-valued logic of first-degree entailment and for
Nelson’s
constructive paraconsistent logic **N4** are included as natural subsystems of \(\hbox{I}_{16}.\) In a second step, a logic \(\hbox{IT}_{16}\) is introduced as a tableau calculus. The tableau system \(\hbox{IT}_{16}\) is an intuitionistic counterpart of Odintsov’s axiom system for truth entailment \(\models_t\) in \(SIXTEEN_3\) and of the sequent calculus for \(\models_t\) presented in Chap. 6. 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.