Conjunction Introduction¶

The proof rule that combines derivations of A and B available in a common context into a derivation of their conjunction A ∧ B.

Version: v2 · 2026-09-06 · History
Domain-specific #: 1541
Origin domain: logic
Subdomain: natural deduction
Aliases: And-introduction, Conjunction introduction rule, Conjunction introduction, ∧-introduction, ∧I

Core Idea¶

Conjunction Introduction is the rule of inference that combines proofs of two formulas into a proof of their conjunction. In its familiar natural-deduction display,

\[ \frac{A \qquad B}{A\land B}\;\land I \]

the two items above the line are established formulas available to the derivation, and the item below is the newly licensed conclusion. In a context-indexed presentation, the rule is commonly written

\[ \frac{\Gamma\vdash A \qquad \Gamma\vdash B}{\Gamma\vdash A\land B}\;\land I. \]

The shared \(\Gamma\) says that both derivations are available under compatible undischarged assumptions. A Fitch-style proof expresses the same constraint by requiring the cited lines to be accessible at the line where \(A\land B\) is introduced. The compressed sequent \(A,B\vdash A\land B\) is a valid instance, not the most general rule schema.^[1]^[2]^[3]

The rule is truth-preserving: every valuation that makes both \(A\) and \(B\) true makes \(A\land B\) true. But its identity is proof-theoretic rather than merely truth-tabular. It specifies how a proof of a compound formula is constructed from proofs of its immediate components. Paired with Conjunction Elimination, it contributes to the inferential meaning of \(\land\): to establish a conjunction one must establish both conjuncts; from an established conjunction, either conjunct may be recovered.^[4]^[5]

This exact construction recurs in natural deduction, sequent systems, typed lambda calculi, and proof assistants. Under the propositions-as-types interpretation, a proof of \(A\land B\) is a pair \(\langle a,b\rangle\) containing a proof of \(A\) and a proof of \(B\). Lean's And.intro hA hB is a direct machine-checked realization.^[6]^[7]

Structural Signature¶

A valid instance preserves these roles and constraints:

First target formula \(A\). Any well-formed formula of the object logic; it need not be atomic.
Second target formula \(B\). Another well-formed formula, independent of whether it is topically related to \(A\).
A derivation of \(A\). The proof system has already licensed \(A\) in the relevant context.
A derivation of \(B\). The system has likewise licensed \(B\) in a compatible context.
Context accessibility. Both derivations may be cited at the point of application. A result trapped inside a closed subproof cannot be imported without another rule.
The conjunction-forming operation. The conclusion has principal connective \(\land\), with the cited formulas as its ordered immediate subformulas.
No assumption discharge. Ordinary \(\land I\) combines available results; unlike implication introduction, it does not close a temporary assumption.
System-relative structural policy. In ordinary classical and intuitionistic natural deduction, assumptions may be shared or weakened into a common context. Resource-sensitive logics may distinguish shared-context conjunction from context-splitting multiplicative conjunction.

Recognition test. Locate two accessible derivations, verify that their end formulas exactly match the intended left and right conjuncts, and check that the conclusion is their syntactic conjunction. If a purported application creates an unproved conjunct, changes a formula, cites an inaccessible line, or silently discharges assumptions, it is not Conjunction Introduction.

The order of citation determines the order of the result. From proofs of \(A\) and \(B\), one may derive either \(A\land B\) or \(B\land A\) by citing them in the corresponding order. This does not make the two formulas syntactically identical; their interderivability is proved using elimination and introduction.

What It Is Not¶

It is not the conjunction connective itself. \(A\land B\) is a formula constructor with semantic and proof-theoretic behavior. Conjunction Introduction is one rule governing how a proof of that formula may be formed.

It is not Conjunction Elimination. Elimination moves from \(A\land B\) to \(A\) or to \(B\). Introduction moves in the opposite proof-building direction and requires both components.

It is not Disjunction Introduction, sometimes called addition. From \(A\), disjunction introduction may infer \(A\lor B\) without a proof of \(B\), because one true disjunct suffices. From \(A\) alone, conjunction introduction cannot infer \(A\land B\).

It is not a claim that two unrelated English sentences can safely be joined with and under every pragmatic circumstance. Formal validity abstracts away temporal order, discourse coherence, presupposition, and conversational implicature.

It is not the conjunction fallacy. The probability of \(A\land B\) cannot exceed the probability of either conjunct; Conjunction Introduction concerns categorical derivability once both conjuncts are established, not judging an uncertain conjunction more probable.

It is not generic Deductive Reasoning. Deduction includes many rule forms, including modus ponens, elimination rules, reductio, and quantifier rules. \(\land I\) is the exact two-proof constructor for conjunction.

