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\'an 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 aziomatisations, 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.
翻译:本文考虑一类二值“全评估左序逻辑”(FELs),其中自由FEL(由Staudt于2012年定义)最具区分性(最弱)且不受原子副作用影响。其次是记忆FEL,其中子表达式的评估结果被记忆。更强的逻辑是条件FEL(受Guzmán和Squier于1990年提出的条件逻辑启发)。最强的FEL是静态FEL,即命题逻辑的序版本。我们使用评估树作为简单直观的语义,并为封闭项(左序命题表达式)提供了完全公理化。对于除静态FEL外的每个FEL,我们还定义了其三值版本,其中包含一个用于表示“未定义”的常数U,并再次提供了完全独立的公理化,每个公理化在二值情况的基础上增加了关于U的两个额外公理。在此设定下,最强的FEL等价于Bochvar的严格逻辑。