Modus Ponendo Tollens¶

From the incompatibility of A and B together with A, infer not-B: affirming one jointly forbidden proposition eliminates the other.

Version: v3 · 2026-09-06 · History
Domain-specific #: 2297
Origin domain: propositional proof theory
Subdomain: rules of inference
Aliases: MPT, Mode that denies by affirming

Core Idea¶

Modus ponendo tollens is the valid propositional inference that affirms one member of an incompatible pair and thereby denies the other. Its basic nonconjunction form is:

¬(A ∧ B)
A
therefore ¬B.

The first premise does not say that either proposition must be true. It says only that they cannot both be true. Once A is affirmed, B would make the forbidden conjunction true, so B must be false. E. J. Lemmon describes the rule exactly this way: the negation of a conjunction plus one conjunct yields the negation of the other.^[1]

The inference is symmetric. From ¬(A ∧ B) and B one may infer ¬A. What matters is not which letter appears first but the role map: a joint-exclusion premise, an affirmed conjunct, a remaining conjunct, and the negation of that remaining conjunct.

A direct natural-deduction proof exposes the mechanism:

1. ¬(A ∧ B)       premise
2. A              premise
3. assume B
4. A ∧ B          conjunction introduction, 2 and 3
5. contradiction  1 and 4
6. ¬B             negation introduction, discharging 3

This proof uses only conjunction introduction and negation introduction. It does not require replacing the first premise by a disjunction or using classical double-negation elimination. The Open Logic Project’s natural-deduction rules supply those exact proof operations.^[2]

The rule also has an exclusive-disjunction presentation:

A XOR B
A
therefore ¬B.

Exclusive disjunction is a stronger premise than ¬(A ∧ B) because it additionally asserts that at least one disjunct is true. Given the separate premise A, that extra existential information does not strengthen the conclusion. Inclusive A ∨ B is insufficient: A and B may both be true.

Structural Signature¶

the propositions A and B — formulas with determinate truth conditions in the logic being used;
the incompatibility premise — ¬(A ∧ B), or an explicitly stronger premise that entails it;
the affirmed conjunct — A, or symmetrically B;
the hypothetical rejected case — assuming the remaining proposition would produce A ∧ B;
the contradiction bridge — the forbidden conjunction conflicts with its negation;
the discharged assumption — the temporary assumption of B is discharged under negation introduction;
the conclusion — ¬B, the contradictory of the unaffirmed conjunct;
the validity invariant — no valuation makes both premises true and the conclusion false;
the exchange symmetry — swapping A and B preserves the rule form;
the proof-system presentation — MPT may appear as a primitive rule, a derived natural-deduction rule, a truth-table-valid schema, a NAND consequence, or an exclusive-disjunction elimination;
the scope discipline — object-language negation and conjunction must not be confused with uncertainty, low probability, pragmatic opposition, or modal impossibility unless a formal bridge is supplied.

Recognition test. Locate a premise forbidding A and B from holding together, a premise affirming one of them, and a conclusion denying the other. If the first premise merely says A or B inclusively, or if the affirmed statement is the antecedent of an implication rather than one of a forbidden pair, the rule is different.

What It Is Not¶

Not modus ponens. Modus ponens uses A → B and A to infer B. MPT uses incompatibility to infer a negation.
Not modus tollens. Modus tollens uses A → B and ¬B to infer ¬A. MPT affirms one proposition rather than denying a consequent.
Not modus tollendo ponens. That rule uses A ∨ B and ¬A to infer B. It denies one alternative and affirms another; MPT affirms one and denies the incompatible other.
Not disjunctive syllogism under the basic presentation. A classical derivation may rewrite ¬(A ∧ B) as ¬A ∨ ¬B and then use A as ¬¬A, but that is one derivation, not the rule’s locked identity.
Not conjunction elimination. Conjunction elimination infers A from A ∧ B. MPT begins with the negation of the conjunction and one conjunct.
Not denying the antecedent. A → B and ¬A do not entail ¬B.
Not an inference from inclusive disjunction and one disjunct. A ∨ B and A permit B to be either true or false.
Not merely “A and B are different.” Distinct propositions can both be true. The premise must exclude their joint truth.
Not probabilistic suppression. If A makes B unlikely but not impossible, categorical ¬B does not follow.
Not modal reasoning without translation. “A and B cannot both occur” may express logical, physical, legal, or model-relative incompatibility. The context must specify why that claim licenses the formal premise.

