The main aim of this paper is to introduce the logics of evidence and truth $$LET_{K}^+$$ and $$LET_{F}^+$$ together with sound, complete, and decidable six-valued deterministic semantics for them. These logics extend the logics $$LET_{K}$$ and $$LET_{F}^-$$ with rules of propagation of classicality, which are inferences that express how the classicality operator $${\circ }$$ is transmitted from less complex to more complex sentences, and vice-versa. The six-valued semantics here proposed extends the 4 values of Belnap-Dunn logic with 2 more values (...) that intend to represent (positive and negative) reliable information. A six-valued non-deterministic semantics for $$LET_{K}$$ is obtained by means of Nmatrices based on swap structures, and the six-valued semantics for $$LET_{K}^+$$ is then obtained by imposing restrictions on the semantics of $$LET_{K}$$. These restrictions correspond exactly to the rules of propagation of classicality that extend $$LET_{K}$$. The logic $$LET_{F}^+$$ is obtained as the implication-free fragment of $$LET_{K}^+$$. We also show that the 6 values of $$LET_{K}^+$$ and $$LET_{F}^+$$ define a lattice structure that extends the lattice L4 defined by the Belnap-Dunn four-valued logic with the 2 additional values mentioned above, intuitively interpreted as positive and negative reliable information. Finally, we also show that $$LET_{K}^+$$ is Blok-Pigozzi algebraizable and that its implication-free fragment $$LET_{F}^+$$ coincides with the degree-preserving logic of the involutive Stone algebras. (shrink)

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. Here, we intend to make a first step in this 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_s. (...) 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 relationships 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ütte’s technique. (shrink)