Finite Model Property for Modal Ideal Paraconsistent Four-Valued Logic

A modal extension M4CC of Arieli, Avron, and Zamansky's ideal paraconsistent four-valued logic 4CC is introduced as a Gentzen-type sequent calculus. The completeness theorem with respect to a Kripke semantics for M4CC is proved. The finite model property for M4CC is shown by modifying the completeness proof. The decidability of M4CC is obtained as a corollary.