Scope of Application¶

In propositional proof theory, MPT can be adopted as a named primitive transformation or derived from more basic natural-deduction rules. A proof checker may implement it as a convenience rule while verifying that the two cited premises match ¬(A ∧ B) and A up to substitution. A derivation remains sound because the rule preserves truth under every Boolean valuation.

The form is historically important. The Stanford Encyclopedia of Philosophy’s account of Stoic logic lists a third indemonstrable that infers the contradictory of one conjunct from the negation of a conjunction and the other conjunct. It separately lists a fourth indemonstrable using an exclusive disjunction plus one disjunct.^[3] Modern terminology can group both under “denying by affirming,” but the premise structures should remain distinguished.

In digital logic, the Sheffer stroke A | B is NAND: ¬(A ∧ B). Therefore A | B together with A entails ¬B. The Open Logic Project confirms the usual NAND reading of the Sheffer stroke and its functional completeness.^[2] The inference concerns logical output states, not electrical timing or uncertainty.

In constraint systems, a pairwise “not both” constraint plus assignment of one Boolean variable propagates falsity to the other. This is the same truth-functional pattern when the variables and constraint have Boolean semantics. In a SAT clause representation, ¬(A ∧ B) is equivalent classically to ¬A ∨ ¬B; setting A true unit-propagates ¬B.

Psychology of reasoning can study whether people make this inference under categorical or uncertain premises. Politzer and Carles use the MPT terminology in work on belief revision and uncertain reasoning.^[4] Their application does not convert a probability judgment into a valid categorical conclusion; it studies how reasoners handle related forms under uncertainty.

Clarity¶

Use four tests:

Normalize the first premise. Does it entail ¬(A ∧ B)? “Exactly one,” NAND, and a declared mutual-exclusion constraint do; inclusive OR alone does not.
Match the affirmed proposition. The second premise must affirm one of the jointly forbidden propositions, not merely something correlated with it.
Negate the other proposition. The conclusion is the contradictory of the remaining proposition, not its contrary, improbability, or absence of evidence.
Check the countervaluation. Try A=true, B=true. The conclusion ¬B would be false, but the incompatibility premise would also be false; hence no valuation falsifies the conclusion while satisfying both premises.

Example: “Ann and Bill cannot both win; Ann won; therefore Bill did not win” qualifies if “cannot both” is categorical and both names refer to the same race and winning condition. It fails if ties are permitted despite the first sentence’s informal wording, if the race differs, or if “Ann is likely to win” replaces the affirmed premise.

Manages Complexity¶

MPT compresses a recurring contradiction subproof into one visible inference. Rather than reopening an assumption, building the forbidden conjunction, deriving contradiction, and discharging the assumption each time, a reasoner can cite the incompatibility and the affirmed member directly.

The rule also exposes hidden premise strength. Everyday elimination often sounds like “A happened, so B did not,” but that conclusion is valid only when the incompatibility premise is present. Naming the rule forces an analyst to locate and defend that premise. Many bad inferences disappear once “not both” is distinguished from “usually not together,” “different,” or inclusive “either.”

In automated constraint propagation, the same schema turns a global-looking pairwise restriction into a local update. Assigning one literal immediately fixes the other. This reduces search without adding information not already entailed by the constraint.

Abstract Reasoning¶

