| Version 5 |
Version 4 |
| \emph{Modus ponens} is a rule of inference that is commonly found in many logics where the binary logical connective $\to$ called implication is defined. Informally, it states that |
\emph{Modus ponens} is a rule of inference that is commonly found in many logics where the binary logical connective $\to$ called implication is defined. Informally, it states that |
| \begin{quote} |
\begin{quote} |
| \begin{center} |
|
| \end{center} |
|
| \end{quote} |
\end{quote} |
| Modus ponens is also called the \emph{rule of detachment}: the formula $b$ can be ``detached'' from the formula $a\to b$ provided that $a$ is also a formula. |
Modus ponens is also called the \emph{rule of detachment}: the formula $b$ can be ``detached'' from the formula $a\to b$ provided that $a$ is also a formula. |
|
|
| An example of this rule is the following: From the premises ``It is raining.'' |
An example of this rule is the following: From the premises ``It is raining.'' |
| and ``If it rains, then my laundry will se soaked.'', we may draw the conclusion |
and ``If it rains, then my laundry will se soaked.'', we may draw the conclusion |
| ``My laundry will be soaked.''. |
``My laundry will be soaked.''. |
|
|
| Two common ways of mathematically denoting modus ponens are the following: |
Two common ways of mathematically denoting modus ponens are the following: |
| $$\frac{a,a\to b}{b}\qquad\mbox{ or }\qquad (a\mbox{ and }a\to b)\Rightarrow b.$$ |
$$\frac{a,a\to b}{b}\qquad\mbox{ or }\qquad (a\mbox{ and }a\to b)\Rightarrow b.$$ |
|
|
| One formal way of looking at modus ponens is to define it as a partial function $\Rightarrow: 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 |
One formal way of looking at modus ponens is to define it as a partial function $\Rightarrow: 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 |
| \begin{enumerate} |
\begin{enumerate} |
| \item |
\item |
| $\Rightarrow(x,y)$ is defined whenever $x,y\in F$ and $y=x\to z$ for some $z\in L$, and |
$\Rightarrow(x,y)$ is defined whenever $x,y\in F$ and $y=x\to z$ for some $z\in L$, and |
| \item |
\item |
| when this is the case, $z\in F$ and $\Rightarrow(x,y):=z$; |
when this is the case, $z\in F$ and $\Rightarrow(x,y):=z$; |
| \item |
\item |
| $\Rightarrow$ is not defined otherwise. |
$\Rightarrow$ is not defined otherwise. |
| \end{enumerate} |
\end{enumerate} |
