Proof-theoretic aspects of paraconsistency with strong consistency operator

Abstract

In order to develop efficient tools for automated reasoning with inconsistency (theorem provers), eventually making Logics of Formal inconsistency (LFI) a more appealing formalism for reasoning under uncertainty, it is important to develop the proof theory of the first-order versions of such LFI's. In our work, we intend make a first step in that direction. On the other hand, the logic Ciore was developed to provide new logical systems in the study of inconsistent databases from the point of view of LFI. An interesting fact about Ciore is that it has a strong consistency operator, that is, a consistency operator which (forward/backward) propagates inconsistency. Also, it turns out to be an algebraizable logic (in the sense of Blok and Pigozzi) that can be characterized by means of a 3-valued logical matrix. Recently, a first-order version of Ciore, namely QCiore, was defined preserving the spirit of Ciore, that is, without introducing unexpected relations between the quantifiers. Besides, some important model-theoretic results were obtained for this logic. In this paper we study some proof--theoretic aspects of both Ciore and QCiore respectively. In first place, we introduce a two-sided sequent system for Ciore. Later, we prove that this system enjoys the cut-elimination property and apply it to derive some interesting properties. Later, we extend the above-mentioned system to first-order languages and prove completeness and cut-elimination property using the well-known Sh\"utte's technique.