2 Deduction and inference

Inference rules forms the basic steps of proving theorems and corollaries.

• $p \rightarrow q, p \vert q$
• $p \rightarrow q, \neg q \vert \neg p$
• $p \rightarrow q, q \rightarrow r \vert p \rightarrow r$
• $p \vee q, \neg p \vert q$
• $p \rightarrow q, r \rightarrow s, p \vee r \vert q \vee s$
• $p \rightarrow q, r \rightarrow s, \neg q \vee \neg s \vert \neg p \vee \neg s$
• $p, q \vert p$
• $p \wedge q \vert p, q$
• $p \vert p \vee q$
• $\forall x: P(x) \vert \exists x:P(x)$

With quantifiers, we also have some two-way transformation rules:

• $(\neg(\forall x: P(x))) \equiv (\exists x: \neg P(x))$
• $(\neg(\exists x: P(x))) \equiv (\forall x: \neg P(x))$