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

v3 · 2026-09-19 · History

Domain-specific #

1541

Domain group

Humanities

Origin domain

Philosophy

Subdomains

Logic, Natural Deduction → Philosophy

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. \]

How would you explain it like I'm…

Putting Two Proofs Together

If you know it's sunny, and you know it's warm, then you can say "it's sunny and warm." Putting two things you already know together with "and" is Conjunction Introduction. You need to know both parts first.

The 'And' Building Rule

In logic, people build proofs step by step, and each step has to follow a rule. Conjunction Introduction is the rule that says: if you have already proved A, and you have already proved B, you may write down "A and B." Both pieces must really be proved, and under the same starting assumptions. A partner rule works backward: if you have "A and B," you can take out either piece. Together, these two rules explain what "and" means in a proof.

Proving an And From Both Parts

Conjunction Introduction is a rule of inference that combines a proof of A and a proof of B into a proof of A and B, written A with B above a line and A-and-B below it. In the version that tracks assumptions, if A and B can each be derived from the same set of assumptions Gamma, then so can A and B; in a Fitch-style proof, the lines for A and B must be accessible where the conjunction is introduced. The rule is truth-preserving, since whenever A and B are both true their conjunction is true, but it is really about how proofs are built rather than just truth tables. Paired with Conjunction Elimination, which recovers either part from a conjunction, it gives "and" its meaning in proofs: to prove a conjunction, prove both parts. In computer proof systems, a proof of A and B is simply a pair made of a proof of A and a proof of B.

 

Conjunction Introduction (∧I) is the rule of inference that combines proofs of two formulas into a proof of their conjunction. In natural deduction it is displayed with premises A and B above the line and A ∧ B below; in a context-indexed form it reads: from Γ ⊢ A and Γ ⊢ B, infer Γ ⊢ A ∧ B. The shared context Γ expresses that both derivations depend on compatible undischarged assumptions, and Fitch-style systems enforce the same constraint by requiring the cited lines to be accessible where A ∧ B is introduced. The sequent A, B ⊢ A ∧ B is a valid instance, not the most general schema. The rule is truth-preserving, but its identity is proof-theoretic: it specifies how a proof of a compound is constructed from proofs of its immediate components. Paired with Conjunction Elimination, it contributes to the inferential meaning of ∧: to establish a conjunction you must establish both conjuncts, and from a conjunction either conjunct can be recovered. The same construction appears in sequent calculi, typed lambda calculi, and proof assistants; under propositions-as-types, a proof of A ∧ B is a pair ⟨a, b⟩, and Lean's And.intro hA hB is a machine-checked instance.

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.

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.

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.

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.

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.

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.

Relationships to Other Abstractions

Current abstraction Conjunction Introduction Domain-specific

Parents (1) — outgoing typed relations

• Conjunction Introduction is a kind of Deductive Reasoning Prime

  Deductive Reasoning is the broader abstraction this entry instantiates.

Hierarchy path (1) — routes to 1 parentless root

• Conjunction Introduction → is a kind of Deductive Reasoning

Neighborhood in Abstraction Space

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

Family — Unclustered & Miscellaneous (2769 abstractions)

Nearest neighbors

• Rule of replacement — 0.84
• Peirce's Law — 0.82
• Propositional formula — 0.82
• Formal Theory — 0.82
• Accessibility Relation — 0.82

Computed from structural-signature embeddings · 2026-10-25