This tutorial overviews a series of concepts, results and techniques that have been yielding new insights in the analysis (and synthesis) of logics in recent years. The covered results establish effective bridges between the semantical and deductive presentations of logics enabling recipes for various practical problems in logic, including procedures to: extracting analytic axiomatizations from a given semantics, over which a series of reasoning activities in a purely symbolic fashion can be performed, including proof search and counter-model generation; constructively updating semantics when imposing new axioms, including language extensions; effectively combining the semantics of two logics capturing the effect of joining their axiomatizations. These bridges depend on working on a generalized context both on the semantical and on the deductive side.

On the one hand we departure from the traditional notion of logic based on SetFmla viewof logical consequence abstractly introduced as a mathematical object via the work of Tarski and his followers, and adopt a more symmetric, multipleconclusion conception of logical consequence of type Set  Set that was studied, initially by Scott [1] and Shoesmith and Smiley [2], according to which a set of conclusions (to be understood disjunctively) may follow from a set of premises (to be understood conjunctively). Both Set  Fmla and Set  Set logics are associated with very natural notions of axiomatizability according to their type, as bases of the logic. In other words, a set of rules axiomatizes a logic if the latter is the smallest logic (consequence relation of according type) containing those rules. Crucially, in both Set  Fmla and Set  Set formulations, the abstract properties defining each type of logic correspond to the machinery of the associated Hilbert-style calculi, where derived consequences using a set of rules R are exactly the ones that hold in the logic axiomatized by R. In the Set  Fmla case, derivations may be written as sequences where the application of a rule produces a new formula, and in the Set  Set case the proofs take an arboreal shape since the application of the rules produces a set of formulas, each corresponding to a child of the node where it was applied. The second notion strictly generalizes the first, as derivations using only single-conclusion rules coincide in both settings.

On the other hand we also depart from the traditional approach in logic of using (total and deterministic) semantics based on logical matrices and adopting a partial non-deterministic generalization of the standard logic matrix semantics based on PNmatrices. PNmatriceswere introduced in [3], as a generalization of non-deterministic matrices (Nmatrices) that on their turn were proposed in the beginning of this century by Avron and his collaborators [4, 5]. In PNmatrices the connectives are interpreted by (partial) multi-functions instead of functions. The central idea is that a connective can non-deterministically pick from a set of possible values instead of its value being completely determined by the input values.

A surprising advantage of the Set  Set environment, perhaps, is on the proof-theoretical front. In their far-reaching monograph [2], Shoesmith and Smiley showed that the Set  Set consequence relation determined by any finite matrix can be finitely axiomatized using Set  Set rules. In [19, 20] a generalization of this procedure is presented and shown to be applicable PNmatrices satisfying a natural expressivity requirement. However, the surprises do not end here, as the obtained Set  Set calculi are analytic (based on the generalized notion of subformula mentioned above). Analytic calculi are valuable tools in logic, allowing not only for the implementation of symbolic decision procedures for the validity problem, but also proof-search and counter-model generation.

Furthermore, PNmatrices can finitely characterize logics that do not have finite semantics based on (total deterministic) matrices [6], and has proven relevant in a myriad of recent compositional results in logic [3, 5, 7, 8, 9], namely as semantical counterparts of certain families of sequent calculi. Indeed PNmatrices are very malleable. The operation Bridges between semantics and proof-calculi UNILOG 2022 of replicating values in a PNmatrix is called expansion and the operation of deleting elements from the possible values of a certain connective in a given input is called refinement. When an expansion is followed by a refinement we obtain a rexpansion [10]. In [11] a general construction for axiomatic extensions based on rexpansions is introduced, yielding denumerable PNmatrix semantics for classically and intuitionistically based modal logics. The same paper also includes a sharper construction, albeit not universal, extending the strategy introduced in [8], that allows a finiteness-preserving effective method for calculating the effect of imposing a finite number of extra axioms and subsumes methods based on twist [12, 13] and swap constructions [14].

