Non-Deterministic Matrices for Combinations of Canonical and Cocanonical Deduction Systems

Bruno Da Ré; Damian Szmuc

doi:10.18778/0138-0680.2026.22

Authors

Bruno Da Ré University of Buenos Aires, Department of Philosophy, Argentina Author https://orcid.org/0000-0002-2958-7840
Damian Szmuc University of Buenos Aires, Department of Philosophy, Argentina Author https://orcid.org/0000-0002-7324-0908

DOI:

https://doi.org/10.18778/0138-0680.2026.22

Keywords:

non-deterministic semantics, Gentzen calculus, substructural logics

Abstract

This article aims to study, proof-theoretically and semantically, Gentzen-style sequent calculi (including possibly Cut-free and Identity-free systems), containing combinations of canonical and cocanonical rules, i.e. Gentzen systems for sequents, with well-behaved forms of left and right introduction and elimination rules for logical expressions. Our main goals are to provide soundness and completeness results for the derivability relations of the target systems in terms of 2-, 3-, or 4-valued non-deterministic semantics, and to give sufficient conditions under which these calculi are prone to produce well-behaved normal derivations of a structurally-atomic analytic-synthetic kind.

References

A. Avron, Tonk—A Full Mathematical Solution, [in:] A. Biletzki (ed.), Hues of Philosophy: Essays in Memory of Ruth Manor, College Publications, London (2010), pp. 17–42.

A. Avron, J. Ben-Naim, B. Konikowska, Cut-Free Ordinary Sequent Calculi for Logics Having Generalized Finite-Valued Semantics, Logica Universalis, vol. 1(1) (2007), pp. 41–70, DOI: https://doi.org/10.1007/s11787-006-0003-6.

A. Avron, B. Konikowska, Multi-Valued Calculi for Logics Based on Non-Determinism, Logic Journal of the IGPL, vol. 13(4) (2005), pp. 365–387, DOI: https://doi.org/10.1093/jigpal/jzi030.

A. Avron, O. Lahav, Canonical Constructive Systems, [in:] M. Giese, A. Waaler (eds.), Automated Reasoning with Analytic Tableaux and Related Methods, vol. 5607 of Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2009), pp. 62–76, DOI: https://doi.org/10.1007/978-3-642-02716-1_6.

A. Avron, I. Lev, Canonical Propositional Gentzen-Type Systems, [in:] R. Goré, A. Leitsch, T. Nipkow (eds.), Automated Reasoning: First International Joint Conference, IJCAR 2001, Siena, Italy, June 18–23, 2001, Proceedings, vol. 2083 of Lecture Notes in Artificial Intelligence, Springer, Berlin, Heidelberg (2001), pp. 529–544, DOI: https://doi.org/10.1007/3-540-45744-5_45.

A. Avron, I. Lev, Non-Deterministic Multiple-Valued Structures, Journal of Logic and Computation, vol. 15(3) (2005), pp. 241–261, DOI: https://doi.org/10.1093/logcom/exi001.

A. Avron, A. Zamansky, Canonical Signed Calculi, Non-Deterministic Matrices and Cut-Elimination, [in:] S. Artemov, A. Nerode (eds.), Logical Foundations of Computer Science: International Symposium, LFCS 2009, Deerfield Beach, FL, USA, January 3–6, 2009, Proceedings, vol. 5407 of Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2009), pp. 31–45, DOI: https://doi.org/10.1007/978-3-540-92687-0_3.

A. Avron, A. Zamansky, Non-Deterministic Semantics for Logical Systems, [in:] D. M. Gabbay, F. Guenthner (eds.), Handbook of Philosophical Logic, 2nd ed., vol. 16, Springer Netherlands, Dordrecht (2011), pp. 227–304, DOI: https://doi.org/10.1007/978-94-007-0479-4_4.

M. Baaz, C. G. Fermüller, G. Salzer, R. Zach, Labeled Calculi and Finite-Valued Logics, Studia Logica, vol. 61(1) (1998), pp. 7–33, DOI: https://doi.org/10.1023/A:1005022012721.

M. Baaz, O. Lahav, A. Zamansky, Effective Finite-Valued Semantics for Labelled Calculi, [in:] B. Gramlich, D. Miller, U. Sattler (eds.), Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26–29, 2012, Proceedings, vol. 7364 of Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2012), pp. 52–66, DOI: https://doi.org/10.1007/978-3-642-31365-3_7.

M. Baaz, O. Lahav, A. Zamansky, Finite-Valued Semantics for Canonical Labelled Calculi, Journal of Automated Reasoning, vol. 51(4) (2013), pp. 401–430, DOI: https://doi.org/10.1007/s10817-013-9273-x.

A. M. Bavosa Castro, A. Borzi, B. Da Ré, A. J. Roffé, J. S. Toranzo Calderón, Tableaux for Metainferential Logics, Journal of Applied Non-Classical Logics, vol. 36(1) (2026), pp. 113–146, DOI: https://doi.org/10.1080/11663081.2025.2573584, published online 3 December 2025.

