> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/300-logic/logic-inference/lo-inference-rules3.md).

# Rules of inference

* [Conjunction](/math-debrief/300-logic/logic-inference/lo-inference-rules3.md#conjunction)
* [Disjunction](/math-debrief/300-logic/logic-inference/lo-inference-rules3.md#disjunction)
* [implication](/math-debrief/300-logic/logic-inference/lo-inference-rules3.md#implication)
* [Modus ponens](/math-debrief/300-logic/logic-inference/lo-inference-rules3.md#modus-ponens)
* [Negation](/math-debrief/300-logic/logic-inference/lo-inference-rules3.md#negation)
* [double negation](/math-debrief/300-logic/logic-inference/lo-inference-rules3.md#double-negation)
* [De Morgan's laws](/math-debrief/300-logic/logic-inference/lo-inference-rules3.md#de-morgans-laws)
* [Rules of propositional calculus](/math-debrief/300-logic/logic-inference/lo-inference-rules3.md#rules-of-propositional-calculus)

## Conjunction

* and-introduction
* $$\land\_{i}$$
* adjunction
* conjunction introduction
* and-elimination

two rules, one for each assumption: $$\wedge{e\_1}$$ and $$\wedge{e\_2}$$

## Disjunction

Disjunction introduction

* ∨I
*

$$p\vdash p\lor q$$ and $$q\vdash p\lor q$$

Disjunction elimination, ∨EL and ∨ER

$$p\lor q,p\to r,q\to r \vdash r$$

## implication

* implication introduction: $$\rightarrow{i}$$
* implication elimination: $$\rightarrow{e}$$    

  (*modus ponens*,  implies-elimination, arrow-elimination)
* *modus tollens*: $$MT$$

  $$\phi \rightarrow \psi, \neg \psi \vdash \neg \phi$$
* implication introduction
* implication elimination (modus ponens, implies-elimination, conditional elimination) 
* conditional proof (conditional introduction) 
* modus tollens

## Modus ponens

Modus ponens (modus ponendo ponens i.e. "mode that affirms by affirming", or implication elimination, or $$\rightarrow$$ elimination) is a rule of inference in propositional logic that can be summarized as: "if p then q; there is a p, therefore there is a q".

$$
p\to{q}\\
\underline{p\quad\quad}\\
\therefore{q\quad}
$$

As a sequent: $$p\to{q}, ; p;; \vdash;; q$$ where $$\vdash$$ is a metalogical symbol meaning that q is a syntactic consequence of $$p\to{q}$$ and $$p$$ in some logical system.

As the statement of a truth-functional tautology or theorem of propositional logic: $$((p \to q) \land p) \to q$$, where $$p$$, and $$q$$ are propositions expressed in some formal system.

## Negation

Negation introduction (Reductio ad absurdum)

$$
{\phi \vdash \psi }\\
{\underline {\phi \vdash \lnot \psi}}\\
{\lnot \phi}
$$

$$p\to q, p\to\neg q \vdash\neg p$$

## double negation

* double negation introduction: $$\neg\neg{i}$$
* double negation elimination: $$\neg\neg{e}$$

## De Morgan's laws

The negation of conjunction rule may be written in sequent notation:

$$\neg (P\land Q) \vdash (\neg P \lor \neg Q)$$

The negation of disjunction rule may be written as:

$$\neg (P\lor Q)\vdash (\neg P\land \neg Q)$$

De Morgan's duality can be generalised to quantifiers, the universal quantifier and existential quantifier are duals:

$$\forall x P(x) \equiv \neg (\exists x,\neg P(x))$$

$$\exists x P(x)\equiv \neg (\forall x,\neg P(x))$$

## Rules of propositional calculus

<https://en.wikipedia.org/wiki/Propositional_calculus>

**Negation introduction** $$p\to q, p\to\neg q \vdash\neg p$$

**Negation elimination** $$\neg p \vdash p\to r$$

**Double negative elimination** $$\neg \neg p\vdash p$$

**Conjunction introduction** $$p,q \vdash p\land q$$

**Conjunction elimination** $$p\land q \vdash p$$ and $$p\land q \vdash q$$

**Disjunction introduction** $$p\vdash p\lor q$$ and $$q\vdash p\lor q$$

**Disjunction elimination** $$p\lor q,p\to r,q\to r \vdash r$$

**Biconditional introduction** From $$p\to q$$ and $$q\to p$$ infer $$p\leftrightarrow q$$ $$p\to q, q\to p \vdash p\leftrightarrow q$$

**Biconditional elimination** $$p\leftrightarrow q \vdash (p\to q)$$ and $$(p\leftrightarrow q)\vdash (q\to p)$$

**Modus ponens** (conditional elimination) From p and (p\to q), infer q. $$p, p\to q \vdash q$$

**Conditional proof** (conditional introduction) From, assumption that $$p$$ allows a proof of $$q$$, infer $$p\to q$$ $$(p\vdash q)\vdash (p\to q)$$