Rules of Inference, 1.5

Modus Ponens	$\begin{displaymath} \begin{array}{l} p \rightarrow q \newline p \end{array}\over... ...hbox{.}\kern-0.1em\lower0.2ex\hbox{.}\thinspace \hspace{1em} q \end{displaymath}$
Modus Tollens	$\begin{displaymath} \begin{array}{l} \neg q \newline p \rightarrow q \end{array}... ....}\kern-0.1em\lower0.2ex\hbox{.}\thinspace \hspace{1em} \neg p \end{displaymath}$
Hypothetical Syllogism	$\begin{displaymath} \begin{array}{l} p \rightarrow q \newline q \rightarrow r \e... ....1em\lower0.2ex\hbox{.}\thinspace \hspace{1em} p \rightarrow r \end{displaymath}$
Disjunctive Syllogism	$\begin{displaymath} \begin{array}{l} p \vee q \newline \neg p \end{array}\over \... ...hbox{.}\kern-0.1em\lower0.2ex\hbox{.}\thinspace \hspace{1em} q \end{displaymath}$
Addition	$\begin{displaymath} \begin{array}{l} p~~~ \end{array}\over \hspace{-1.5em}\leave... ...\kern-0.1em\lower0.2ex\hbox{.}\thinspace \hspace{1em} p \vee q \end{displaymath}$
Simplification	$\begin{displaymath} \begin{array}{l} p \wedge q \end{array}\over \hspace{-3.5em}... ...hbox{.}\kern-0.1em\lower0.2ex\hbox{.}\thinspace \hspace{1em} p \end{displaymath}$
Conjunction	$\begin{displaymath} \begin{array}{l} p~~~ \newline q \end{array}\over \hspace{-1... ...ern-0.1em\lower0.2ex\hbox{.}\thinspace \hspace{1em} p \wedge q \end{displaymath}$
Resolution	$\begin{displaymath} \begin{array}{l} p \vee q \newline \neg p \vee r \end{array}... ...\kern-0.1em\lower0.2ex\hbox{.}\thinspace \hspace{1em} q \vee r \end{displaymath}$

Universal instantiation	$\begin{displaymath} \begin{array}{l} \forall x \: P(x) \end{array}\over \hspace{... ....}\kern-0.1em\lower0.2ex\hbox{.}\thinspace \hspace{0.5em} P(c) \end{displaymath}$
Universal generalization	$\begin{displaymath} \begin{array}{l} P(c)~{\rm for~all}~c \end{array}\over \hspa... ...\lower0.2ex\hbox{.}\thinspace \hspace{0.5em} \forall x \: P(x) \end{displaymath}$
Existential instantiation	$\begin{displaymath} \begin{array}{l} \hspace{-2.5em}\exists x \: P(x) \end{array... ...er0.2ex\hbox{.}\thinspace \hspace{0.5em} P(c)~{\rm for~some}~c \end{displaymath}$
Existential generalization	$\begin{displaymath} \begin{array}{l} P(c)~{\rm for~some}~c \end{array}\over \hsp... ...\lower0.2ex\hbox{.}\thinspace \hspace{0.5em} \exists x \: P(x) \end{displaymath}$

Universal modus ponens

$\begin{displaymath} \begin{array}{l} \forall x \: P(x) \rightarrow Q(x) \newline... ....}\kern-0.1em\lower0.2ex\hbox{.}\thinspace \hspace{0.5em} Q(a) \end{displaymath}$

Universal modus tollens

$\begin{displaymath} \begin{array}{l} \forall x \: P(x) \rightarrow Q(x) \newline... ...rn-0.1em\lower0.2ex\hbox{.}\thinspace \hspace{0.5em} \neg P(a) \end{displaymath}$

Rules of Inference, 1.5

Exercises