modus ponens (original) (raw)
from A and A→B, we may infer B.
Modus ponens is also called the rule of detachment: the theorem b can be “detached” from the theorem A→B 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 conclusion“My laundry will be soaked”.
Two common ways of mathematically denoting modus ponens are the following:
Remark. With modus ponens, one can easily prove the converse of the deduction theorem
(see this link (http://planetmath.org/DeductionTheorem)). Another easily proven fact is the following:
If Δ⊢A and Δ⊢A→B, then Δ⊢B, where Δ is a set of formulas.
To see this, let A1,…,An be a deduction of A from Δ, and B1,…,Bm be a deduction of A→B 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 A→B) by modus ponens.