Condensed Detachment

From Wikipedia, the free encyclopedia

Condensed Detachment is a method of finding the most general possible conclusion given two formal logical statements. It was developed by the Irish Logician Carew Meredith in the 1950's, along with the "D" operator notation for complete proofs.

Contents 1 Informal description 2 Formal description 2.1 footnotes 3 D-notation 4 References

[edit] Informal description

A rule of detachment says:

Given that P implies Q
And Given P
---------------
Produce Q

Condensed detachment goes a step further and says

 Given that P implies Q
 And Given an R
------------
 Produce the most general possible result of substitutions into P and R, 
 followed by a standard rule of detachments. 

A substitution A that when applied to P produces T, and a substituition B that when applied to R produces T, are called the Unifiers of P and Q. Various unifiers may produce expressions with varying numbers of free variables. Some possible unifying expression are substitution instances of others. If one expression is a substitution instance of another, then that other is called "more general".

If the most general unifier is used in Condensed Detachment, then the logical result is the most general conclusion that can be made in the given inference with the given second expression. (And since any weaker inference you can get is a substitution instance of the most general one, nothing less than the most general unifier is ever used in practice.)

In some logics (such as standard PC) have a set of defining axioms with the "D-completeness" property. Any conclusion that can be arrived at by a sequence of Uniform Substitution and Modus Ponens steps can either be done as a sequence of Condensed Detachment steps, or is a substitution instance of something that can be.

[edit] Formal description

From an e-mail from Dolph Ulrich to Larry Wos, used by Ulrich's permission. The original uses Lukasiewicz ("Polish" or "prefix") notation, which is the traditional notation for discussions of Condensed Detachment, infix notation has been added for the convenience of those not familiar with the traditional notation. Example expression: CpCqp [ ]

---

Pick any sentential language, L, that includes a binary connective, say C [ in the infix comments], and let the rules of Detachment/Modus Ponens (for C []) and of Uniform Substitution be formulated as usual.

Where Cαβ () (the major premise) and γ (the minor premise) are any two formulas, let γ' be an alphabetic variant of γ containing no letters occurring in Cαβ (). If there exists a substitution s of formulas for the letters occurring in α and γ' for which s(α) = s(γ'), α and γ' are said to be "unifiable", and s is called a unifier for them. When α and γ;' are unifiable, there is, by the Unification Theorem of Robinson's "A machine-oriented logic based on the resolution principle" Journal of the ACM, volume 12 (1965), pp. 23-41, always a most general unifier for the two, that is, a substitution s of formulas for the letters occurring in α and γ' such that for any other substitution s' unifying α and γ;', s'(α) is a substitution instance of s(α). By trivial letter-for-letter alterations, s can always be turned into a β-acceptable most general unifier s* for α and γ', that is, a most general unifier for α and γ' for which no sentence letters occurring in s * (α) occur in β but not α. Rule D can be formulated as follows:

RULE D: Premises: Any two formulas Cαβ [ ] and γ for which α and γ have a common substitution instance. Conclusion: any alphabetic variant of s * (β) where γ' is any alphabetic variant of gamma containing no sentence letters in common with Cαβ [] and s* is any β-acceptable most general unifier for α and γ'.

METATHEOREM(Footnote ¹): For each set A of wffs of L, let the formulas Classically Derivable from those in A be the formulas that can be derived from those in A using the rules of Detachment and Uniform Substitution, and let the formulas D-derivable from those in A be the formulas that can be derived from those in A using the rule D of Condensed Detachment alone. Then a formula is classically derivable from formulas in A if and only if it is a substitution instance of at least one formula D-derivable from formulas in A.</a>

DEFINITION: A set A of wffs of L is D-complete if and only if every formula classically derivable from formulas in A is D-derivable from formulas in A.</a>

D-completeness is, however, not a property of logics but of specific axiom sets. For instance, {EEpqEErqEpr} [ (p=q) = [(r=q) = (p=r)] ] is (with Substitution and Modus Ponens for E [ = ] as the rules) a complete axiom set for the classical equivalential calculus, but it is not D-complete--nor is virtually any other well-known axiom set for EQ. The set {EEpqEErqEsEsEsEsEpr} [ (p=q) = [(r=q) = {s=(s=(s=(s=(p=r))))}] ], however, is not only a complete axiom set for that same calculus--it happens to be D-complete as well. (footnote ²)

[edit] footnotes

Footnote 1: Published in J. A. Kalman's "Condensed detachment as a rule of inference" Studia Logica, volume 42 (1983), pp. 443-451, though the result was certainly known to Meredith, Prior, and many others, and had presumably been proved by them earlier though not published.

Footnote 2: D. Ulrich, "D-complete axioms for the classical equivalential calculus", Bulletin of the Section of Logic, forthcoming].

[edit] D-notation

Since a given major premise and a given minor premise uniquely determine the conclusion (up to variable renaming), Meredith observed that it was only necessary to note which two statements were involved, and that Condensed Detachment was used, without any other notation required. This led to the "D-notation" for proofs. This notation uses the "D" operator to mean Condensed Detachment, and takes 2 arguments, in a standard polish notation string. For example:

 D D 1 2 D 3 4 

means a Condensed detachment step using the result of two prior condensed detachment steps, the first of which used axioms 1 and 2, and the second of which used axioms 3 and 4.

This notation, besides being used in some automated theorem provers, sometimes appears in catalogs of proofs, such as the "Shortest known proofs of the propositional calculus theorems from Principia Mathematica"

Condensed Detachment's use of Unification predates the Resolution techniques of automated theorem proving.

[edit] References

• BCK and BCI logics, condensed detachment and the $2$-property by J. Roger Hindley, Notre Dame Journal of Formal Logic 34, no. 2 (1993), 231–250
• Experiments in Automated Deduction with Condensed Detachment, William McCune and Larry Wos, Proceedings of the 11th International Conference on Automated Deduction (1992)