Procedure for converting proofs that use Detachment to proofs with Condensed Detachment

Question

I’Recently I’ve been looking into Condensed Detachment (CD) as an inference rule for axiomatic systems. I have a hazy understanding of how it works and how to find a most general unifier for two wffs. Is there a general procedure for converting an axiomatic proof using normal Detachment (Modus Ponens) into a proof using CD?

Condensed Detachment takes a formula $A \to B$ and a formula $C$ such that $C$ and $A$ have a $B$-acceptable most general unifier and allows one to infer $B’$ which results from the substitution to unify $A$ and $C$.

For example, the following is a proof using CD:

1. $p \to q \to p$ [Ax. 1]

2. $(p \to (q \to r)) \to (p \to q) \to p \to r$ [Ax. 2]

3. $(p \to q) \to p \to p$ [2.1 CD]

Here is a proof of the same theorem using normal detachment and substitution:

1. $p \to q \to p$ [Ax. 1]
2. $(p \to (q \to r)) \to (p \to q) \to p \to r$ [Ax. 2]
3. $(p \to (q \to p)) \to (p \to q) \to p \to p$ [2, $r:=p$]
4. $(p \to q) \to p \to p$ [1,3 MP]

Answer 1

Is there a general procedure for converting an axiomatic proof using normal Detachment (Modus Ponens) into a proof using CD?

Yes, straightforwardly. First note that something like "[(line) 2, r:=p]" is not a dedicated reason of the proof system, so lines like that have to be merged with the line they reference.

Then use the same reasons in the same lines, and refill all the formulas with most general unifiers. Since condensed detachment results are always most general, they can always replace the at most as general formulas in their positions. For example, consider (1): 0→(1→0) and (2): (0→(1→2))→((0→1)→(0→2)) as axioms, and the proof

1. 0→(0→0)  (1)
2. 0→((0→0)→0)  (1)
3. (0→((0→0)→0))→((0→(0→0))→(0→0))  (2)
4. (0→(0→0))→(0→0)  (D):2,3
5. 0→0  (D):1,4

which has reasons (1),(1),(2),(D):2,3,(D):1,4. Building a consensed detachment proof with this sequence of reasons results in:

1. 0→(1→0)  (1)
2. 0→((1→0)→0)  (1)
3. (0→((1→0)→0))→((0→(1→0))→(0→0))  (2)
4. (0→(1→0))→(0→0)  (D):2,3
5. 0→0  (D):1,4

Since no line is referenced multiple times, and later lines are used first, we could simply write in this case, that the proof is D(D(2,1),1), or just DD211 since prefix notation does not need parentheses. Here 1 and 2 stand for axiom numbers. I wrote a tool that can construct the latter proof simply like:

./pmGenerator -c -n -s CpCqp,CCpCqrCCpqCpr --parse DD211

Here CpCqp,CCpCqrCCpqCpr are the axioms (1),(2) in order, given in normal Polish notation.

In case you wonder how to find the most general unifier of tree structures (e.g. formulas) algorithmically, you may have a look at my implementation. This can be rather complicated. In some cases there is exponential blowup. I wouldn't want to do this by hand.