Mapping the Logic of If: A Machine-Checked Classification of Seventeen Conditional Principles

We treat the indicative conditional as an arbitrary binary operation on a Boolean algebra of propositions and classify all 131,072 combinations of seventeen principles from the literature on conditionals. A combination collapses when the material conditional is the only operation that obeys it, and it is inconsistent when no operation obeys it on any algebra with more than two elements. We find 89 minimal bad combinations: 63 collapse and 26 are inconsistent. The consistent combinations form 12 maximal sets. Three of these keep Modus Ponens, Identity and Right Weakening: the strict conditional, Stalnaker's C2, and a conditional we call consequent-or-strict. All results hold on every Boolean algebra. Two results avoid Modus Ponens. Import-Export, Contraposition and the rule that "if true, then b" equals b together force the material conditional. Import-Export, Identity and Conditional Non-Contradiction have no model on any algebra with more than two elements. Gibbard's collapse holds with only the Export half of Import-Export, while every weaker form of Import-Export we tested blocks the first result. The Z3 solver checked each proof step, and an independent checker re-verified all 392 finite models. The supplementary archive contains the encodings, model certificates, proof scripts, a Lean 4 formalization of the main theorems (not yet compiled), and the LaTeX source.