Evaluation Trees and Normalisation for Proposition Algebra

Proposition algebra is based on Hoare’s conditional, a ternary connective comparable to if–then–else and used in the context of propositional logic. Conditional statements are composed from atomic propositions (propositional variables), constants for the Boolean truth values, and the conditional. In previous work, various equational axiomatisations have been defined, each of which leads to a so-called valuation congruence. The weakest of these is “free valuation congruence” and the strongest is “static valuation congruence”, which is equivalent to propositional logic. Free valuation congruence is axiomatised by four simple equational axioms, and we use evaluation trees to give a simple semantics: two conditional statements are free valuation congruent if, and only if, they have equal evaluation trees. Increasingly stronger valuation congruences arise by adding axioms to the four that define free valuation congruence: repetition-proof, contractive, memorising, and static valuation congruence. We prove that each such valuation congruence C can be characterised using a transformation on evaluation trees: two conditional statements are C-valuation congruent if, and only if, their C-transformed evaluation trees are equal. In order to prove that these transformations preserve the congruence property, we use normalisation functions: two conditional statements are C-valuation congruent if, and only if, the C-normalisation function returns equal images. Our framework provides the first comprehensive tree-based semantics that unifies all major valuation congruences in proposition algebra, offering both conceptual clarity and practical decision procedures.