If ¬(A ∧ B) and A are true, then B cannot be true; otherwise A ∧ B and its negation would both hold.
Swapping A and B yields an equally valid inference because conjunction is commutative.
The premise A XOR B entails ¬(A ∧ B), so the exclusive-disjunction form is valid.
The premises A ∨ B and A do not entail ¬B; the valuation A=true, B=true is a counterexample.
If the incompatibility claim is defeasible or probabilistic, the categorical rule no longer applies without strengthening or changing the conclusion.
In intuitionistic natural deduction, the direct subproof from assumed B to contradiction establishes ¬B; classical De Morgan conversion is unnecessary.
If A is inconsistent by itself, then A and the first premise can entail any conclusion in an explosive logic; that degeneracy is not the informative MPT mechanism.
If a system uses a paraconsistent negation, the ordinary contradiction and explosion behavior may differ; the rule must be verified under that logic’s semantics rather than imported by name.
NAND plus A entails ¬B because NAND is definitionally ¬(A ∧ B), not because the Sheffer stroke visually resembles disjunction.
Unit propagation on ¬A ∨ ¬B after assigning A=true is an implementation of the classical MPT consequence.

Knowledge Transfer¶

Exact transfer occurs wherever claims are Boolean and a “not both” constraint is categorical: natural deduction, truth tables, Boolean circuits, SAT solving, rule engines, finite-domain constraints, and formal specifications. Rename A and B, preserve the incompatibility and affirmation roles, and the inference remains valid.

Transfer to ordinary reasoning is licensed only after translating natural-language statements into those roles. Legal exclusivity, resource locking, mutually exclusive classifications, and contest outcomes can supply ¬(A ∧ B), but the domain must justify exclusivity. If exceptions, ties, overlapping categories, or uncertain observations remain, the formal rule may not apply.

The cross-domain skeleton is deductive elimination under incompatibility. That structure is already captured by Deductive Reasoning and Mutual Exclusion at the prime layer. MPT remains a domain-specific named rule because its exact identity depends on propositional formulas, connectives, truth-preserving entailment, and proof rules.

Examples¶

Race outcome. Ann and Bill cannot both win the specified race. Ann won. Therefore Bill did not win. Roles: incompatibility, A, and ¬B are explicit.

Boolean constraint. A scheduling model contains ¬(Morning ∧ Evening) for one mutually exclusive assignment. Morning is set true. Propagation sets Evening false. The inference is exact only if the assignments are genuinely exclusive.

NAND gate. Output A | B is true and input A is true. With the stroke interpreted as NAND, B must be false. If the symbol instead names an uninterpreted operation, no inference follows.

Exclusive choice. Exactly one of red or blue is selected; red is selected; therefore blue is not selected. The XOR premise contains the required not-both relation plus an unused at-least-one condition.

Non-example: inclusive choice. At least one of red or blue is selected; red is selected; therefore blue is not selected. Invalid: both may be selected.

Non-example: empirical tendency. Two symptoms rarely co-occur; symptom A is observed; therefore symptom B is absent. “Rarely” supplies probability, not logical incompatibility.

Structural Tensions¶

Primitive rule versus derived rule. A calculus may name MPT directly or derive it from conjunction and negation rules. Diagnose the inferential relation, not the presentation.
Nonconjunction versus exclusive disjunction. Both license the conclusion with A, but XOR adds at-least-one information. Do not call them logically equivalent premises.
Formal incompatibility versus worldly impossibility. Logic preserves a supplied premise; it does not prove that a race, category, or resource rule is actually exclusive.
Categorical validity versus uncertain reasoning. Small probability is not negation. Change either the premise or the conclusion when uncertainty enters.
Direct constructive proof versus classical rewrite. De Morgan plus disjunctive syllogism is convenient classically; the assumption-to-contradiction proof reveals that the base inference does not need classical double-negation elimination.
Mnemonic Latin versus structural transparency. The name is historically useful but easily confused with three other modi. The premise–conclusion schema should always accompany it.
Useful shortcut versus composite derivability. Derivability does not erase operational identity, but acceptance depends on the rule recurring as a named, checkable proof transformation rather than merely being one theorem among infinitely many.

