Rules of Inference

Standard rules:

• Implication introduction

• Implication elimination

• Conjunction introduction

• Conjunction elimination

• Disjunction introduction

• Disjunction elimination

• Universal generalization

• Universal instantiation

• Existential generalization

• Existential instantiation

Classical (more)

• Exportation

• Negation introduction

• Negation elimination

• Disjunctive syllogism

List

• Assumption

• Conjunction

  • and-introduction

  • and-elimination (conjunction elimination, simplification)

• Disjunction

  • disjunction introduction

  • disjunction elimination

• Implication

  • implication introduction, conditional proof

  • implication elimination (modus ponens)

• Biconditional

  • biconditional introduction

  • biconditional elimination

• Negation

  • negation introduction

  • negation elimination

• Double negation

  • double negation introduction

  • double negation elimination

Pile of terms

• Transformation rules

• Rules of inference

• Propositional calculus

  • Implication introduction / elimination (modus ponens)

  • Biconditional introduction / elimination

  • Conjunction introduction / elimination

  • Disjunction introduction / elimination

  • Disjunctive / hypothetical syllogism

  • Constructive / destructive dilemma

  • Absorption / modus tollens / modus ponendo tollens

  • Rules of replacement

  • Associativity

  • Commutativity

  • Distributivity

  • Double negation

  • De Morgan's laws

  • Transposition

  • Material implication

  • Exportation

  • Tautology

  • Negation introduction

• Predicate logic

  • Universal generalization / instantiation

  • Existential generalization / instantiation