Creating and sharing knowledge for telecommunications

On the abstract characterization of broadly truth-functional logics

Marcelino, S. ; Caleiro, C. ; Marcos, J. ; Rivieccio, U.

On the abstract characterization of broadly truth-functional logics, Proc International Joint Conf. on Automated Reasoning - IJCAR, Coimbra, Portugal, Vol. 0, pp. 0 - 0, July, 2016.

Digital Object Identifier:


We overview our ongoing work on tackling the problem of describing relevant subclasses of broadly truth functional logics by means of abstract properties regarding their underlying consequence relations. In previous work we presented weaker versions of the notion of cancellation, an abstract property of a logic that corresponds to being characterizable by a single matrix. In particular, we introduced the notion of Ncancellation that captures the wider class of logics characterizable by a single Nmatrix. We furthermore showed that although the property of Ncancellation is preserved by disjoint fibring, the fact that the component logics are characterizable by finite Nmatrices does not imply that the combined logic is too.

We will now focus on various (independent) abstract properties connected with the nature of a possible matrix semantics for a given logic. Besides cancellation, we consider the properties of n-determinedness (a logic is n-determined for n a natural number, when for all Γ ∪ {φ} we have Γ ⊢ φ if and only if Γσ ⊢ φσ for every substitution σ mapping variables to formulas having (at most) p1 , . . . , pn as variables), local finiteness (a logic is locally finite when for any set of formulas over a finite number of variables, the Tarski congruence relation has only finitely many equivalence classes), local tabularity (a logic is locally tabular when for any set of formulas over a finite number of variables, the Frege derivability equivalence relation has only finitely many equivalence classes). We will study the relative independence between these properties, and ultimately show that combinations of these properties can be used to describe precisely when a logic is characterizable by a family of (at most) n-generated matrices, by a finite family of finite matrices, or by a single finite matrix.

This reports on joint work with Carlos Caleiro, Jo ̃ao Marcos and Umberto Rivieccio.

∗The author thanks the support of EU FP7 Marie Curie PIRSES-GA-2012-318986 project GeTFun: Generalizing Truth- Functionality, and of FEDER/FCT project PEst-OE/EEI/LA0008/2013 and also acknowledges the FCT postdoc grant SFRH/BPD/76513/2011.