modus ponens

Modus ponens is a rule of inference that is commonly found in many logics where the binary logical connective $\to$ (sometimes written $\Rightarrow$ or $\supset$) called logical implication are defined. Informally, it states that

from $A$ and $A\to B$, we may infer $B$.

Modus ponens is also called the rule of detachment: the theorem $b$ can be “detached” from the theorem $A\to 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:

$$\frac{A\mathit{\hspace{1em}}A\to B}{B}\mathit{\hspace{1em}\hspace{1em}}\text{or}\mathit{\hspace{1em}}\{A,A\to B\}⊢B.$$

One formal way of looking at modus ponens is to define it as a partial function $⊢:F\times F\to F,$ where $F$ is a set of formulas in a language $L$ where a binary operation $\to$ is defined, such that

1. $⊢(A,B)$ is defined whenever $A,B\in F$ and $B\equiv (A\to C)$ for some $C\in L$, and

2. when this is the case, $C\in F$ and $⊢(A,B):=C$;

3. $⊢$ is not defined otherwise.

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 $\mathrm{\Delta }⊢A$ and $\mathrm{\Delta }⊢A\to B$, then $\mathrm{\Delta }⊢B$, where $\mathrm{\Delta }$ is a set of formulas.

To see this, let $A_1,\mathrm{\dots },A_n$ be a deduction of $A$ from $\mathrm{\Delta }$, and $B_1,\mathrm{\dots },B_m$ be a deduction of $A\to B$ from $\mathrm{\Delta }$. Then $A_1,\mathrm{\dots },A_n,B_1,\mathrm{\dots },B_m,B$ is a deduction of $B$ from $\mathrm{\Delta }$, where $B$ is inferred from $A_n$ (which is $A$) and $B_m$ (which is $A\to B$) 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