Lesson 14: Why this result: reasons and strictness (advanced, 20 min)

A verdict says whether a rule holds; this lesson reads the result backwards. Which facts does every passing case share, which sets of facts guarantee the result, which facts of one case really decide it, what are the fewest changes that flip it, and when is one rule at least as strict as another? Four steps, advanced level, about twenty minutes.

Level: advanced20 min7 claims in this lesson were confirmed by the exact checker at build time

Read a result backwards: which facts every passing case shares, which sets of facts guarantee it, which facts of one case really decide it, what the fewest changes are, and when one rule is at least as strict as another.

For the entry rule (member OR invited) AND NOT banned, every admissible case that allows entry has banned = FALSE: a necessary condition, shown by an exact query that finds no case with entry and banned = TRUE. Neither member nor invited is necessary on its own, because an invited stranger enters. The second step lists the two ways to qualify, member AND NOT banned and invited AND NOT banned: each guarantees entry, no fact can be dropped from either, and together they cover every entering case, so the list is complete. For one case, an invited member who is not banned, member = TRUE, banned = FALSE is an irreducible reason and invited = TRUE, banned = FALSE is another; irreducible means that no fact can be removed, never the smallest or the only reason.

The third step asks for the smallest change: a refused stranger is one change from entry, membership or an invitation, and the engine tries distance 1, then 2, and claims “no change of at most d inputs” only when every smaller distance was shown impossible. You choose which inputs may change, and with banned fixed no change lets a banned member in. The fourth step compares rules: a prospectus rule that needs two agencies at investment grade is at least as strict as an internal rule satisfied with one, because every case the first allows the second allows too, and the internal rule is looser, with S&P alone as the witness. A strictness map orders up to twelve rules from strictest to loosest and shows one case each way for an incomparable pair.

The exercises ask for a case the internal rule allows and the prospectus rule refuses, whether “a way to qualify guarantees the result” is always true, and what a banned member’s smallest change is when banned must stay as it is. The glossary pages on prime implicants and witnesses explain the terms behind ways to qualify, and the testing section’s eligibility pattern shows the same questions on a five-condition rule.

Do this lesson interactively in the app

Steps

1. Necessary conditions: what every passing case shares

For allow_entry := (member OR invited) AND NOT banned, every admissible case that allows entry has banned = FALSE. The engine shows this with an exact query: a case with entry and banned = TRUE does not exist.

Neither member = TRUE nor invited = TRUE is necessary on its own: an invited stranger enters without being a member. Necessary conditions are facts, not advice: they say what the formulas read.

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

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

Necessary conditions: what every passing case shares

#	member	invited	banned	allow_entry
0	FFALSE	FFALSE	FFALSE	FFALSE
1	FFALSE	FFALSE	TTRUE	FFALSE
2	FFALSE	TTRUE	FFALSE	TTRUE
3	FFALSE	TTRUE	TTRUE	FFALSE
4	TTRUE	FFALSE	FFALSE	TTRUE
5	TTRUE	FFALSE	TTRUE	FFALSE
6	TTRUE	TTRUE	FFALSE	TTRUE
7	TTRUE	TTRUE	TTRUE	FFALSE

Open the Why view for allow_entry and read its necessary conditions.

2. Ways to qualify and irreducible reasons

There are exactly two ways to be allowed in: member AND NOT banned, and invited AND NOT banned. Each guarantees entry, no fact can be dropped from either, and together they cover every case that enters: the list is complete.

For one case, a member who is invited and not banned, an irreducible reason is member = TRUE, banned = FALSE: these two facts alone still guarantee entry. invited = TRUE, banned = FALSE is another reason inside the same case. Irreducible means no fact can be removed; it never means “the smallest” or “the only” reason.

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

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

Ways to qualify and irreducible reasons

#	member	invited	banned	allow_entry
0	FFALSE	FFALSE	FFALSE	FFALSE
1	FFALSE	FFALSE	TTRUE	FFALSE
2	FFALSE	TTRUE	FFALSE	TTRUE
3	FFALSE	TTRUE	TTRUE	FFALSE
4	TTRUE	FFALSE	FFALSE	TTRUE
5	TTRUE	FFALSE	TTRUE	FFALSE
6	TTRUE	TTRUE	FFALSE	TTRUE
7	TTRUE	TTRUE	TTRUE	FFALSE

Set member, invited TRUE and banned FALSE, then ask for the reason and its alternatives.

3. Smallest changes

A stranger who is refused (member, invited, and banned all FALSE) is one change away from entry: become a member, or get an invitation. The engine tries distance 1, then 2, and so on, and says “no change of at most d inputs” only when every smaller distance was shown impossible.

You choose which inputs may change. With banned marked fixed, no change gives a banned member entry: the result is honest about what the model allows, and it is a fact about the model, not an instruction.

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

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

Smallest changes