It is not a categorical adjunction, despite “adjunction” being an older name for this inference rule in some logic textbooks. A category-theoretic adjunction relates functors by hom-set correspondences or units and counits.

Scope of Application¶

The rule's canonical home is Gentzen-style natural deduction for classical and intuitionistic propositional or predicate logic. It applies to formulas of any complexity: if \(\Gamma\vdash (P\to Q)\) and \(\Gamma\vdash \forall x,R(x)\), then \(\Gamma\vdash (P\to Q)\land\forall x,R(x)\). Nothing requires the conjuncts to be atomic or to share vocabulary.^[1]^[4]

In Fitch systems, the user cites two accessible line numbers and writes their conjunction on a new line. The lines need not be adjacent or appear in the same order as originally derived, but both must be in scope. In tree-style natural deduction, entire derivations stand above the inference bar. In a sequent calculus, the corresponding right-introduction rule for conjunction typically derives \(\Gamma\Rightarrow A\land B\) from derivations of \(\Gamma\Rightarrow A\) and \(\Gamma\Rightarrow B\), subject to the calculus's context conventions.

In constructive type theory and proof assistants, conjunction is represented by a product-like or inductive type with a constructor requiring evidence for both components. Lean defines proofs of A ∧ B through the And constructor; And.intro hA hB, or tuple notation ⟨hA, hB⟩, packages the two proof objects.^[7] Similar constructor tactics in other assistants reduce a conjunctive goal to two subgoals.

Automated theorem provers and proof search procedures use the rule both forward and backward. Forward use combines known facts. Backward use sees a goal \(A\land B\) and decomposes proof search into the subgoals \(A\) and \(B\). The backward operation is goal decomposition justified by the introduction rule, not conjunction elimination on an existing premise.

The ordinary form must be qualified outside structural logic. In intuitionistic linear logic, additive and multiplicative conjunction-like connectives have different context disciplines: one may require both subproofs in the same resources, while another splits resources. A resource-sensitive rule is not licensed merely by copying the classical shared-context schema.

Clarity¶

Three distinctions make applications auditable.

First, truth is not availability. A formula may be semantically true in the intended interpretation yet unavailable as a proof line. The rule needs derivations, assumptions, axioms, or previously licensed formulas—not the user's confidence that the conjuncts are true.

Second, line occurrence is not scope accessibility. Suppose \(B\) was derived only inside a temporary assumption box that has since closed. An outer line containing \(A\) and that inaccessible inner \(B\) do not license outer \(A\land B\). Context labels or Fitch indentation prevent this leakage.

Third, the conclusion is syntactically ordered. From \(A\) and \(B\), citing \(A\) first constructs \(A\land B\). Commutativity is an admissible theorem, not a textual identity: derive \(B\land A\) by eliminating both conjuncts and reintroducing them in reverse order.

The name “introduction” refers to the principal connective of the conclusion. \(A\) and \(B\) may already contain conjunctions, but the application introduces the outermost \(\land\) joining them. This lets proof readers identify the rule from formula shape.

Manages Complexity¶

Conjunction Introduction modularizes proof construction. Instead of deriving a large compound claim in one step, a reasoner proves each conjunct through whatever method fits it and packages the results only when both are ready. A goal

\[ (A_1\land A_2)\land(A_3\land A_4) \]

becomes a tree of smaller obligations. Each internal node is one \(\land I\) application; each leaf is proved independently. This divide-and-assemble pattern is exact because the constructor records both proofs.

The rule also structures proof search. When the target's outermost connective is \(\land\), backward application deterministically exposes two subgoals. Unlike guessing an intermediate lemma or choosing a disjunct, there is no ambiguity about the formulas required. This makes conjunction introduction an “invertible” goal-directed step in many proof-search settings, though operational details depend on the calculus.

Proof terms make dependency explicit. If \(a:A\) and \(b:B\), pairing gives \(\langle a,b\rangle:A\times B\). The term records which evidence supports each conjunct and supports later projections. Proof assistants can therefore reduce a conjunctive goal to separately checkable obligations, exploit independent automation for each branch, and reject construction if either branch remains unsolved.

Nested conjunctions expose a representational cost: binary \(\land\) requires bracketing. \((A\land B)\land C\) and \(A\land(B\land C)\) are interderivable but may have different proof-term shapes. The rule manages the complexity without erasing this structure.

Abstract Reasoning¶

Forward construction. Given \(\Gamma\vdash A\) and \(\Gamma\vdash B\), conclude \(\Gamma\vdash A\land B\). The rule does not require a relevance relation between \(A\) and \(B\) in ordinary logic.

