Rules of inference

Conjunction

  • and-introduction

  • i\land_{i}

  • adjunction

  • conjunction introduction

  • and-elimination

two rules, one for each assumption: e1\wedge{e_1} and e2\wedge{e_2}

Disjunction

Disjunction introduction

  • ∨I

ppqp\vdash p\lor q and qpqq\vdash p\lor q

Disjunction elimination, ∨EL and ∨ER

pq,pr,qrrp\lor q,p\to r,q\to r \vdash r

implication

  • implication introduction: i\rightarrow{i}

  • implication elimination: e\rightarrow{e}

    (modus ponens, implies-elimination, arrow-elimination)

  • modus tollens: MTMT

    ϕψ,¬ψ¬ϕ\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".

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

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

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

Negation

Negation introduction (Reductio ad absurdum)

ϕψϕ¬ψ¬ϕ{\phi \vdash \psi }\\ {\underline {\phi \vdash \lnot \psi}}\\ {\lnot \phi}

pq,p¬q¬pp\to q, p\to\neg q \vdash\neg p

double negation

  • double negation introduction: ¬¬i\neg\neg{i}

  • double negation elimination: ¬¬e\neg\neg{e}

De Morgan's laws

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

¬(PQ)(¬P¬Q)\neg (P\land Q) \vdash (\neg P \lor \neg Q)

The negation of disjunction rule may be written as:

¬(PQ)(¬P¬Q)\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:

xP(x)¬(x¬P(x))\forall x P(x) \equiv \neg (\exists x\,\neg P(x))

xP(x)¬(x¬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 pq,p¬q¬pp\to q, p\to\neg q \vdash\neg p

Negation elimination ¬ppr\neg p \vdash p\to r

Double negative elimination ¬¬pp\neg \neg p\vdash p

Conjunction introduction p,qpqp,q \vdash p\land q

Conjunction elimination pqpp\land q \vdash p and pqqp\land q \vdash q

Disjunction introduction ppqp\vdash p\lor q and qpqq\vdash p\lor q

Disjunction elimination pq,pr,qrrp\lor q,p\to r,q\to r \vdash r

Biconditional introduction From pqp\to q and qpq\to p infer pqp\leftrightarrow q pq,qppqp\to q, q\to p \vdash p\leftrightarrow q

Biconditional elimination pq(pq)p\leftrightarrow q \vdash (p\to q) and (pq)(qp)(p\leftrightarrow q)\vdash (q\to p)

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

Conditional proof (conditional introduction) From, assumption that pp allows a proof of qq, infer pqp\to q (pq)(pq)(p\vdash q)\vdash (p\to q)

Last updated

Was this helpful?