Definition
An inference rule in a formal system is a rule that specifies how to derive new theorems from existing ones. Each rule names a pattern of premises and a conclusion, and licenses any substitution into that pattern. Common examples: modus ponens (from A and A ⊃ B derive B), universal generalization (from P(x) for arbitrary x derive ∀x: P(x)), substitution.
Why it matters
How it works
An inference rule is given as a schema with placeholders (variables). To apply the rule, find a substitution of strings for placeholders that makes the schema's premises match existing theorems; the conclusion under the same substitution is then a new theorem. Most formal systems have a small number of rules — propositional logic typically has modus ponens plus a few axiom schemes; predicate logic adds rules for quantifiers.