Norihiro Kamide

It is known that many-valued paraconsistent logics are useful for expressing uncertain and inconsistency-tolerant reasoning in a wide range of Computer Science. Some four-valued and sixteen-valued logics have especially been well-studied. Some four-valued logics are not so fine-grained, and some sixteen-valued logics are enough fine-grained, but rather complex. In this paper, a natural eight-valued paraconsistent logic rather than four-valued and sixteen-valued logics is introduced as a Gentzen-type sequent calculus. This eight-valued logic is enough fine-grained and simpler than sixteen-valued logic. A triplet valuation semantics is introduced for this logic, and the completeness theorem for this semantics is proved. The cut-elimination theorem for this logic is proved, and this logic is shown to be decidable.

[1] A. Almukdad and D. Nelson, Constructible falsity and inexact predicates, Journal of Symbolic Logic 49:1 (1984), 231–233.

[2] O. Arieli and A. Avron, Logical bilattices and inconsistent data, Proceedings of the

9th IEEE Annual Symposium on Logic in Computer Science, IEEE Press, 1994, pp. 468–476.

[3] O. Arieli and A. Avron, Reasoning with logical bilattices, Journal of Logic, Language and Information 5 (1996), 25–63.

[4] N. D. Belnap, useful four-valued logic, in: J.M. Dunn and G. Epstein (eds.), Modern Uses of Multiple-Valued Logic, Reidel, Dordrecht, 1977, pp. 5–37.

[5] J. M. Dunn, Intuitive semantics for first-degree entailment and ‘coupled trees’, Philo- sophical Studies 29:3 (1976), 149–168.

[6] Y. Gurevich, Intuitionistic logic with strong negation, Studia Logica 36 (1977), 49–59.

[7] N. Kamide, On natural eight-valued reasoning, Proceedings of the 43rd IEEE Inter- national Symposium 
on Multiple-Valued Logic (ISMVL 2013), pp. 231–236.

[8] N. Kamide and H. Wansing, Combining linear time temporal logic with construc- tiveness and paraconsistency, Journal of Applied Logic 8 (2010), 33–61.

[9] N. Kamide and H. Wansing, A paraconsistent linear-time temporal logic, Funda- menta Informaticae 106:1 (2011), 1–23.

[10] N. Kamide and H. Wansing, Completeness and cut-elimination theorems for trilat- tice logics, Annals of Pure and Applied Logic 162:10 (2011), 816–835.

[11] N. Kamide and H. Wansing, Proof theory of Nelson’s paraconsistent logic: A uniform perspective, Theoretical 
Computer Science 415 (2012), 1–38.

[12] D. Nelson, Constructible falsity, Journal of Symbolic Logic 14 (1949), 16–26.

[13] S. POdintsov, On axiomatizing Shramko-Wansing’s logic, Studia Logic91:3 (2009), 407–428.

[14] W. Rautenberg, Klassische und nicht-klassische Aussagenlogik, Vieweg, Braun- schweig, 1979.