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.