A constructive proof of the Craig’s interpolation theorem for QCiore

The logic Ciore was introduced with the aim of providing new logical systems that axiomatize formal representations of inconsistency (here, equivalent to contradictoriness) in classical logic. The idea was to present a general formal system apt to handle contradictions in informatics, in particular, in the management of databases. A first order version of Ciore, QCiore, was presented and studied by Coniglio, Gomez-Pereira, and M. Figallo. These authors provided a partial structures semantics for QCiore, which generalizes the semantic notion of quasi-truth considered by Mikeberg, da Costa, and Chuaqui. Besides, some important results of classical Model Theory were obtained for this logic. Recently, a sequent system for QCiore, GQCiore, was presented and proved that this system enjoys the cut-elimination property. In this paper, following Maehara’s method, we provide a constructive proof of the Craig’s interpolation theorem for QCiore as an application of the cut-elimination property of GQCiore.