#	member	invited	banned	allow_entry
0	FFALSE	FFALSE	FFALSE	FFALSE
1	FFALSE	FFALSE	TTRUE	FFALSE
2	FFALSE	TTRUE	FFALSE	TTRUE
3	FFALSE	TTRUE	TTRUE	FFALSE
4	TTRUE	FFALSE	FFALSE	TTRUE
5	TTRUE	FFALSE	TTRUE	FFALSE
6	TTRUE	TTRUE	FFALSE	TTRUE
7	TTRUE	TTRUE	TTRUE	FFALSE

Set every input FALSE, ask for the smallest change to TRUE, then mark banned fixed and try a banned member.

4. Strictness: every case one rule allows, the other allows

prospectus_rule requires two agencies at investment grade; internal_rule is satisfied with one. The prospectus rule is at least as strict: every case it allows, the internal rule allows too (K AND prospectus_rule AND NOT internal_rule is unsatisfiable). The internal rule is looser, shown by a case such as only S&P at investment grade.

A strictness map draws up to twelve rules from strictest to loosest: all_three → prospectus_rule → internal_rule and all_three → sp_only → internal_rule. prospectus_rule and sp_only are incomparable: one case each way.

prospectus_rule := AT_LEAST(2; sp_investment_grade, moodys_investment_grade, fitch_investment_grade) · outputinternal_rule := AT_LEAST(1; sp_investment_grade, moodys_investment_grade, fitch_investment_grade) · outputall_three := AT_LEAST(3; sp_investment_grade, moodys_investment_grade, fitch_investment_grade) · outputsp_only := sp_investment_grade · output

sp_investment_grade: S&P rates the bond BBB- or better; moodys_investment_grade: Moody’s rates the bond Baa3 or better; fitch_investment_grade: Fitch rates the bond BBB- or better; prospectus_rule: the prospectus accepts the bond (two agencies agree); internal_rule: the internal rule accepts the bond (any agency); all_three: all three agencies agree; sp_only: only S&P’s rating counts;

Strictness: every case one rule allows, the other allows

#	sp_investment_grade	moodys_investment_grade	fitch_investment_grade	prospectus_rule	internal_rule	all_three	sp_only
0	FFALSE	FFALSE	FFALSE	FFALSE	FFALSE	FFALSE	FFALSE
1	FFALSE	FFALSE	TTRUE	FFALSE	TTRUE	FFALSE	FFALSE
2	FFALSE	TTRUE	FFALSE	FFALSE	TTRUE	FFALSE	FFALSE
3	FFALSE	TTRUE	TTRUE	TTRUE	TTRUE	FFALSE	FFALSE
4	TTRUE	FFALSE	FFALSE	FFALSE	TTRUE	FFALSE	TTRUE
5	TTRUE	FFALSE	TTRUE	TTRUE	TTRUE	FFALSE	TTRUE
6	TTRUE	TTRUE	FFALSE	TTRUE	TTRUE	FFALSE	TTRUE
7	TTRUE	TTRUE	TTRUE	TTRUE	TTRUE	TTRUE	TTRUE

Open the Strictness view, compare prospectus_rule with internal_rule, then draw the map of all four rules.

not-equivalent prospectus_rule / internal_rule · holds

Exercises

1. Find a case the internal rule allows and the prospectus rule refuses (it shows that the internal rule is looser). (find-assignment)
2. Classify member_way := member AND NOT banned -> allow_entry: is “a way to qualify guarantees the result” always true, never true, or contingent? (classify)
3. A banned member (member TRUE, invited FALSE, banned TRUE) asks what the smallest change to entry is when banned must stay as it is. Is allow_entry TRUE for this case as given? (predict-output)

Do this lesson interactively in the app

Questions

What is the difference between a necessary condition and a way to qualify?

A necessary condition is a fact every passing case has, such as banned = FALSE; on its own it does not guarantee entry. A way to qualify is a set of facts that does guarantee it, with nothing removable, such as member AND NOT banned: a prime implicant under the assumptions, in textbook terms.

When is a strictness result “Not determined”?

When the exact queries behind it run out of budget. A pair that is not determined leaves the map partial, and the map says so; it never fills the gap with a guess.

Related

Tools

• Truth table generator: any Boolean expression, up to 12 variables, with intermediate columns

See also

• Lesson 5: If, only if, unless: necessary and sufficient conditions (intermediate, 15 min)
• Lesson 9: Counterexamples (intermediate, 12 min)
• Prime implicant: meaning and examples
• Witness (satisfying assignment): meaning and examples
• Assumption (domain constraint): meaning and examples
• Eligibility rules: the pattern, the usual exceptions and the tests
• Lesson 13: Categories, scales, and counting (intermediate, 20 min)
• Entry rule: (member OR invited) AND NOT banned, checked every way

Lessons

• Lesson 2: XOR: exclusive OR and parity (beginner, 10 min)
• Lesson 3: Grouping and precedence (beginner, 12 min)
• Lesson 4: Truth tables (beginner, 12 min)
• Lesson 5: If, only if, unless: necessary and sufficient conditions (intermediate, 15 min)

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.