Lesson 9: Counterexamples (intermediate, 12 min)

One concrete assignment can refute an equivalence or an argument. This intermediate lesson, about twelve minutes, finds counterexamples, replays them, keeps them as regression tests, and explains what it means when there is none.

Level: intermediate12 min6 claims in this lesson were confirmed by the exact checker at build time

One concrete assignment can refute an equivalence or an argument. Find counterexamples, replay them, and keep them as regression tests.

The first step compares the intended entry rule with a colleague's version, member OR (invited AND NOT banned), and settles the question with one assignment, a banned member, on which the two differ. The second step is about trust: every counterexample the engine shows is replayed by an independent evaluator before you see it, it is a complete assignment anyone can reproduce, and the right thing to do with it is to turn it into a test. The third step applies the idea to arguments, where a counterexample makes every premise TRUE and the conclusion FALSE, with discount -> member, member, therefore discount as the invalid example. The fourth step says what no counterexample means: the claim holds on every assignment the assumptions allow, which is a proof within that scope and not beyond it.

The lesson's three equivalence and validity claims are verified at build time. The exercises ask for the assignment that exposes the alternative rule, a prediction of its output, the classification of (A -> B) -> (B -> A), and the verdict on a sprinkler argument.

The testing section builds on this lesson directly: the page on counterexamples as tests shows the row from the first step becoming a regression test, and the independence-pair pages generalise “one row that matters” to “one pair per input”.

Do this lesson interactively in the app

Steps

1. One assignment settles it

The intended entry rule is (member OR invited) AND NOT banned. A colleague wrote member OR (invited AND NOT banned). Are they the same?

No. With member=TRUE, invited=FALSE, banned=TRUE, the intended rule denies entry but the alternative allows it: the ban was not applied to the membership path. One counterexample is enough to refute the equivalence.

intended := (member OR invited) AND NOT banned · outputalternative := member OR (invited AND NOT banned) · output

member: the person is a member; invited: the person has an invitation; banned: the person is banned;

One assignment settles it
#	member	invited	banned	intended	alternative
0	FALSE	FALSE	FALSE	FALSE	FALSE
1	FALSE	FALSE	TRUE	FALSE	FALSE
2	FALSE	TRUE	FALSE	TRUE	TRUE
3	FALSE	TRUE	TRUE	FALSE	FALSE
4	TRUE	FALSE	FALSE	TRUE	TRUE
5	TRUE	FALSE	TRUE	FALSE	TRUE
6	TRUE	TRUE	FALSE	TRUE	TRUE
7	TRUE	TRUE	TRUE	FALSE	TRUE

Compare intended with alternative, then replay the counterexample on the diagram.

not-equivalent intended / alternative · holds

2. Replay it, then keep it

Every counterexample Tangibool shows is replayed by an independent evaluator before you see it. It is a complete assignment, so anyone can reproduce it.

Turn it into a regression test: keep the inputs and write the expected result from the requirement (here FALSE: banned people never enter), not from whichever formula you currently have.

alternative := member OR (invited AND NOT banned) · output

member: the person is a member; invited: the person has an invitation; banned: the person is banned;

Replay it, then keep it
#	member	invited	banned	alternative
0	FALSE	FALSE	FALSE	FALSE
1	FALSE	FALSE	TRUE	FALSE
2	FALSE	TRUE	FALSE	TRUE
3	FALSE	TRUE	TRUE	FALSE
4	TRUE	FALSE	FALSE	TRUE
5	TRUE	FALSE	TRUE	TRUE
6	TRUE	TRUE	FALSE	TRUE
7	TRUE	TRUE	TRUE	TRUE

Save the counterexample as a test of alternative with the expected value FALSE and watch it fail.

3. Counterexamples to arguments

For an argument, a counterexample makes every premise TRUE and the conclusion FALSE.

Premises discount -> member and member; conclusion discount. The counterexample discount=FALSE, member=TRUE shows a member without a discount: the premises allow it, so the conclusion does not follow.

p1 — discount -> member · premisep2 — member · premiseconclusion — discount · conclusion

member: the person is a member; discount: the person gets a discount;

Counterexamples to arguments
#	discount	member	p1	p2	conclusion
0	FALSE	FALSE	TRUE	FALSE	FALSE
1	FALSE	TRUE	TRUE	TRUE	FALSE
2	TRUE	FALSE	FALSE	FALSE	TRUE
3	TRUE	TRUE	TRUE	TRUE	TRUE

Check validity, then add the premise member -> discount and check again.

invalid · holds

4. No counterexample: proven, within scope

When the exact checker finds no counterexample, the claim holds for every assignment allowed by the stated assumptions. That is a proof, which no number of passing examples can give.

Here premium OR member and member agree only because of the assumption premium -> member (every premium customer is a member). Disable the assumption and a counterexample appears. If the assumptions are inconsistent, results hold only vacuously, and Tangibool says so.

either := premium OR member · outputjust_member := member · output

premium: the customer has a premium plan; member: the person is a member;

No counterexample: proven, within scope
#	premium	member	either	just_member	k1	Scope
0	FALSE	FALSE	FALSE	FALSE	TRUE	in scope
1	FALSE	TRUE	TRUE	TRUE	TRUE	in scope
2	TRUE	FALSE	TRUE	FALSE	FALSE	excluded
3	TRUE	TRUE	TRUE	TRUE	TRUE	in scope

Compare either with just_member, then disable the assumption and compare again.

equivalent either / just_member · holds

Exercises

Find an assignment where the alternative lets in someone whom the intended rule keeps out. (find-assignment)
For alternative := member OR (invited AND NOT banned), predict the output for a banned member without an invitation: member=TRUE, invited=FALSE, banned=TRUE. (predict-output)
Is (A -> B) -> (B -> A) always TRUE? Classify it. (classify)
Premises: sprinkler -> wet_lawn and wet_lawn. Conclusion: sprinkler. Valid or not? If not, give a counterexample. (argument-validity)

Do this lesson interactively in the app

Questions

Can a counterexample be wrong?

The engine replays every witness through an independent evaluator before showing it, and labels the result if the replay fails. What it cannot judge is whether the assignment is realistic, which is where assumptions come in.

What if two formulas are equivalent?

Then there is no counterexample, and the checker says so after examining every row in scope. That is a proof of equivalence within the stated assumptions, the fourth step's point.

Tools

Argument validity checker: premises, conclusion, counterexample or proof

Lessons

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.