Considering Hilbert-style calculi fares well on the compositional front, as given two logics of compatible type axiomatized by sets of rules R1 and R2 (of according type), their fibring, the smallest logic (of the same type) in the combined language that contains both, is axiomatized by R1 ä R2. In [15, 16] it is shown how to effectively combine the semantics of logics characterized by PNmatrices capturing the result of their fibring. In the Set  Set environment the combination mechanism preserves finite-valuedness, but in the SetFmla framework this property may be broken. These advantages of the multiple-conclusion environment come without the usual price on the compositionality front of introducing meta-level language in the calculi as is the case in the most used alternatives: sequent calculi, natural deduction and labelled tableaux. Allowing for a purely internal view of logic which fits well with the compositional approach, granting a finer control on the origin of the interactions and tracking the increases in complexity.

These advances form the basis of a modular approach to compositionality that allows for a wider understanding of the effects of tuning the key logical parameters: language, semantics and proof system, and the mechanisms that influence the growth of complexity in reasoning tasks.

1. Problems: the key ingredients to solve them

– Generalized consequence relations and calculi

* Single- vs Multiple-conclusion logics (Set  Fmla vs Set  Set )

* Linear vs Arboreal Hilbert-style proofs

– Generalized semantics

* Semantics based on partial and non-deterministic logical matrices

* Novelties brought by partiality and non-determinism

2. From semantics to analytical axiomatizations

– Generating calculli from semantics

* Monadicity (1-separability)

* Procedure for axiomatizing under expressivity requirement of monadicity

– Analytical calculli

* Generalized subformula property, analyticity

* Procedures for counter-model generation and proof-search

3. From calculi to semantics

– Rexpansions and adding axioms

* Universal recipe for adding axioms, flat ([) construction: denumerable semantics for axiomatic

strengthnings of logics characterized by denumerable PNmatrices

* ]-construction: look-aheads and finiteness preserving constructive update of rexpansions of Pmatrices

with simple axioms

– Semantics of combining logics

* Combining logics by joining axiomatizations (fibring)

* Semantics of fibring Set  Fmla and Set  Set logics

References

[1] D. Scott. Completeness and axiomatizability in many-valued logic. In L. Henkin, J. Addison, C. Chang,W. Craig, D. Scott, and R. Vaught, editors, Proceedings of the Tarski Symposium, volume XXV of Proceedings of Symposia in Pure Mathematics, pages 411–435. American Mathematical Society, 1974.

[2] D. Shoesmith and T. Smiley. Multiple-Conclusion Logic. Cambridge University Press, 1978.

[3] M. Baaz, O. Lahav, and A. Zamansky. Finite-valued semantics for canonical la- belled calculi. Journal of Automated Reasoning, 51(4):401–430, 2013.

[4] A. Avron and I. Lev. Non-deterministic multiple-valued structures. Journal of Logic and Computation, 15(3):241– 261, 2005.

[5] A. Avron and A. Zamansky. Non-deterministic semantics for logical systems. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 16, pages 227–304. Springer, 2011.

[6] C. Caleiro, S. Marcelino, and U. Rivieccio. Characterizing finite-valuedness. Fuzzy Sets and Systems, 345:113–125, 2018.

[7] Arnon Avron, Jonathan Ben-Naim, and Beata Konikowska. Cut-free ordinary sequent calculi for logics having generalized finite-valued semantics. Logica Universalis, 1(1):41–70, 2007.

[8] Agata Ciabattoni, Ori Lahav, Lara Spendier, and Anna Zamansky. Taming paraconsistent (and other) logics: An algorithmic approach. ACM Transactions on Computational Logic, 16(1):5–23, December 2014.

[9] C. Caleiro, S. Marcelino, and J. Marcos. Combining fragments of classical logic: When are interaction principles needed? Soft Computing, 23(7):2213–2231, 2019.

