Paraconsistent provability logic and rational epistemic agents

A Paraconsistent Provability Logic is presented, developed inside a suitable sequent-formulated system of Paraconsistent Recursive Arithmetic PCA, based on paraconsistent C-systems. PCA allows a paraconsistent reasoning about standard numbers, so that a comparison with Classical and Intuitionistic Arithmetic is possible. PCA has a suitable expressive power and relevant paraconsistency properties, even if it rejects numerical absurdities such as 1=0. The formalization of metatheory in PCA is provided, and the provability predicate PrPCA(.) is studied. The intensional character of the paraconsistent negation is investigated through provability logic tools. The non-triviality of a rec. ax. PCA-extension T, the negation-consistency of T, the classical consistency of T, are formalized inside PCA. It is proved that the provability predicate PrPCA(.) preserves some of the standard properties of the classical provability predicates, but not all of them. A relevant novelty is that the well known Gödel Diagonal Lemma cannot hold for PCA; however, a Paraconsistent Diagonal Lemma for PCA is presented, where the local consistency assertions ◦B of the paraconsistent C-systems play a central role. A possible weakened Hilbert’s program for Paraconsistent Arithmertic is con- jectured. In the second part of the paper a new application for the paraconsistent logical framework is proposed, through a logical formalization of rational agents: an agent Ti is a non trivial paraconsistent system of the form PCA+AxT. Then, the provability predicate PrTi(.) is used as an epistemic predicate. In such a framework, a notion of relevant epistemic interaction between agents is expressed. Existence theorems of a denumerable infinity of societies made by complex and relevantly interacting agents are given, and a complexity hierarchy for the agent’s different possible rationalities is proposed.