Logical systems with left-sequential versions of NAND and XOR
Cornets de Groot Sven Hugo

Abstract:
In this thesis, we define two new left-sequential connectives ℓNAND and ℓXOR that prescribe a short-circuit evaluation strategy, in which the second argument is evaluated only if the first argument does not suffice to determine the value of an expression, and a full evaluation strategy, in which each argument is evaluated, respectively. First, we define and axiomatize free left-sequential nand logic (FLNL) to investigate which logical laws axiomatize short-circuit evaluation of terms with ℓNAND in a setting where repeated occurrences of the same atomic proposition can yield different Boolean values, that is, modulo free valuation congruence. Then, we define and axiomatize free left-sequential xor logic (FLXL) to investigate which logical laws axiomatize full evaluation of terms with ℓXOR in the same setting. Finally, we investigate expressiveness modulo free valuation congruence of terms with (combinations of) ℓNAND, ℓXOR, left-sequential short-circuit conjunction and disjunction (the primitive connectives of short-circuit logic) and Hoare’s conditional (the primitive connective of proposition algebra).