elimination-rule

Definition

An introduction-rule is an inference-rule that allows to derive a formula-statement of some syntactic form from some define premises.

List of well-known introduction-rules

• biconditional-elimination-1

• biconditional-elimination-2

• conjunction-elimination-1

• conjunction-elimination-2

• double-negation-elimination

Quotes

“Each of the introduction rules tells us how to derive a formula of some syntactic form. For instance, the conjunction introduction rule (∧I) shows that we can derive a conjunction if we derive both conjunctive terms; the disjunction introduction rules (∨I) show that we can derive a disjunction if we derive one of the disjunctive terms.” [PLVH08, p. 6-7]