1 Introduction rules in formal logic
1.1 Basic idea and purpose
In formal proof systems, an introduction rule licenses the formation of a compound statement by relying on proofs of its immediate parts. The guiding intuition is constructive: to assert a structured claim such as a conjunction, implication, disjunction, negation, or quantified formula, the proof system demands evidence corresponding to the internal structure of that claim.
As a result, introduction rules are central in natural-deduction and related styles because they mirror how mathematicians reason when building complex statements from simpler arguments. In many frameworks, an introduction rule explicitly specifies what subproofs or assumptions must be available and how they may be arranged to yield the target formula.
1.2 Introduction rules vs. elimination rules
Most connectives are governed by two complementary kinds of rules. Introduction rules explain how to create a formula with a particular outer connective, while elimination rules explain how to extract or use information from such a formula.
For example, to obtain a conjunction one typically introduces it from separate demonstrations of each conjunct; conversely, to use a conjunction one typically eliminates it to obtain either component. This division organizes proof construction: introduction rules are typically used “at the top” of a reasoning step that produces a new formula, whereas elimination rules are used when a previously established compound formula is exploited.
1.3 Soundness and proof-theoretic meaning
A proof system is sound (with respect to its semantics) when any formula derivable by its rules is genuinely valid or true under the intended interpretation. Introduction rules contribute to this property because they must preserve truth in the framework’s interpretation.
Beyond semantic correctness, introduction rules also carry proof-theoretic meaning. In proof theory, the shape of an introduction rule often reflects the nature of the information being constructed—e.g., an implication introduction corresponds to transforming an assumed derivation into a conditional claim. Under interpretations such as the Curry–Howard correspondence, introduction rules can be viewed as operators that build evidence objects; elimination rules then correspond to operations that consume or transform that evidence.
2 Natural deduction style introduction rules
2.1 Conjunction introduction (∧-introduction)
Conjunction introduction typically states that if one has a proof of \(A\) and a proof of \(B\), then one may infer \(A \wedge B\). In natural deduction, these proofs may occur independently, possibly within larger contexts. The resulting conjunction packages both pieces of evidence into a single composite statement.
This rule reflects the intuitive requirement that establishing “and” means simultaneously establishing each conjunct. The proof structure often records both derivations as subcomponents feeding into the conjunction.
2.2 Disjunction introduction (∨-introduction)
Disjunction introduction allows one to infer \(A \vee B\) from evidence for either side. There are usually two schematic variants: from a proof of \(A\), infer \(A \vee B\); and from a proof of \(B\), infer \(A \vee B\).
Unlike conjunction, disjunction does not demand simultaneous support for both disjuncts. Instead, the rule captures that a proof of a disjunction can be obtained by choosing the relevant alternative and embedding the corresponding proof into the disjunction.
2.3 Implication introduction (→-introduction)
Implication introduction is typically expressed using a subproof with an additional assumption. A standard formulation is: if assuming \(A\) leads to a derivation of \(B\), then one may discharge the assumption and conclude \(A \to B\).
This design encodes the idea that an implication is justified by a method that converts any proof of \(A\) into a proof of \(B\). The subproof structure records the dependency on the temporary assumption, and discharge formalizes the shift from conditional reasoning to a standalone conditional statement.
2.4 Negation introduction (¬-introduction)
Negation introduction often uses a derivation that produces an inconsistency from an assumed negation. One common pattern is: if assuming \(A\) yields a contradiction (or bottom, depending on the system), then infer \( \neg A \). Some systems use a direct rule that assumes \(A\) and derives falsity; others define negation via implication to contradiction.
The rule’s purpose is to turn “\(A\) cannot hold because it leads to impossibility” into a formal statement of non-derivability or incompatibility, with discharge ensuring that the contradiction is tied to the temporary assumption.
2.5 Universal quantifier introduction (∀-introduction)
Universal quantifier introduction asserts a statement for all objects, provided the proof of an instance meets certain constraints. A typical natural-deduction version: if one can derive \(P(x)\) for an arbitrary \(x\), then one may infer \( \forall x\, P(x) \).
The critical issue is that the proof must not rely on \(x\) being a special, fixed entity. Systems therefore impose side conditions about freshness or eigenvariables (often requiring that the chosen \(x\) be new with respect to the surrounding context). This ensures that the inference captures genuine generality rather than a claim about a particular example.
2.6 Existential quantifier introduction (∃-introduction)
Existential quantifier introduction typically allows one to infer \( \exists x\, P(x) \) when a witness is provided. If the system has a term or variable \(t\) and a proof of \(P(t)\), then it may conclude \( \exists x\, P(x) \).
The rule formalizes the idea that an existential claim is supported by constructing or indicating a specific candidate satisfying the property. In proof representations, the witness may appear explicitly as a term used to build the existential statement.
3 Sequent calculus introduction rules
3.1 Connection to left/right rules
Sequent calculus represents judgments as sequents, usually of the form “from assumptions \(\Gamma\) derive conclusions \(\Delta\).” Introduction rules are then separated according to whether they act on formulas appearing on the left (assumptions) or on the right (conclusions) of the sequent.
For a connective \(C\), introduction rules typically exist in two-sided forms:
- Right introduction produces a compound conclusion in \(\Delta\) from derivations where its components appear appropriately.
- Left introduction uses the compound assumption in \(\Gamma\) to allow reasoning about how it could be decomposed.
This left/right split aligns with proof search: applying right rules tends to build up goals, while left rules tend to break down assumptions.
3.2 Structural context and rules of weakening/strengthening
Sequent calculi handle the management of context via structural rules such as weakening (adding unused assumptions) and strengthening (removing redundant ones), along with exchange and contraction depending on whether the calculus treats contexts as multisets or sequences.
Introduction rules interact with these structural features because they often presume the presence of certain formulas in the relevant context while remaining insensitive to irrelevant context changes. Some systems are formulated to be resource-sensitive (e.g., linear logic), where weakening and contraction may be restricted; in such settings, the “right” introduction rules account for how evidence is consumed.
3.3 Example sequent derivations
A small illustration often used to convey the style is showing how to derive a sequent involving conjunction or implication. For instance, to show that \(A \wedge B\) can be concluded on the right, one typically applies the conjunction-right introduction rule, requiring separate derivations of \(A\) and \(B\) from the same or related contexts.
Similarly, implication on the right is handled by a rule that shifts \(A\) into the antecedent (left side) and then derives \(B\) in that enriched context. Although the exact notation varies among calculi, the hallmark is that the rule’s premises display precisely where the connective components must be proved.
4 Subproofs, discharged assumptions, and side conditions
4.1 Discharging assumptions in implication and negation
Natural deduction frequently uses temporary assumptions within subproofs. When a subproof establishes a target from an assumption, introduction rules then “discharge” that assumption, turning a dependency into a compound statement.
In implication introduction, discharge converts “under assumption \(A\), derive \(B\)” into \(A \to B\). In negation introduction, discharge converts “assuming \(A\) leads to contradiction” into \(\neg A\) (or a negation-like form). The discharge mechanism is not merely bookkeeping: it determines which assumptions count as premises of the resulting formula.
4.2 Eigenvariables in quantifier introduction
Quantifier introduction must prevent accidental generality. For universal quantification, a proof of \(P(x)\) for a variable \(x\) must treat \(x\) as arbitrary. This is commonly enforced by selecting an eigenvariable: a variable introduced specifically for the rule application and guaranteed not to appear in a way that ties the derivation to a particular individual.
Eigenvariables support a soundness intuition: since the proof does not depend on special properties of the chosen variable, the conclusion is valid for every instance. For existential quantification, by contrast, one typically supplies a witness term rather than introducing an eigenvariable with arbitrary interpretation.
4.3 Common side conditions and freshness constraints
Side conditions regulate variables and contexts to ensure that introduction rules are applied correctly. Typical requirements include:
- Freshness constraints ensuring that certain variables are new relative to undischarged assumptions.
- Restrictions on where and how a variable may be substituted in later stages.
- Conditions ensuring that discharged assumptions do not incorrectly influence subsequent rules.
These constraints are essential in systems where naive quantifier rules would otherwise allow unsound inferences, especially when proof steps reuse variables across scopes. Proper formulation ensures that the calculus remains reliable for both proof checking and proof search.
5 Rule schemata and notation
5.1 Generic templates with metavariables
Introduction rules are frequently presented as schemata rather than as single fixed rules. A schema contains metavariables—placeholders ranging over formulas, terms, variables, or derivations. For example, an introduction rule for implication is not about a specific pair of formulas only; it applies to any formulas \(A\) and \(B\) fitting the schema.
This generic presentation allows a logic’s rules to scale uniformly across the entire language of formulas. When a proof is written, the metavariables are instantiated to the actual formulas and terms used at that point.
5.2 Reading derivation trees
In proof systems with derivation trees, each inference step corresponds to placing a conclusion at the top of a node and premises as its subnodes. Introduction rules typically combine one or more subderivations under a connective-forming step.
Reading such trees often requires attention to scope: discharged assumptions correspond to segments of the tree that feed into an introduction rule, and quantifier eigenvariables are tied to the subtree where they are introduced. Thus, the tree structure encodes not only logical structure but also the bookkeeping needed for correctness.
5.3 Substitution and instantiation in proof systems
Substitution is the operation of replacing variables with terms (or, for some systems, replacing metavariables with actual formulas) while maintaining capture-avoidance and respecting scopes. Instantiation is related but is often discussed in terms of applying quantifier-elimination or quantifier-introduction in a controlled manner.
Introduction rules interact with substitution because a proof of \(P(x)\) for a variable \(x\) might need to be transformed to match the variable conventions of a larger proof. Good calculi specify exactly which variables may be substituted and which side conditions must be preserved, preventing incorrect movement of information across scopes.
6 Examples and small derivations
6.1 Building a conjunction from two proofs
A typical derivation pattern uses conjunction introduction as a final step. Suppose one has already derived \(A\) and derived \(B\) in the same context. Applying \(\wedge\)-introduction yields \(A \wedge B\).
In a derivation tree, the last rule node has two immediate children: one subtree ending in \(A\) and another ending in \(B\). The resulting conjunction is thus directly supported by both branches.
6.2 Proving an implication via a subproof
To introduce \(A \to B\), the proof system expects a subproof that begins by adding \(A\) to the available assumptions and ends with a derivation of \(B\). After this subproof is complete, the implication introduction rule discharges the assumption \(A\).
The overall structure resembles a “local reasoning” phase: one temporarily assumes \(A\), performs deductions to reach \(B\), and then abstracts away from that assumption to obtain the global conditional statement.
6.3 Introducing a universal statement safely
For \(\forall x\, P(x)\), a safe derivation proves \(P(x)\) for an arbitrary but fixed eigenvariable \(x\). The proof must not rely on any special property of \(x\) or on information that would make \(x\) effectively non-arbitrary within the proof’s surrounding scope.
If the side condition is satisfied, the universal introduction rule allows promotion from the instance \(P(x)\) to the universal claim. This step is often emphasized because it is the point where generality is earned, not assumed.
6.4 Introducing an existential with a witness
To obtain \(\exists x\, P(x)\), one provides a witness term \(t\) along with a derivation of \(P(t)\). The existential introduction rule then wraps that instance into the existential quantifier.
This reflects the semantics of existence in proof-theoretic terms: rather than claiming only that “some” object exists, the proof provides a concrete object (or expression) serving as the witness.
7 Relation to semantics and correctness
7.1 Proof-theoretic vs. model-theoretic viewpoint
Proof-theoretic perspectives interpret introduction rules as operators that build structured proofs according to the syntax of connectives and quantifiers. Model-theoretic perspectives instead interpret formulas in structures and judge correctness by truth conditions.
The relationship between these viewpoints is mediated by soundness and completeness theorems. Soundness ensures that introduction-based proof construction does not create formulas that fail in the semantic interpretation. Completeness ensures that semantically valid statements can be recovered by the proof rules, including the introduction rules and their accompanying elimination rules.
7.2 Compatibility with truth-preserving interpretations
Introduction rules are designed so that, under standard truth-preserving interpretations, the premises entail the conclusion. For conjunction, the interpretation of “and” requires both components; for implication, it requires that assuming the antecedent leads to satisfaction of the consequent; for universal quantification, it requires satisfaction for all instances; and for existential quantification, it requires satisfaction for at least one witness.
Side conditions in quantifier rules are also connected to semantic correctness, preventing a proof of an instance from being misconstrued as proof of an arbitrary general statement.
7.3 Normalization and transformation intuition
Many proof-theoretic results show that proofs can be transformed into “normal” forms without changing what they establish. Introduction rules play a role in these transformations because they often correspond to canonical ways of building complex statements. When combined with elimination rules, the interaction may support reductions: for instance, an implication introduced from a derivation and then immediately eliminated can sometimes be transformed into a simpler direct derivation.
This intuition—sometimes described via normalization or proof reduction—shows that introduction rules are not just safe, but also align with a coherent computational or inferential behavior of proofs, where detours introduced by introduction/elimination pairings can be collapsed.