[10] A. Avron and Y. Zohar. Rexpansions of non-deterministic matrices and their applications in non-classical logics. Review of Symbolic Logic, 12(1):173–200, 2019.

[11] C. Caleiro. and S. Marcelino. On axioms and rexpansions. In: Arieli O., Zamansky A. (eds) Arnon Avron on Semantics and Proof Theory of Non-Classical Logics. Outstanding Contributions to Logic, vol 21. Springer, Cham.

[12] S. Odintsov. Constructive Negations and Paraconsistency, volume 26 of Trends in Logic. Springer Netherlands, 2008.

[13] H. Ono and U. Rivieccio. Modal twist-structures over residuated lattices. Logic Journal of the IGPL, 22 (3), 2014, p. 440-457.

[14] M. Coniglio and A. Golzio. Swap structures semantics for Ivlev-like modal logics. Soft Computing, 23(7):2243–2254, 2019.

[15] S. Marcelino and C. Caleiro. Disjoint fibring of non-deterministic matrices. In R. de Queiroz J. Kennedy, editor, Logic, Language, Information and Computation (WoLLIC 2017), volume 10388 of LNCS, pages 242–255. Springer, 2017.

[16] C. Caleiro and S. Marcelino. Partial non-deterministic compositional semantics for propositional logics, submitted

[17] W. Blok and D. Pigozzi. Algebraizable logics. Number 396 in Memoirs of the AMS. American Mathematical Society, 1989.

[18] J. Font. Abstract Algebraic Logic - An Introductory Textbook. College Publications, 2016.

[19] S. Marcelino and C. Caleiro. Axiomatizing non-deterministic many-valued generalized consequence relations. Synthese, 2019.

[20] C. Caleiro and S. Marcelino. Analytic calculi for monadic PNmatrices. In Logic, Language, Information, and Computation (WoLLIC 2019), volume 11541 of LNCS, pages 84–98. Springer, 2019.

[21] W. Rautenberg. 2-element matrices. Studia Logica, 40(4):315–353, 1981.

[22] A.Wro«ski. A three element matrix whose consequence operation is not finitely based. Bulletin of the Section of Logic, 2(8):68–70, 1979.

[23] S. Gottwald. A Treatise on Many-Valued Logic. Research Studies Press (2001)

[24] J. Ivlev. A semantics for modal calculi. Bulletin of the Section of Logic, 17(3–4):114–121, 1988.

[25] J. Kearns. Modal semantics without possible worlds. Journal of Symbolic Logic, 46(1):77–86, 1981.

[26] W. Carnielli, M. Coniglio, and J. Marcos. Logics of formal inconsistency. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 14. Kluwer, 2007.

[27] W.Carnielli and J.Marcos. A taxonomy of C-systems. In W.Carnielli, M.Coniglio, and I. D’Ottaviano, editors, Paraconsistency: The logical way to the inconsistent, volume 228 of Lecture Notes in Pure and Applied Mathematics, pages 1–94. Marcel Dekker, 2002.

[28] D. Nelson. Constructible falsity. Journal of Symbolic Logic, 14:247–257, 1948.

[29] D. Vakarelov. Notes on N-lattices and constructive logic with strong negation. Studia Logica: An International Journal for Symbolic Logic, 36(1/2):109–125, 1977.

[30] M. Kracht. On extensions of intermediate logics by strong negation. Journal of Philosophical Logic, 27:49–73, 1998.

[31] N. Belnap. How a computer should think. In G. Ryle, editor, Contemporary Aspects of Philosophy, volume 2 of Episteme, pages 30–55. Oriel Press, 1977.

[32] N. Belnap. A useful four-valued logic. In G. Epstein J.M. Dunn, editor, Modern Uses of Multiple-Valued Logic, volume 2 of Episteme, pages 5–37. Oriel Press, 1977.

[33] D’Agostino. Informational Semantics, Nmatrices and Feasible Deduction. ENTCS, 2014