Published in Volume XXXV, Issue 2, 2025, pages 161–196, doi:10.47743/SACS.2025.2.161
Author: J. A. Bergstra, A. Ponse
Abstract
Three-valued conditional logic (CL), defined by Guzmán and Squier (1990) and based on McCarthy’s noncommutative connectives, axiomatises a short-circuit logic (SCL), that is, a logic that prescribes short- circuit evaluation of conjunction and disjunction. CL defines more identities than three-valued MSCL (Memorising SCL, which also has a two-valued variant). This follows from the fact that the definable connective that prescribes full left-sequential conjunction is commutative in CL.
We observe that CL also has a two-valued variant of which the full left-sequential connectives and negation define a commutative logic that is weaker than propositional logic because the absorption laws do not hold.
Next, we show that the original, equational axiomatisation of CL is not independent and give several alternative, independent axiomatisations.
Finally, we show that in CL, the full left-sequential connectives and negation define Bochvar’s three-valued logic. The paper ends with an appendix on the use of Prover9 and Mace4.
References
[1] Jan A. Bergstra, Inge Bethke, and Piet Rodenburg. A propositional logic with 4 values: true, false, divergent and meaningless. Journal of Applied Non-Classical Logics, 5(2):199–217, 1995. doi:10.1080/11663081.1995.10510855.
[2] Jan A Bergstra, Jan Heering, and Paul Klint. Module algebra. Journal of the ACM, 37(2):335–372, 1990. doi:10.1145/77600.77621.
[3] Jan A. Bergstra and Alban Ponse. Proposition algebra. ACM Transactions on Computational Logic, 12(3), 2011. doi:10.1145/1929954.1929958.
[4] Jan A. Bergstra and Alban Ponse. Evaluation trees for proposition algebra, 2017. arXiv:1504.08321.
[5] Jan A. Bergstra and Alban Ponse. Fracterm calculus for partial meadows, 2025. arXiv:2502.13812.
[6] Jan A. Bergstra, Alban Ponse, and Daan J. C. Staudt. Short-circuit logic, 2013. (v4, first version v1 appeared in 2010). arXiv:1010.3674.
[7] Jan A. Bergstra, Alban Ponse, and Daan J. C. Staudt. Non-commutative propositional logic with short-circuit evaluation. Journal of Applied Non- Classical Logics, 31(3-4):234–278, 2021. doi:10.1080/11663081.2021.2010954.
[8] Dmitry Anatolévich Bochvar. Ob odnom tréhznacnom isčislenii i égo priménénii k analiza paradoksov klassičékogo râssirénnogo funkcional’nogo isčislénid. Matématičeskij Sbornik, 4:287–308, 1939. Translation: Dmitry Anatolévich Bochvar and Merrie Bergmann (1981). On a three-valued logical calculus and its application to the analysis of the paradoxes of the classical extended functional calculus. History and Philosophy of Logic, 2(1-2), 87-112. doi:10.1080/01445348108837023.
[9] Alonzo Church. Conditioned disjunction as a primitive connective for the propositional calculus. Portugaliae Mathematica, 7:87–90, 1948. URL: https://purl.pt/2171/1/j-5293-b-vol7-fasc2-art3_PDF/j-5293-b-vol7-fasc2-art3_PDF_01-B-R0300/j-5293-b-vol7-fasc2-art3_0000_capa1-90_t01-B-R0300.pdf.
[10] Alonzo Church. Introduction to Mathematical Logic. Princeton University Press, 1956. Also published as a paperback edition. De Gruyter Brill, 1991. doi:10.1515/9781400881451.
[11] David Gries. The Science of Programming. Texts and Monographs in Computer Science. Springer, 1981. doi:10.1007/978-1-4612-5983-1.
[12] Fernando Guzmán. A Gentzen system for conditional logic. Studia Logic, 53:243–257, 1994. doi:10.1007/978-1-4612-5983-1.
[13] Fernando Guzmán and Craig C. Squier. The algebra of conditional logic. Algebra Universalis, 27:88–110, 1990. doi:10.1007/BF01190256.
[14] Charles Antony Richard Hoare. A couple of novelties in the propositional calculus. Mathematical Logic Quarterly, 31(9-12):173–178, 1985. doi:10.1002/malq.19850310905.
[15] John McCarthy. A basis for a mathematical theory of computation. In Paul Braffort and David Hirschberg, editors, Computer Programming and Formal Systems, volume 35 of Studies in Logic and the Foundations of Mathematics, pages 33–70. Elsevier, 1963. doi:10.1016/S0049-237X(08)72018-4.
[16] John McCarthy. Predicate calculus with “undefined” as a truth-value, 1963. Stanford Artificial Intelligence Project Memo I (5 pages). URL: https://stacks.stanford.edu/file/druid:zc129sh9123/SC1041 _SAIL_AIM_001.pdf.
[17] William McCune. The GUI: Prover9 and Mace4 with a graphical user interface. Prover9-Mace4 Version 0.5B, 2008. Prover9-Mace4-v05B.zip, March 14, 2008. URL: https://www.cs.unm.edu/~mccune/prover9/gui/v05.html.
[18] Alban Ponse and Daan J. C. Staudt. An independent axiomatisation for free short-circuit logic. Journal of Applied Non-Classical Logics, 28(1):35–71, 2018. doi:10.1080/11663081.2018.1448637.
[19] Alban Ponse and Daan J. C. Staudt. Fully evaluated left-sequential logics, 2024. arXiv:2403.14576.
[20] Daan J. C. Staudt. Completeness for two left-sequential logics, 2012. arXiv:1206.1936.
Bibtex
@article{sacscuza:Bergstra2025clscl,
title={Conditional Logic as a Short-Circuit Logic},
author={J. A. Bergstra, A. Ponse},
journal={Scientific Annals of Computer Science},
volume={35},
number={2},
organization={Alexandru Ioan Cuza University, Ia\c si, Rom\^ania},
year={2025},
pages={161-196},
publisher={Alexandru Ioan Cuza University Press, Ia\c si},
doi={10.47743/SACS.2025.2.161}
}