Backward goal decomposition. To prove \(A\land B\), plan separate derivations of \(A\) and \(B\) under the required context. Completion of one branch alone is insufficient.

Soundness. If the premise derivations are semantically sound, every valuation satisfying their open assumptions satisfies both \(A\) and \(B\), and hence satisfies \(A\land B\). Therefore the rule preserves validity.

Commutativity derivation. From \(A\land B\), eliminate to obtain \(A\) and \(B\), then introduce \(B\land A\). This proves interderivability without pretending the formulas are identical.

Associativity derivation. Elimination and repeated introduction transform \((A\land B)\land C\) into \(A\land(B\land C)\) and back. Bracketing controls the construction tree even when logic proves equivalence.

Local reduction. If a proof constructs \(A\land B\) by \(\land I\) and immediately eliminates it to recover \(A\), the detour reduces to the original derivation of \(A\). This local soundness is a basic normalization step.^[4]^[2]

Expansion. Starting from a proof of \(A\land B\), eliminate to get both components and reintroduce their conjunction. This shows that the elimination rules recover enough information to reconstruct what the introduction rule built, a simple case of proof-theoretic harmony.

Knowledge Transfer¶

The rule transfers literally across paper proofs, proof trees, sequent systems, typed programs, and proof assistants when each target implements ordinary conjunction. The notation changes—from a bar rule, to line citations, to a pair constructor—but the roles remain two component derivations, compatible context, and one compound proof.

Under Curry–Howard, the mapping is exact: propositions become types, proofs become terms, conjunction becomes a product or pair-like inductive type, introduction becomes pair construction, and elimination becomes projection or pattern matching. This permits logical normalization results to appear as program reduction and turns a tactic that splits an A ∧ B goal into a type-directed constructor step.^[8]^[7]

The broader pattern—assemble a compound guarantee only after independently satisfying every required component—appears in checklists, multi-condition validation, and product construction. Those are analogies unless they use a formal conjunction and a sound inference system. Their portable residue belongs to Deductive Reasoning, Composition, and Validation rather than to this domain-specific node.

Resource-sensitive logics show a limit on transfer. The word “and” may correspond to more than one connective, with different context-use policies. One must map the exact connective and structural rules before importing the ordinary \(\land I\) schema.

Examples¶

Atomic example. From Rain and CatInside, infer Rain ∧ CatInside. Both premises must be separately available; the inference says nothing about causal or topical connection.

Fitch accessibility. If line 4 contains \(P\) and line 9 contains \(Q\), both at the current or an enclosing open scope, line 10 may be \(P\land Q\) justified by ∧I 4,9. If line 9 lies in a closed subproof, that citation is invalid.

Nested goal. To prove \(P\land(Q\land R)\), derive \(P\), \(Q\), and \(R\); introduce \(Q\land R\); then introduce \(P\land(Q\land R)\). The bracketing determines the two applications.

Reordering. From \(P\land Q\), eliminate \(P\) and \(Q\), then cite \(Q\) first and \(P\) second to infer \(Q\land P\). Conjunction Introduction participates in, but does not alone prove, commutativity.

Proof assistant. Given Lean hypotheses hP : P and hQ : Q, the term And.intro hP hQ has type P ∧ Q. If either term has the wrong type or is missing, the kernel rejects the construction.^[7]

Invalid missing conjunct. From \(P\) alone, P ∧ Q does not follow. Confusing this with disjunction introduction is a rule-shape error.

Invalid scope escape. Assume \(Q\) temporarily, derive it inside a subproof, close that assumption without deriving an implication, then combine the inner \(Q\) with an outer \(P\). This leaks a dependency and is rejected by context-sensitive proof systems.

Structural Tensions¶

Semantic obviousness versus proof availability. The truth table makes the rule look trivial, but a formal derivation needs both proofs in scope. Diagnostic: can each conjunct be cited with all dependencies still open?

Modular independence versus shared context. The conjuncts can be proved by unrelated methods, yet the results must coexist under a compatible assumption policy. Diagnostic: write the context above each premise and verify the rule permits their merge or reuse.

Compound packaging versus usable components. Introduction packages evidence; elimination unpacks it. Too much packaging produces detours, while too little prevents a compound goal from closing. Diagnostic: is the conjunction required by the goal or a later rule, or will it be immediately projected away?

Syntactic order versus semantic commutativity. \(A\land B\) and \(B\land A\) are interderivable, not the same parse tree. Diagnostic: distinguish formula identity from proved equivalence and proof-term isomorphism.

Classical sharing versus resource sensitivity. Standard contexts allow reuse, whereas linear systems track consumption and distinguish conjunction-like connectives. Diagnostic: identify the calculus and its structural rules before copying the shared-context schema.

Structural–Framed Character¶

