Constructive dilemma: (A → B) AND (C → D), A OR C, therefore B OR D

Q: Is there a destructive dilemma too?

Yes: from (A -> B) AND (C -> D) and NOT B OR NOT D, conclude NOT A OR NOT C. It is the contrapositive version of this argument and can be entered into the validity checker the same way, with the same four variables and sixteen rows.

Constructive dilemma: from (A -> B) AND (C -> D) and A OR C, conclude B OR D. Four variables, a sixteen-row table, and a validity check that holds on every row.

Two implications and the knowledge that at least one antecedent holds give at least one consequent: if it rains the match is cancelled, if it snows the roads close, and it will rain or snow, so the match is cancelled or the roads close. The model has four variables, the premises p1, (A -> B) AND (C -> D), and p2, A OR C, and the conclusion B OR D. The engine's reading of the conclusion is “at least one of B or D is true, both may be true”.

The validity check holds across the sixteen rows: no admissible assignment makes both premises true and the conclusion false. The premise-consistency check holds with the witness A = FALSE, B = FALSE, C = TRUE, D = TRUE, where the second implication fires through C and D. On the table p2 is false on the four rows where A and C are both false, and p1 is false on the seven rows where some implication is broken; every remaining row has B or D true, which is what the exhaustive search confirms. No counterexample is reported because none exists.

Dilemmas structure case analyses in code reviews and incident reports: whichever of two conditions caused the alert, each leads to a consequence we can act on. They also underlie exhaustive match statements, where each arm's guard implies its result and the arms together cover the input. The thing to watch is coverage: A OR C is the premise that says the cases are exhaustive, and if it is false in reality the dilemma concludes nothing, however sound the two implications are.

p1 — (A -> B) AND (C -> D) · premisep2 — A OR C · premiseconclusion — B OR D · conclusion

Exact checks

Does the conclusion follow from the premises? Yes · Exhaustively checked and solver cross-checked · 16 rows

Can all premises be true together? Yes Example assignment: A = F, B = F, C = T, D = T · Exhaustively checked and solver cross-checked · 4 rows

Truth table (16 rows)

Constructive dilemma: (A → B) AND (C → D), A OR C, therefore B OR D
#	A	B	C	D	p1	p2	conclusion
0	FALSE	FALSE	FALSE	FALSE	TRUE	FALSE	FALSE
1	FALSE	FALSE	FALSE	TRUE	TRUE	FALSE	TRUE
2	FALSE	FALSE	TRUE	FALSE	FALSE	TRUE	FALSE
3	FALSE	FALSE	TRUE	TRUE	TRUE	TRUE	TRUE
4	FALSE	TRUE	FALSE	FALSE	TRUE	FALSE	TRUE
5	FALSE	TRUE	FALSE	TRUE	TRUE	FALSE	TRUE
6	FALSE	TRUE	TRUE	FALSE	FALSE	TRUE	TRUE
7	FALSE	TRUE	TRUE	TRUE	TRUE	TRUE	TRUE
8	TRUE	FALSE	FALSE	FALSE	FALSE	TRUE	FALSE
9	TRUE	FALSE	FALSE	TRUE	FALSE	TRUE	TRUE
10	TRUE	FALSE	TRUE	FALSE	FALSE	TRUE	FALSE
11	TRUE	FALSE	TRUE	TRUE	FALSE	TRUE	TRUE
12	TRUE	TRUE	FALSE	FALSE	TRUE	TRUE	TRUE
13	TRUE	TRUE	FALSE	TRUE	TRUE	TRUE	TRUE
14	TRUE	TRUE	TRUE	FALSE	FALSE	TRUE	TRUE
15	TRUE	TRUE	TRUE	TRUE	TRUE	TRUE	TRUE

Plain-language reading

BeginnerConclusion: at least one of B or D is true (both may be true).
About the operators:
- OR is inclusive: it is true when at least one part is true, including when several are.

IntermediateConclusion: at least one of B or D is true (both may be true).

AdvancedConclusion: at least one of B or D is true (both may be true) [inclusive disjunction ∨].
Formal notation: B ∨ D

Logic diagram

The common slip

Concluding B AND D instead of B OR D. Only one antecedent is guaranteed, so only one consequent follows. On the row A = TRUE, B = TRUE, C = FALSE, D = FALSE both premises are true and B AND D is false, so the stronger conclusion fails while B OR D holds.

Questions

Is there a destructive dilemma too?

Yes: from (A -> B) AND (C -> D) and NOT B OR NOT D, conclude NOT A OR NOT C. It is the contrapositive version of this argument and can be entered into the validity checker the same way, with the same four variables and sixteen rows.

Guides

Rules of inference

Operators and gates

Tools

Worked examples

Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build 2026-11-07. Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.