Structural–Framed Character¶

Structural; aggregate 0.10. Once the connectives and consequence relation are fixed, validity is independent of institutional preference or interpretation. Every Boolean valuation confirms the same entailment. The Latin name and proof notation are conventional wrappers around a formal relation.

The abstraction remains domain-specific rather than prime. Its literal roles are propositions, conjunction, negation, derivation, and truth preservation. The substrate-neutral residue—deductive elimination of an incompatible alternative—is already represented by existing primes.

Structural Core vs. Domain Accent¶

The structural core is two states are jointly forbidden; one is established; eliminate the other. Mutual Exclusion supplies the not-both relation, Contradiction explains the rejected joint case, and Deductive Reasoning supplies truth-preserving consequence.

The domain accent fixes Boolean propositions, ¬ and ∧, a formal consequence relation, temporary assumptions, contradiction, and negation introduction. Those are constitutive. Without them the pattern may guide practical reasoning, but it is no longer literally the propositional inference rule called modus ponendo tollens.

Deductive Reasoning is the minimal prospective parent. MPT is a strict truth-preserving inference from premises to a conclusion. Most deductive arguments do not have its incompatibility-plus-affirmation form.

Mutual Exclusion supplies the content of ¬(A ∧ B), while Contradiction supplies the proof step that rejects assumed B. Neither is the result type of the abstraction: MPT is an inference rule, not a resource-control mechanism or an inconsistent commitment set. Proof by Contradiction is a related proof strategy, but the MPT subderivation discharges only the temporary assumption of B.

Relationships to Other Abstractions¶

Current abstraction Modus Ponendo Tollens Domain-specific

Parents (1) — more general patterns this builds on

Modus Ponendo Tollens is a kind of Deductive Reasoning Prime

Deductive Reasoning is the minimal prospective parent.

Hierarchy path (1) — routes to 1 parentless root

Modus Ponendo Tollens → Deductive Reasoning

Neighborhood in Abstraction Space¶

Modus Ponendo Tollens sits in a sparse region of the domain-specific corpus (85^th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Unclustered & Miscellaneous (1565 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-09-08

Not to Be Confused With¶

prime:deductive_reasoning is the correct parent, not exact coverage. It includes countless valid forms without selecting MPT’s four roles.

prime:mutual_exclusion generalizes the at-most-one constraint across systems, but does not itself name the inference from one occupied alternative to the negation of another. prime:contradiction describes joint inconsistency, not the full transformation rule.

Modus ponens affirms a consequent through implication. Modus tollens denies an antecedent through implication. Modus tollendo ponens denies one disjunct and affirms another. Disjunctive syllogism uses inclusive disjunction and a negated disjunct. Conjunction elimination extracts a conjunct from a positive conjunction. The Sheffer stroke is a connective; MPT is one consequence involving it.

References¶

[1] E. J. Lemmon. Beginning Logic. Thomas Nelson, 1965; later Routledge editions, p. 61. States modus ponendo tollens as inference from a negated conjunction and one conjunct to the negation of the other. registry ↩

[2] Open Logic Project. Open Logic Project: Complete Build, release 9620cc7 (2026-07-12), Chapter 10 and the section on Boolean operators. Documents conjunction introduction, negation introduction, and the NAND reading of the Sheffer stroke. registry ↩a ↩b

[3] Susanne Bobzien. “Ancient Logic.” Stanford Encyclopedia of Philosophy. Section 5.4 distinguishes the Stoic third indemonstrable using negated conjunction from the fourth using exclusive disjunction. registry ↩

[4] Guy Politzer and Laure Carles. “Belief Revision and Uncertain Reasoning.” Thinking & Reasoning 7 (2001): 217–234. A modern reasoning-study context using the MPT terminology. registry ↩

[5] Jon R. Stone. Latin for the Illiterati. Routledge, 1996, p. 60. Supports the conventional Latin gloss. registry