Fully Evaluated Left-Sequential Logics
Alban Ponse, Daan J. C. Staudt
TL;DR
This paper develops a hierarchy of fully evaluated left-sequential logics (FELs) based on evaluation-tree semantics and complete equational axiomatisations. It introduces FFEL, MFEL, and their undefinedness extensions, along with two-valued and three-valued Conditional FELs and Static FEL, providing normal forms, tree-structure analyses, and completeness theorems. The work shows deep connections to Bochvar's three-valued logic and to short-circuit logics, and demonstrates independence results for several axiomatisations. The approaches combine normalization via $\text{FNF}$, memorisation and conditional evaluation schemes, and formal verification using Prover9 and Mace4, yielding rigorous, modular axiomatisations for each FEL variant. These results advance both the theory of sequential propositional evaluation and its applications to environments with undefinedness or side effects.
Abstract
We consider a family of two-valued "fully evaluated left-sequential logics" (FELs), of which Free FEL (defined by Staudt in 2012) is most distinguishing (weakest) and immune to atomic side effects. Next is Memorising FEL, in which evaluations of subexpressions are memorised. The following stronger logic is Conditional FEL (inspired by Guzmán and Squier's Conditional logic, 1990). The strongest FEL is static FEL, a sequential version of propositional logic. We use evaluation trees as a simple, intuitive semantics and provide complete axiomatisations for closed terms (left-sequential propositional expressions). For each FEL except Static FEL, we also define its three-valued version, with a constant U for "undefinedness" and again provide complete, independent axiomatisations, each one containing two additional axioms for U on top of the axiomatisations of the two-valued case. In this setting, the strongest FEL is equivalent to Bochvar's strict logic.