Modus Ponens

Modus ponens is an inference rule in logic that permits the conclusion $Q$ from the premises “If $P$, then $Q$” and $P$. It is a basic form of deductive reasoning, used in propositional logic and more expressive logical systems. Also called affirming the antecedent or implication elimination, it specifies how an established conditional can be applied when its antecedent has been established. Its defining feature is truth preservation: true premises cannot produce a false conclusion under the standard interpretation of implication. (en.wikipedia.org)

Form and interpretation

The rule is conventionally represented as

Here $P$ is the antecedent and $Q$ the consequent of the conditional $P\rightarrow Q$. The horizontal line separates premises from conclusion; it is not itself a connective within the logical language. The letters can represent complex formulas, not merely atomic statements. An application requires the separately established premise to match the antecedent of the conditional. (plato.stanford.edu)

For example:

1. If an integer is divisible by four, it is divisible by two.
2. Twelve is divisible by four.
3. Therefore, twelve is divisible by two.

The reasoning depends on the argument’s form rather than on its particular mathematical subject matter. The same pattern applies to $P\rightarrow(Q\land R)$: once $P$ is established, modus ponens yields the entire consequent $Q\land R$, rather than just one of its components. (plato.stanford.edu)

Semantic validity

In classical logic, the conditional is commonly interpreted as material implication. It is false only when its antecedent is true and its consequent false. A truth table therefore verifies modus ponens:

The only row in which both premises are true also makes the conclusion true. This establishes logical validity: there is no interpretation making the premises true and the conclusion false. Validity does not establish that the premises of a particular argument actually are true; that is a separate question. (plato.stanford.edu)

The corresponding formula

is a tautology in classical logic. Nevertheless, a formula and an inference rule have different roles. The formula is an expression evaluated within a logical language; the rule licenses a transition between expressions in a derivation. (iep.utm.edu)

Role in proof systems

In natural deduction, modus ponens is the elimination rule for implication, often written $\rightarrow E$. Its counterpart, implication introduction, establishes $P\rightarrow Q$ by deriving $Q$ under a temporary assumption $P$, then discharging that assumption. Elimination instead uses an available conditional together with its antecedent. These complementary rules describe how implications are proved and used. (plato.stanford.edu)

In a Hilbert-style proof system, modus ponens can serve as the sole inference rule for propositional logic when accompanied by suitable axiom schemata. A formal proof then consists of a sequence of formulas, each an axiom instance or the result of applying modus ponens to earlier formulas. The rule alone, without axioms or premises, does not supply a complete logical calculus. This organization is important in proof theory, including demonstrations that a calculus preserves truth. (iep.utm.edu)

Modus ponens also operates in first-order logic, alongside rules for quantifiers. It is retained in intuitionistic logic: applying an implication does not require the distinctively classical principle of double-negation elimination. (plato.stanford.edu)

Related and invalid patterns

Modus tollens has a different form: from $P\rightarrow Q$ and $\neg Q$, infer $\neg P$. Both patterns are valid in classical logic, but they use different information about the conditional. (iep.utm.edu)

Two superficially similar patterns are instances of fallacy:

• Affirming the consequent: from $P\rightarrow Q$ and $Q$, infer $P$.
• Denying the antecedent: from $P\rightarrow Q$ and $\neg P$, infer $\neg Q$.

Both fail when $P$ is false and $Q$ true. A conditional establishes a sufficient condition for its consequent, not necessarily a necessary one. Thus, knowing that an integer is divisible by two does not establish that it is divisible by four. (iep.utm.edu)

Historical development

An ancient counterpart appears in the logic of Stoicism, developed especially by Chrysippus in the third century BCE. The Stoics recognized a basic “indemonstrable” argument that concludes a conditional’s consequent from the conditional and its antecedent. Their propositional approach differed from the term-based syllogistic associated with Aristotle. Historical continuity concerns the inference pattern; ancient accounts of conditionals should not simply be identified with modern material implication. (plato.stanford.edu)

Computational interpretation

Under the Curry–Howard correspondence, implication is interpreted as a function type. A proof of $P\rightarrow Q$ acts as a function taking a proof of $P$ to a proof of $Q$; modus ponens corresponds to function application. This interpretation connects logical inference with type theory and machine-checked proof. In the Lean proof assistant, for example, if h : P → Q and hp : P, the expression h hp is a proof of Q. The dependency on both premises is represented directly in the proof term. (docs.lean-lang.org)