What is the difference between an elimination rule vs an inference rule? They seem like they are the same thing.

  • 1
    In Natural Deduction inference rules are classified as -introduction vs -elimination according to the fact that they eliminate or introduce a connective in the conclusion. Commented May 30, 2020 at 7:15

1 Answer 1


An elimination rule is one specific kind of inference rule, usually contrasted with Introduction rules. An elimination rule is one in which there is a logical connective in the antecedent that does not appear in the consequent - the connective is "eliminated" from the consequence by following the rule.

A common example is the rule of Modus Ponens, which can be understood as an elimination rule for the "implies" connective. If we have a premise of "A implies B", and a premise of "A", then applying the Modus ponens rule allows us to "eliminate" the implication connective and derive a conclusion "B".

There is also an "Implication introduction" rule, which is not an elimination rule but is an inference rule. This is the rule that allows us to say that if we can derive a statement "B" from a statement "A", then we can conclude that "A implies B" is true (and can discharge A if we assumed it), thus introducing "implies" into our conclusion.

Elimination and introduction rules often work together to describe the functioning of logical connectives in an inference system, and the distinction can be quite strategically useful if we want to start to work out how to prove a given statement from a given set of premises.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .