modus ponens

Modus ponensMathworldPlanetmath is a rule of inferenceMathworldPlanetmath that is commonly found in many logics where the binary logical connective (sometimes written or ) called logical implication are defined. Informally, it states that

from A and AB, we may infer B.

Modus ponens is also called the rule of detachment: the theoremMathworldPlanetmath b can be “detached” from the theorem AB provided that A is also a theorem.

An example of this rule is the following: From the premisses “It is raining”, and “If it rains, then my laundry will be soaked”, we may draw the conclusionMathworldPlanetmath “My laundry will be soaked”.

Two common ways of mathematically denoting modus ponens are the following:

AABB  or{A,AB}B.

One formal way of looking at modus ponens is to define it as a partial functionMathworldPlanetmath :F×FF, where F is a set of formulasMathworldPlanetmathPlanetmath in a languagePlanetmathPlanetmath L where a binary operationMathworldPlanetmath is defined, such that

  1. 1.

    (A,B) is defined whenever A,BF and B(AC) for some CL, and

  2. 2.

    when this is the case, CF and (A,B):=C;

  3. 3.

    is not defined otherwise.

Remark. With modus ponens, one can easily prove the converseMathworldPlanetmath of the deduction theoremMathworldPlanetmath (see this link ( Another easily proven fact is the following:

If ΔA and ΔAB, then ΔB, where Δ is a set of formulas.

To see this, let A1,,An be a deductionMathworldPlanetmathPlanetmath of A from Δ, and B1,,Bm be a deduction of AB from Δ. Then A1,,An,B1,,Bm,B is a deduction of B from Δ, where B is inferred from An (which is A) and Bm (which is AB) by modus ponens.

Title modus ponens
Canonical name ModusPonens
Date of creation 2013-03-22 16:50:48
Last modified on 2013-03-22 16:50:48
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 19
Author CWoo (3771)
Entry type Definition
Classification msc 03B22
Classification msc 03B05
Classification msc 03B35
Synonym rule of detachment
Synonym detachment
Synonym modus ponendo ponens