N. D. Belnap, Jr., A Useful Four-Valued Logic, [in:] J. M. Dunn, G. Epstein (eds.), Modern Uses of Multiple-Valued Logic, vol. 2 of Episteme, D. Reidel Publishing Company, Dordrecht (1977), pp. 5–37, DOI: https://doi.org/10.1007/978-94-010-1161-7_2.

C. Blasio, J. Marcos, H. Wansing, An Inferentially Many-Valued Two-Dimensional Notion of Entailment, Bulletin of the Section of Logic, vol. 46(3/4) (2017), pp. 233–262, DOI: https://doi.org/10.18778/0138-0680.46.3.4.05.

C. Caleiro, S. Marcelino, Modular Many-Valued Semantics for Combined Logics, The Journal of Symbolic Logic, vol. 89(2) (2024), pp. 583–636, DOI: https://doi.org/10.1017/jsl.2023.22.

A. Ciabattoni, K. Terui, Towards a Semantic Characterization of Cut-Elimination, Studia Logica, vol. 82(1) (2006), pp. 95–119, DOI: https://doi.org/10.1007/s11225-006-6607-2.

B. Da Ré, D. Szmuc, Non-Deterministic Semantics for Cocanonical and Semi-Cocanonical Deduction Systems, Journal of Logic and Computation, vol. 35(3) (2025), DOI: https://doi.org/10.1093/logcom/exaf019, article exaf019.

B. A. Dicher, F. Paoli, Logical Metainferentialism, Ergo: An Open Access Journal of Philosophy, vol. 13(9) (2026), pp. 255–297, DOI: https://doi.org/10.3998/ergo.9265.

S. Frankowski, Formalization of a Plausible Inference, Bulletin of the Section of Logic, vol. 33(1) (2004), pp. 41–52.

G. Gentzen, Untersuchungen über das logische Schließen I–II, Mathematische Zeitschrift, vol. 39(1) (1935), pp. 176–210, 405–431, DOI: https://doi.org/10.1007/BF01201353, part I: pp. 176–210, DOI 10.1007/BF01201353; part II: pp. 405–431, DOI 10.1007/BF01201363.

J.-Y. Girard, Y. Lafont, P. Taylor, Proofs and Types, vol. 7 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge (1989).

V. R. Greati, S. Marcelino, J. Marcos, Proof Search on Bilateralist Judgments over Non-Deterministic Semantics, [in:] A. Das, S. Negri (eds.), Automated Reasoning with Analytic Tableaux and Related Methods, vol. 12842 of Lecture Notes in Computer Science, Springer, Cham (2021), pp. 129–146, DOI: https://doi.org/10.1007/978-3-030-86059-2_8.

S. C. Kleene, Introduction to Metamathematics, vol. 1 of Bibliotheca Mathematica, North-Holland Publishing Company and P. Noordhoff N.V., Amsterdam and Groningen (1952).

O. Lahav, Non-Deterministic Matrices for Semi-Canonical Deduction Systems, [in:] Proceedings of the 42nd IEEE International Symposium on Multiple-Valued Logic (ISMVL 2012), IEEE Computer Society, Los Alamitos, CA (2012), pp. 79–84, DOI: https://doi.org/10.1109/ISMVL.2012.48.

O. Lahav, Studying Sequent Systems via Non-Deterministic Multiple-Valued Matrices, Journal of Multiple-Valued Logic and Soft Computing, vol. 21(5–6) (2013), pp. 575–595.

O. Lahav, Y. Zohar, Pure Sequent Calculi: Analyticity and Decision Procedure, ACM Transactions on Computational Logic, vol. 20(3) (2019), pp. 1–38, DOI: https://doi.org/10.1145/3319501, article 13.

G. Malinowski, Q-Consequence Operation, Reports on Mathematical Logic, vol. 24 (1990), pp. 49–59.

S. Marcelino, C. Caleiro, P. Filipe, Computational Properties of Partial Non-Deterministic Matrices and Their Logics, [in:] S. Artemov, A. Nerode (eds.), Logical Foundations of Computer Science: International Symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10–13, 2022, Proceedings, vol. 13137 of Lecture Notes in Computer Science, Springer, Cham (2022), pp. 180–197, DOI: https://doi.org/10.1007/978-3-030-93100-1_12.

S. Negri, J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge (2008), DOI: https://doi.org/10.1017/CBO9780511527340, reprint of the 2001 edition; appendix by Aarne Ranta.

A. Přenosil, Cut Elimination, Identity Elimination, and Interpolation in Super-Belnap Logics, Studia Logica, vol. 105(6) (2017), pp. 1255–1289, DOI: https://doi.org/10.1007/s11225-017-9746-8.

A. N. Prior, The Runabout Inference-Ticket, Analysis, vol. 21(2) (1960), pp. 38–39, DOI: https://doi.org/10.1093/analys/21.2.38.