ModusPonens 2007-03-18 13:52:06 2008-06-23 12:21:25 Definition inference rule \usepackage{amssymb,amscd} \usepackage{amsmath} \usepackage{amsfonts} % used for TeXing text within eps files %\usepackage{psfrag} % need this for including graphics (\includegraphics) %\usepackage{graphicx} % for neatly defining theorems and propositions \usepackage{amsthm} % making logically defined graphics \usepackage{xypic} \usepackage{pst-plot} \usepackage{psfrag} % define commands here \newtheorem{prop}{Proposition} \newtheorem{thm}{Theorem} \newtheorem{ex}{Example} \newcommand{\real}{\mathbb{R}} \textbf{Modus ponens} is a rule of inference that is commonly found in many logics where the binary logical connective $\rightarrow$ or the binary logical relation $\Rightarrow$ called logical implication are defined. Informally, it states that \begin{center} If $a$ and $a \Rightarrow b$ are theorems, then $b$ is a theorem. \end{center} Modus ponens is also called the \emph{rule of detachment}: the theorem $b$ can be ``detached'' from the theorem $a \Rightarrow 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,\ a \Rightarrow b}{b} \qquad \mbox{or} \quad a, (a \Rightarrow b) \vdash b.$$ One formal way of looking at modus ponens is to define it as a partial function $\vdash : F \times F \to F,$ where $F$ is a set of formulas in a language $L$ where a binary operation $\Rightarrow$ is defined, such that \begin{enumerate} \item $\vdash(x, y)$ is defined whenever $x, y \in F$ and $y \equiv (x \Rightarrow z)$ for some $z \in L$, and \item when this is the case, $z \in F$ and $\vdash(x, y) := z$; \item $\vdash$ is not defined otherwise. \end{enumerate}