Paraconsistent Arithmetic with a Local Consistency Operator and Global Selfreference

The Provability Logic and Proof-Theory of the system of Paraconsistent Arithmetic PRACI are presented. PRACI is based on the paraconsistent predicate calculus CI corresponding to the C-system Ci introduced by Carnielli et al. [W.A. Carnielli, M.E. Coniglio, J. Marcos, Logics of formal inconsistency, in D. Gabbay, F. Guenthner eds., Handbook of Philosophical Logic, volume 14, Kluwer Academic Publishers, 2005]. PRACI can support an infinity of contradictions B∧¬B without trivializing, but reject identifications between different numbers such as 0=1. In PRACI a new propositional connective °(.) is added, so that °A can be read as “A is consistent”. We obtain a system with a local selfreference, based on the local consistency assertions °A, and a global selfeference, based statements involving PrPRACI(.). The fundamental relation PrT(#°B)→¬PrT(#B) betweeen local and global consistency is investigated. It states that in a paraconsistent setting, the provability of the non-trivialty of Arithmetic could be reduced to that of some suitable local consistency assertions, so that we can speak of a possible weakened Hilbert's program.