Conjunction Introduction is strongly structural and domain-framed. Its proof transformation is exact, symbolic, and invariant across notational presentations. It has a small role signature, a semantic soundness proof, normalization behavior, and an executable proof-term interpretation.

Its substrate remains formal logic and type theory. Literal instances require formulas, derivations, contexts, a conjunction connective, and an inference relation. Everyday aggregation or satisfying two practical requirements may resemble the rule, but does not instantiate it without a formal proof system. The generic cross-domain residue is already captured by Deductive Reasoning and Composition, so the candidate is domain-specific rather than prime.

Structural Core vs. Domain Accent¶

The structural core is two independently secured components become one compound witness containing both. This supports modular proof construction, deterministic goal decomposition, and later recovery of either component.

The domain accent supplies the exact identity: object-language formulas; the \(\land\) connective; derivability judgments; accessible proof contexts; introduction/elimination rule pairing; normalization; and proof terms. Remove these commitments and the operation becomes generic assembly. Replace \(\land\) with \(\lor\), \(\to\), a multiplicative tensor, or a database join, and the correctness conditions change.

The rule's recurrence across proof presentations is intra-domain transfer. It does not establish the literal substrate independence needed for a prime.

Deductive Reasoning is the proposed minimal parent. Conjunction Introduction is a strict, truth-preserving deductive inference with explicit premises and conclusion.

Formal System is related because the rule is stated over a formal language and becomes operative only as part of a derivation calculus. It is not a second parent because the rule is an inferential operation, not a complete formal system of symbols, axioms, and rules.

Composition is a portable analogy: two proof objects are assembled into a structured pair. It does not supply the connective semantics or proof context.

Normalization is related through the reduction of an introduction immediately followed by elimination. It is a metatheoretic property/process, not the rule's genus.

Curry–Howard Correspondence explains the exact transfer to product/pair constructors in typed programming and proof assistants.

Relationships to Other Abstractions¶

Current abstraction Conjunction Introduction Domain-specific

Parents (1) — more general patterns this builds on

Conjunction Introduction is a kind of Deductive Reasoning Prime

Deductive Reasoning is the proposed minimal parent.

Hierarchy path (1) — routes to 1 parentless root

Conjunction Introduction → Deductive Reasoning

Neighborhood in Abstraction Space¶

Conjunction Introduction sits in a sparse region of the domain-specific corpus (80^th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Unclustered & Miscellaneous (1565 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-09-08

Not to Be Confused With¶

Logical conjunction: the connective and compound formula, not the introduction rule.
Conjunction Elimination: extracts a conjunct from an established conjunction.
Disjunction Introduction / Addition: needs only one disjunct and concludes \(A\lor B\).
Conjunction Fallacy: a probabilistic judgment error, not a proof rule.
Conjunctive syllogism: an older or system-specific label that may denote a different derived inference.
Adjunction in category theory: a functorial universal relationship unrelated to this textbook synonym.
Pairing in set theory: a construction analogous under Curry–Howard but not itself a logical inference without typing/proof judgments.
Comma in a sequent: may encode a context rather than an object-language conjunction; translating between them depends on the calculus.
Resource-sensitive “and”: additive and multiplicative connectives in linear logic have distinct introduction rules.

References¶

[1] Gerhard Gentzen, “Investigations into Logical Deduction,” originally Mathematische Zeitschrift 39 (1935), translated in M. E. Szabo, ed., The Collected Papers of Gerhard Gentzen (North-Holland, 1969), 68–131. registry ↩a ↩b

[2] Dag Prawitz, Natural Deduction: A Proof-Theoretical Study (Stockholm: Almqvist & Wiksell, 1965; Dover reprint, 2006). registry ↩a ↩b

[3] P. D. Magnus et al., forall x: Calgary—An Introduction to Formal Logic, chapter 17, “Basic Rules for TFL,” Open Logic Project. HTML edition. registry ↩

[4] Andrzej Indrzejczak, “Natural Deduction Systems in Logic,” Stanford Encyclopedia of Philosophy (2021; substantive revision 2023). Archived 2023 edition. registry ↩a ↩b ↩c

[5] Matthew McKeon, “Propositional Logic,” Stanford Encyclopedia of Philosophy (2023). Entry. registry ↩

[6] Open Logic Project, The Open Logic Text, chapter 58, section 58.4, “Natural Deduction.” Complete PDF. registry ↩

[7] Lean Project, Functional Programming in Lean, “Propositions, Proofs, and Indexing.” Official documentation. registry ↩a ↩b ↩c ↩d

[8] William A. Howard, “The Formulae-as-Types Notion of Construction,” in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (Academic Press, 1980), 479–490. registry ↩