Condensed Detachment¶
An inference rule that unifies an implication’s antecedent with a minor premise and detaches the most general resulting consequent.
Core Idea¶
Condensed detachment—also called rule D—combines uniform substitution and modus ponens into one inference operation. Given a major premise whose outer form is \(A\to B\) and a minor premise \(C\), first standardize variables apart, then compute a most general unifier \(\sigma\) of \(A\) and \(C\). If unification succeeds, infer \(\sigma(B)\), with any conventionally permitted variable normalization.[1]
The word “condensed” refers to doing only the substitution needed to detach the consequent, while retaining a most-general result. Any more specialized conclusion obtainable from that application is a substitution instance of the condensed conclusion. Kalman formalized this rule using Robinson-style unification and proved a precise relationship with derivations using uniform substitution plus ordinary detachment.[1] The identity is therefore a stable rule schema, not shorthand for an arbitrary short proof.
Structural Signature¶
Recognition roles:
- Major formula: an implication \(A\to B\) eligible for detachment.
- Minor formula: a theorem or premise \(C\) to be matched against \(A\).
- Variable separation: variables in the two premises are renamed apart before matching.
- Unification problem: solve \(A\sigma=C\sigma\), including an occurs check under first-order term conventions.
- Most general unifier: choose \(\sigma\) such that every other unifier factors through it.
- Detached consequent: output \(B\sigma\), not the entire instantiated implication.
- Failure branch: if no unifier exists, this rule application yields no conclusion.
A practical recognition test asks whether the inference explicitly uses the most-general unifier of antecedent and minor premise and then returns the substituted consequent. If substitution is arbitrary, if the minor merely syntactically equals the antecedent, or if all resolvents are produced, the operation is not specifically condensed detachment.
What It Is Not¶
It is not plain modus ponens, which derives \(B\) from exactly \(A\to B\) and \(A\) without computing substitutions. It is not uniform substitution alone, because it produces a conclusion by detachment. It is not resolution: resolution operates on complementary literals/clauses and creates a resolvent, while rule D matches an implicational antecedent with a minor formula.
It is not every use of unification in type inference or logic programming. Those practices share an algorithmic ingredient but have different input/output roles. It is also not automatically a complete proof system. D-completeness is a property of a specified axiom basis and logic: whether conclusions obtainable with substitution and modus ponens are recoverable, in the appropriate substitution-instance sense, through D alone.[2] One cannot infer D-completeness merely because rule D is well defined.
Scope of Application¶
The rule belongs to implicational propositional calculi, equivalential calculi encoded as terms, single-axiom investigations, automated deduction, and the formula-as-types study of combinatory logic. It was proposed by Carew Meredith in the 1950s and later given rigorous unification-based formulations.[1] Hindley and David Meredith relate rule D to principal type-scheme computation under the formulas-as-types correspondence.[2]
Automated theorem provers use the rule as a compact inference kernel for search over axiom systems. McCune and Wos reported experiments on 112 condensed-detachment problems using the OTTER prover, varying search and deletion strategies.[3] Such application evidence shows recurrence, not that D dominates every theorem-proving calculus. The rule’s scope requires an implication-like constructor, substitutable variables/terms, and a unification discipline.
Clarity¶
The abstraction clarifies where generality enters an inference. Ordinary presentations can first instantiate an axiom many ways and then detach. Rule D reverses that workflow: match the actual minor to the antecedent, compute only a most-general necessary substitution, and return the most-general detachable consequent.
Three checks prevent ambiguity. Variables from premises must be standardized apart so same spellings do not create accidental identity. The unifier must be most general, not an arbitrary ground substitution. Finally, the result is compared up to consistent variable renaming, since a different fresh-variable alphabet does not change the inference. A purported example lacking these controls does not discriminate condensed detachment from ad hoc substitution.
Manages Complexity¶
Rule D compresses two recurring proof steps—substitution and modus ponens—into one generative transition. Rather than enumerate infinitely many substitution instances of a theorem, a prover unifies on demand and keeps a conclusion that subsumes its specializations. This reduces representational redundancy and exposes the principal conclusion available from a premise pair.[1]
The compression does not eliminate search. A theorem prover still chooses major/minor pairs, handles duplicate or subsumed formulas, controls term growth, and selects lemmas. Unification can fail or generate large substitutions. Condensing inference therefore narrows one dimension of branching while leaving strategic proof search explicit, as automated experiments demonstrate.[3]
Abstract Reasoning¶
Suppose \(A\to B\) and \(C\) are standardized apart. If \(\sigma\) is their most-general antecedent/minor unifier, then \(B\sigma\) represents all conclusions from that pair obtainable by first making compatible substitution instances and then applying modus ponens: any such more specific output factors through a further substitution. This is the principal-result invariant.[1]
Failure to unify blocks only that pair, not the entire calculus. D-completeness questions then ask whether iterated D applications recover the theory generated by substitution and detachment. Hindley and Meredith show that the answer depends on the system: the rule is complete for specified intuitionistic and classical implicational logics but incomplete for weaker BCK and BCI systems.[2] This conditional result is a boundary against treating D as universally complete.
Knowledge Transfer¶
Literal transfer occurs between formal-logic calculi and automated proof engines when implication, substitution, and most-general unification preserve the same roles. The formulas-as-types correspondence supplies a rigorous adjacent transfer: condensed detachment corresponds to an algorithm for principal type schemes in combinatory logic, not merely a loose analogy.[2]
Unification techniques transfer instrumentally from logic programming or type inference, but their host operations do not thereby become rule D. Outside formal symbolic systems, “detach after matching” is metaphorical unless terms, substitutions, most-generality, and consequent formation are defined. The generic parent Deductive Reasoning transfers broadly; Condensed Detachment retains specialist syntax and proof-theoretic obligations.
Examples¶
Simple variable specialization. Let the major premise be \((p\to q)\to((r\to p)\to(r\to q))\) and the minor be \(a\to b\). Standardize variables apart. The antecedent \(p\to q\) unifies with \(a\to b\) by \(\sigma=\{p\mapsto a,q\mapsto b\}\). Rule D yields \((r\to a)\to(r\to b)\). Grounding \(r\) later gives more specific substitution instances; it is not required for the D step.
Unification with structure. From major \(P(f(x))\to Q(x)\) and minor \(P(f(a))\), the most-general unifier maps \(x\) to \(a\), yielding \(Q(a)\). Ordinary modus ponens would require the major to be instantiated first; condensed detachment packages that instantiation with detachment.
Failure case. From \(P(f(x))\to Q(x)\) and \(P(g(a))\), no first-order unifier exists when \(f\) and \(g\) are distinct function symbols. Rule D produces no conclusion. A procedure that changes symbols or uses approximate matching has left the abstraction.
Completeness boundary. A successful sequence of D steps proves a theorem within its chosen axiom basis. That success does not by itself show every substitution-plus-detachment theorem is D-derivable; D-completeness requires a system-level proof.[2]
Structural Tensions¶
- Generality versus operational size. Most-general conclusions subsume special cases, yet their terms can grow. Diagnostic: compare subsumption gained with the size/depth of generated formulas.
- Inference compression versus search explosion. One rule replaces two steps, but premise pairing remains combinatorial. Diagnostic: hold the calculus fixed and measure proof search under stated selection strategies.
- Elegant rule versus basis dependence. D is concise, while D-completeness varies by axiom system. Diagnostic: name the exact logic and axiom basis before claiming completeness.
- Autonomy versus reduction. Unification + substitution + modus ponens are components, but only D fixes their sequencing and principal-output invariant. Diagnostic: require most-general antecedent/minor matching followed by consequent extraction.
Structural–Framed Character¶
The rule is strongly structural: variable names can change, and the inference is determined by term structure, unification, and implication position. Its framing comes from a chosen logical language, substitution convention, treatment of occurs check, and proof-system goals. “Minimal substitution” is meaningful relative to most-generality, not an informal count of symbols replaced.
Historical naming also frames the node: “rule D” belongs to a line of implicational-calculus research. The abstraction is evaluatively neutral; shorter or more elegant proofs are research goals, not part of truth preservation. Outside formal logic its vocabulary does not travel literally.
Structural Core vs. Domain Accent¶
The portable skeleton is match a requirement against an available item, compute a most-general adaptation, and propagate the adapted result. The indispensable accent is formal syntax: implication, theoremhood, variables, term substitution, unification, and derivability. Remove those and the name becomes an analogy to pattern matching.
The candidate therefore does not clear the prime bar. It is autonomous within logic because its rule schema, success/failure test, generality invariant, proof-theoretic consequences, and automated uses recur independently of any single axiom.
Instantiates / Related Primes¶
Condensed Detachment specializes Deductive Reasoning: it is a truth-preserving formal inference rule under its host calculus. It also uses Unification as a technical operation, but the accepted catalog’s type-inference and matching nodes are not direct genera for a proof rule. Modus ponens is a component rather than a proposed parent.
The minimal graph proposal is therefore only prime:deductive_reasoning. This avoids conflating a rule with one of its algorithms or with a particular proof representation.
Relationships to Other Abstractions¶
Current abstraction Condensed Detachment Domain-specific
Parents (1) — more general patterns this builds on
-
Condensed Detachment is a kind of Deductive Reasoning Prime
Condensed Detachment specializes Deductive Reasoning: it is a truth-preserving formal inference rule under its host calculus.It also uses Unification as a technical operation, but the accepted catalog’s type-inference and matching nodes are not direct genera for a proof rule. Modus ponens is a component rather than a proposed parent. The minimal graph proposal is therefore only
prime:deductive_reasoning. This avoids conflating a rule with one of its algorithms or with a particular proof representation.
Hierarchy path (1) — routes to 1 parentless root
- Condensed Detachment → Deductive Reasoning
Neighborhood in Abstraction Space¶
Condensed Detachment sits in a sparse region of the domain-specific corpus (82nd percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Computational Number Theory & Enumeration (13 abstractions)
Nearest neighbors
- Variable Elimination — 0.83
- Transitive Set — 0.81
- Prime Model (Model Theory) — 0.81
- Classification of Discontinuities — 0.81
- Probabilistic Graphical Model — 0.81
Computed from structural-signature embeddings · 2026-09-08
Not to Be Confused With¶
- Modus ponens: exact antecedent matching without computed most-general substitution.
- Uniform substitution: instantiates formulas but does not detach a consequent.
- Resolution: combines clauses through complementary literals.
- Unification: supplies the matcher but not the full inference rule.
- Type inference: may compute principal types using related machinery, but has different judgments and outputs.
- D-completeness: a property of a rule plus a specified basis, not a synonym for the rule.
- Reverse condensed detachment: a distinct, directionally altered search operation in some literature.
References¶
[1] J. A. Kalman, “Condensed Detachment as a Rule of Inference,” Studia Logica 42 (1983), 443–451, doi:10.1007/BF01371632. registry ↩a ↩b ↩c ↩d ↩e
[2] J. Roger Hindley and David Meredith, “Principal Type-Schemes and Condensed Detachment,” Journal of Symbolic Logic 55 (1990), 90–105, doi:10.2307/2274956. registry ↩a ↩b ↩c ↩d ↩e
[3] William McCune and Larry Wos, “Experiments in Automated Deduction with Condensed Detachment,” in Automated Deduction—CADE-11, LNCS 607 (Springer, 1992), 209–223, doi:10.1007/3-540-55602-8_167. registry ↩a ↩b