The metatheory so far has emphasized formulas. The more general first-order theory of Boolean categories must consider statements about both morphisms and formulas together. In this section we consider the equational theory of if-then-else in the “3-valued case” in which the corresponding choice operator is deterministic but not necessarily idempotent as was previously true in Proposition 5.13. Since “if P then α else α = α” is essentially the law of the excluded middle for P, we are therefore allowing such a law to fail, that is, “tests need not halt”. This is realistic in any context in which a test can query the result of an arbitrary computable function.

After characterizing 3-valued if-then-else in Boolean categories we pave the way for the main result, Theorem 14.9 below, as succinctly as possible. The proofs, which are of a universal-algebraic nature, are in [Manes, 1992]; the gap to be bridged in this section is to elevate the results of that paper to the setting of preadditive Boolean categories with projection system. At this time, however, the main result applies only to the semilattice-assertional case.

DEFINITION Let B be a Boolean algebra. The elements of B are “2-valued propositions”. A 3-valued proposition on B is a pair P = (PF, PT) with PF, PT ∈ B, PFPT = 0.