Rules of Inferences

• Modus ponens (MP) (implication elimination)

  • $P\to Q,P⊢Q$

• Syllogism

  • Disjunctive Syllogism (modus tollendo ponens (MTP))
    • $P\vee Q,\neg P⊢Q$
  • Hypothetical Syllogism (transitivity, chain argument, chain rule)
    • $(P\to Q)\wedge (Q\to R)⊢P\to R$

• Eliminations

  • Biconditional Elimination
    • $(P\leftrightarrow Q)⊢(P\to Q)$
    • $(P\leftrightarrow Q)⊢(Q\to P)$
  • Conjunction Elimination (simplification)
    • $(P\wedge Q)⊢P$
    • $(P\wedge Q)⊢Q$
  • Disjunction Elimination (proof by cases, case analysis, or elimination)
    • $(P\to Q),(R\to Q),(P\vee R)⊢Q$

• Introductions

  • Biconditional introduction
    • $(P\to Q),(Q\to P)⊢(P\leftrightarrow Q)$
  • Disjunction introduction (addition, or introduction)
    • $P⊢(P\vee Q)$
  • Conjunction introduction (conjunction, and introduction, adjunction)
    • $P,Q⊢P\wedge Q$

• Dilemma

  • Constructive dilemma
    • $(P\to Q),(R\to S),(P\vee R)⊢(Q\vee S)$
  • Destructive dilemma
    • $(P\to Q),(R\to S),(\neg Q\vee \neg S)⊢(\neg P\vee \neg R)$

• Modus Tollens (MT)

  • $P\to Q,\neg Q\therefore \neg P$

• Absorption

  • $P\to Q⊢P\to (P\wedge Q)$

• Tautology

  • $P\vee P⊢P$
  • $P\wedge P⊢P$