Proof theory and mathematical meaning of paraconsistent C-systems

A proof-theoretic analysis and new arithmetical semantics are proposed for some paraconsistent C-systems, which are a relevant sub-class of Logics of Formal Inconsistency (LFIs) introduced by W.A. Carnielli et al. (2002, 2005) [8,9]. The sequent versions BC, CI, CIL of the systems bC, Ci, Cil presented in Carnielli et al. (2002, 2005) 18,91 are introduced and examined. BC, CI, CIL admit the cut-elimination property and, in general. a weakened sub-formula property. Moreover, a formal notion of constructive paraconsistent system is given, and the constructivity of Cl is proven. Further possible developments of proof theory and provability logic of Cl-based arithmetical systems are sketched, and a possible weakened Hilbert's program is discussed. As to the semantical aspects. arithmetical semantics interprets C-system formulas into Provability Logic sentences of classical Arithmetic PA (Artemov and Beklemishev (2004) [2], Japaridze and de Jongh (1998) [19], Gentilini (1999) [15], Smorynski (1991) [221): thus, it links the notion of truth to the notion of provability inside a classical environment. It makes true infinitely many contradictions B boolean AND (sic)B and falsifies many arbitrarily complex instances of noncontradiction principle (sic)(A boolean AND (sic)A). Moreover, arithmetical models falsify both classical logic LK and intuitionistic logic LJ, so that a kind of metalogical completeness property of LFI-paraconsistent logic w.r.t. arithmetical semantics is proven. As a work in progress, the possibility to interpret Cl-based paraconsistent Arithmetic PACI into Provability Logic of classical Arithmetic PA is discussed, showing the role that PACI arithmetical models could have in establishing new meta-mathematical properties. e.g. in breaking classical equivalences between consistency statements and reflection principles. (C) 2011 Elsevier B.V. All rights reserved.