Non-commutative propositional logic with short-circuited biconditional and NAND

TL;DR

This paper extends non-commutative propositional logic with short-circuit evaluation by introducing a left-sequential biconditional and NAND, providing complete axiomatizations, including in a three-valued logic setting.

Contribution

It introduces a left-sequential biconditional and NAND operators into MSCL, with complete axiomatizations, including for three-valued logic, advancing the formal understanding of short-circuit logic.

Findings

Complete axiomatization of left-sequential biconditional in MSCL.

Complete axiomatization of left-sequential NAND in MSCL.

Extension of these systems to three-valued logic with completeness results.

Abstract

Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. In programming, short-circuit evaluation is widely used, with left-sequential conjunction and disjunction as primitive connectives. We consider left-sequential, non-commutative propositional logic, also known as MSCL (memorising short-circuit logic), and start from a previously published, equational axiomatisation. First, we extend this logic with a left-sequential version of the biconditional connective, which allows for an elegant axiomatisation of MSCL. Next, we consider a left-sequential version of the NAND operator (the Sheffer stroke) and again give a complete, equational axiomatisation of the corresponding variant of MSCL. Finally, we consider these logical systems in a three-valued setting with a constant for `undefined', and again provide completeness results.