Rule of Inference

A rule of inference is a schematic instruction specifying how a conclusion may be derived from premises in a formal system. In logic, such rules provide the steps of deductive reasoning: they determine how proofs may proceed, rather than merely listing statements accepted as true. A formal proof consists of applications of these rules, beginning with assumptions or axioms and ending with the proposition to be established. Rules can govern formulas, judgments, or derivability statements. (cs.cmu.edu)

Form and interpretation

A rule is conventionally displayed with its premises above a horizontal line and its conclusion below:

The letters normally stand for arbitrary expressions of the appropriate kind. Consequently, the display describes a family of permissible steps, not just one argument. Applying a rule requires matching its premises and conclusion consistently to particular expressions and satisfying any additional restrictions. Proofs can be written as trees of such applications or as numbered lines referring to earlier steps. (leanprover.github.io)

For example, modus ponens has the form

Given “the switch is closed” and “if the switch is closed, the lamp is lit,” it permits “the lamp is lit.” The rule concerns the argument’s form; it does not establish whether either premise accurately describes a particular lamp. Here the connective $\to$ expresses material implication, while the inference bar authorizes a transition between statements. (leanprover-community.github.io)

An axiom supplies a starting statement, whereas an inference rule ordinarily specifies a transition. In a generalized presentation, however, an axiom is itself treated as a rule with zero premises. An axiom schema specifies a family of such starting statements. (cs.cmu.edu)

Propositional rules and discharged assumptions

In propositional logic, rules operate on formulas built with connectives such as conjunction, disjunction, implication, and negation. Natural deduction organizes many of them into introduction rules, which establish a connective, and elimination rules, which explain how a statement containing that connective may be used. For conjunction, these include

Disjunction introduction permits $A\lor B$ from $A$, but disjunction elimination requires reasoning by cases: the same conclusion must follow both from assuming $A$ and from assuming $B$. Merely knowing $A\lor B$ does not identify which alternative holds. (leanprover.github.io)

Some rules act on entire subderivations. Implication introduction allows a temporary assumption $A$ to be discharged after deriving $B$:

Here $\Gamma$ represents the remaining assumptions, and $\vdash$ denotes formal derivability. Discharging an assumption means that the resulting conditional no longer depends on that assumption as an independently accepted premise. This bookkeeping distinguishes a conditional proof from an unsupported assertion of its consequent. (leanprover-community.github.io)

In classical logic, double-negation elimination permits $A$ from $\neg\neg A$. Classical proof by contradiction similarly permits $A$ after deriving a contradiction under the assumption $\neg A$. These unrestricted principles are not generally accepted in intuitionistic logic. Over the usual intuitionistic rules, they are interderivable with the law of excluded middle, $A\lor\neg A$. (leanprover.github.io)

Quantifiers and side conditions

First-order logic adds rules for quantifiers. Universal elimination allows an instance of a universally quantified formula:

The term $t$ must be substitutable without unintended variable capture. Universal introduction requires that the variable being generalized not occur free in any undischarged assumption: the derivation must concern an arbitrary object, not one constrained by a special premise. (leanprover-community.github.io)

Existential introduction derives $\exists x\,P(x)$ from a suitable instance $P(t)$. Existential elimination permits reasoning with a fresh representative satisfying $P$, but the final conclusion must not depend on that representative’s identity. Freshness and assumption restrictions are essential parts of the rule, not optional conventions. (leanprover-community.github.io)

Soundness and completeness

Rules belong to the syntactic description of a proof system; their justification can also be studied through semantics. For ordinary truth-preserving deduction, a rule is sound when its application cannot produce a false conclusion from true premises under the relevant interpretations. In classical propositional logic, truth tables can test this condition. Logical validity therefore concerns interpretations, whereas derivability concerns available formal rules. (leanprover.github.io)

A system has soundness when

and completeness when the converse holds. The symbol $\models$ expresses semantic consequence. Standard classical propositional calculi satisfy both properties; corresponding first-order results are expressed by Gödel’s completeness theorem. Completeness concerns the collective power of a calculus, not the adequacy of one rule in isolation. (leanprover.github.io)

Derived rules and mechanized proofs

Proof theory distinguishes primitive rules from derived rules, whose applications abbreviate combinations of already available steps. An admissible rule preserves derivability whenever its premises are derivable, although admissibility need not amount to a fixed derivation from hypothetical premises. These distinctions depend on the particular calculus. (cs.cmu.edu)

In proof assistants, inference patterns can be represented by operations on proof objects. Under the Curry–Howard correspondence, propositions are represented as types and proofs as terms: implication elimination corresponds to applying a function to an argument. Lean, for example, represents conjunction introduction by constructing a proof from proofs of both components, and conjunction elimination by extracting either component. Named theorems can then serve as reusable inference patterns without becoming new primitive logical rules. (leanprover.github.io)