# Proving $(p \to (q \to r)) \to ((p \to q) \to (p \to r))$

I'm looking for a way to prove

$$(p \to (q \to r)) \to ((p \to q) \to (p \to r))$$ from the axioms

\begin{align} & p \to (q \to p) \\ & (p \to (p \to q)) \to (p \to q) \\ & (p \to q) \to ((q \to r) \to (p \to r)) \\ & (\sim p \to \, \sim q) \to (q \to p) \\ \end{align} using universal substitution and modus ponens

I suspect the fourth axiom is not necessary for the proof.

I have been working in Tarski's Introduction to Logic and am trying to establish the equivalence of his axiom system with the axioms used at us.metamath.org

\begin{align} & p \to (q \to p) \\ & (p \to (q \to r)) \to ((p \to q) \to (p \to r)) \\ & ( \sim p \to \, \sim q) \to (q \to p) \\ \end{align} which will allow me to connect Tarski's 4 axioms with all sorts of interesting proofs on that site.

-
Do you have the deduction theorem available for your system? –  Henning Makholm Dec 11 '11 at 2:32
@toph: I agree that the fourth axiom is not relevant here. The proposition you are trying to prove is essentially an internal form of modus ponens, which is valid intuitionitically, but the fourth axiom is essentially double negation elimination. –  Zhen Lin Dec 11 '11 at 2:55
This appears to be hard -- are you sure the four axioms you've given are all there is? The first three ones are the K, W, and (almost) B axioms of the BCKW system of combinatory logic, but the C axiom is missing. That makes me doubt that the system you present is complete. –  Henning Makholm Dec 11 '11 at 4:45
The axioms are taken from page 147 of Tarski's Introduction to Logic. I must (guiltily) add that there are three other axioms: (p <-> q) -> (p -> q), (p <-> q) -> (q -> p), (p -> q) -> ((q -> p) -> (p <-> q). I couldn't see how these axioms, which basically define equivalence, would be necessary. But following your remarks I suspect the last axiom above in particular might be crucial. Thanks for your help so far! –  toph Dec 11 '11 at 13:11
Aha! Wikipedia's List of logic systems lists your three (original) axioms as Hilbert's second system for "Postive implicational calculus" (i.e., the implicational fragment of intuitionistic logic). Since your target sentence is intuitionistically valid, it indeed ought to be derivable. Still beats me how, though. –  Henning Makholm Dec 11 '11 at 15:23

As you suspected, this can be proved from the first three axioms only. I couldn't find a short proof, though – I tried brute force enumeration of the theorems deducible from the three axioms (by taking all pairs of theorems already proved and unifying one with the premise of the other), but didn't find your target in the first $80000$ theorems proved.

I then found some guidance in the article on relevance logic in the Handbook of Philosophical Logic. Relevance logic focuses on the fragment of logic in which, roughly speaking, the premises are relevant to the conclusions. It doesn't include the axiom $p\to(q\to p)$, which allows us to add an irrelevant premise to a theorem already proved without that premise, and is thus strictly weaker than the system you're using, but we can nevertheless make use of the results cited in that article.

I'll first describe the structure of the proof and how I found it, and then give the proof in detail. Here are the names I'll use for the axioms; the first column names the corresponding axioms of combinator logic, for comparison with the discussion in the comments under the question:

$$\begin{array}{c|l|l} \mathbf I&\text{self-implication}&p\to p\\ \mathbf K&\text{weakening}& p \to (q \to p) \\ \hline \mathbf B&\text{prefixing}& (p \to q) \to ((r \to p) \to (r \to q)) \\ \mathbf A&\text{suffixing}& (p \to q) \to ((q \to r) \to (p \to r)) \\ \hline \mathbf W&\text{contraction}& (p \to (p \to q)) \to (p \to q) \\ \mathbf S&\text{self-distribution}&(p \to (q \to r)) \to ((p \to q) \to (p \to r))\\ \hline \mathbf C&\text{permutation}&(p\to(q\to r))\to(q\to(p\to r))\\ &\text{assertion}&p\to((p\to q)\to q) \end{array}$$

(The names are the ones used in the article, except I use "weakening" instead of "positive paradox", since it's shorter and makes more sense to me.)

Theorem $1$ of the article states that, with modus ponens (and implicitly universal substitution), the axiom sets formed by self-implication and one each from the three pairs prefixing/suffixing, contraction/self-distribution and permutation/assertion lead to the same theory.

What you have is weakening, suffixing and contraction. Self-implication can be deduced from weakening and contraction in a single step (by substituting $p$ for $q$ everywhere). Thus, if we can deduce assertion in your system, the theorem will tell us that we can deduce everything else, including your target, self-distribution. I did find a proof for assertion by brute force search.

The article doesn't give a proof of its Theorem $1$ and only says that it can be proved by consulting a book that isn't available online and doing some "fiddling", so we still have to show how to get from self-implication, suffixing, contraction and assertion to self-distribution.

I found a deduction of self-distribution online that uses prefixing and permutation. It turns out that prefixing is deducible in a single step from suffixing and permutation, so the problem remained only to deduce permutation. Again, I found a proof for this by brute force search.

So here's the entire proof put together, starting with your three axioms and ending with your target. First, a high-level description similar to the actual calls in my Java code:

assertion = t (t (weakening,suffixing),contraction);
permutation = t (suffixing,m (assertion,suffixing));
prefixing = m (suffixing,permutation);
target = t (m (prefixing,prefixing),t (permutation,m (contraction,prefixing)));


Each call to m is an application of modus ponens, in which the first argument is $A$, the second argument is $A\to B$ and the most general unifier that makes the $A$s coincide is used. Each call to t is an invocation of transitivity (i.e. deducing $A\to C$ from $A\to B$ and $B\to C$), which can be implemented as

t (A->B,B->C) = m (B->C,m (A->B,suffixing))


using suffixing, or as

t (A->B,B->C) = m (A->B,m (B->C,prefixing))


once prefixing is available.

Here's the proof spelled out in $14$ steps. The first table shows the theorems used to generate the antecedents $A$ and the implications $A\to B$ for modus ponens, as well as the resulting theorems $B$:

$$\begin{array}{c|c|c|c|c} &&A&A\to B&B\\\hline \text{(a)}&\text{weakening}&&&p \to (q \to p)\\ \text{(b)}&\text{suffixing}&&&(p \to q) \to ((q \to r) \to (p \to r))\\ \text{(c)}&\text{contraction}&&&(p \to (p \to q)) \to (p \to q)\\ \hline \text{(d)}&\text{*}&\text{(a)}&\text{(b)}&((p \to q) \to r) \to (q \to r)\\ \text{(e)}&&\text{(b)}&\text{(d)}&p \to ((p \to q) \to (r \to q))\\ \text{(f)}&\text{*}&\text{(e)}&\text{(b)}&(((p \to q) \to (r \to q)) \to s) \to (p \to s)\\ \text{(g)}&\text{assertion}&\text{(c)}&\text{(f)}&p \to ((p \to q) \to q)\\ \text{(h)}&&\text{(g)}&\text{(b)}&(((p \to q) \to q) \to r) \to (p \to r)\\ \text{(i)}&\text{*}&\text{(b)}&\text{(b)}&(((p \to q) \to (r \to q)) \to s) \to ((r \to p) \to s)\\ \text{(j)}&\text{permutation}&\text{(h)}&\text{(i)}&(p \to (q \to r)) \to (q \to (p \to r))\\ \text{(k)}&\text{prefixing}&\text{(b)}&\text{(j)}&(p \to q) \to ((r \to p) \to (r \to q))\\ \text{(l)}&&\text{(k)}&\text{(k)}&(p \to (q \to r)) \to (p \to ((s \to q) \to (s \to r)))\\ \text{(m)}&&\text{(c)}&\text{(k)}&(p \to (q \to (q \to r))) \to (p \to (q \to r))\\ \text{(n)}&\text{*}&\text{(j)}&\text{(b)}&((p \to (q \to r)) \to s) \to ((q \to (p \to r)) \to s)\\ \text{(o)}&&\text{(m)}&\text{(n)}&(p \to (q \to (p \to r))) \to (q \to (p \to r))\\ \text{(p)}&\text{*}&\text{(l)}&\text{(b)}&((p \to ((q \to r) \to (q \to s))) \to t) \to ((p \to (r \to s)) \to t)\\ \text{(q)}&\text{self-distribution}&\text{(o)}&\text{(p)}&(p \to (q \to r)) \to ((p \to q) \to (p \to r))\\ \end{array}$$

The asterisks mark intermediate steps in invocations of transitivity. Note that most theorems with more than three variables occur only in such intermediate steps. Substitutions are being performed as late as possible; by performing them as early as possible, the proof could be written using only theorems with at most three variables.

The second table shows the substitutions used; you can also find these automatically by unification. The variables are named such that they appear in alphabetical order in the resulting theorems.

$$\begin{array}{c|l|l} &A&A\to B\\\hline \text{(d)}& p\mapsto q,q\mapsto p& p\mapsto q,q\mapsto (p \to q),r\mapsto r\\ \text{(e)}& p\mapsto r,q\mapsto p,r\mapsto q& p\mapsto r,q\mapsto p,r\mapsto ((p \to q) \to (r \to q))\\ \text{(f)}& p\mapsto p,q\mapsto q,r\mapsto r& p\mapsto p,q\mapsto ((p \to q) \to (r \to q)),r\mapsto s\\ \text{(g)}& p\mapsto (p \to q),q\mapsto q& p\mapsto p,q\mapsto q,r\mapsto (p \to q),s\mapsto ((p \to q) \to q)\\ \text{(h)}& p\mapsto p,q\mapsto q& p\mapsto p,q\mapsto ((p \to q) \to q),r\mapsto r\\ \text{(i)}& p\mapsto r,q\mapsto p,r\mapsto q& p\mapsto (r \to p),q\mapsto ((p \to q) \to (r \to q)),r\mapsto s\\ \text{(j)}& p\mapsto q,q\mapsto r,r\mapsto (p \to r)& p\mapsto (q \to r),q\mapsto r,r\mapsto p,s\mapsto (q \to (p \to r))\\ \text{(k)}& p\mapsto r,q\mapsto p,r\mapsto q& p\mapsto (r \to p),q\mapsto (p \to q),r\mapsto (r \to q)\\ \text{(l)}& p\mapsto q,q\mapsto r,r\mapsto s& p\mapsto (q \to r),q\mapsto ((s \to q) \to (s \to r)),r\mapsto p\\ \text{(m)}& p\mapsto q,q\mapsto r& p\mapsto (q \to (q \to r)),q\mapsto (q \to r),r\mapsto p\\ \text{(n)}& p\mapsto q,q\mapsto p,r\mapsto r& p\mapsto (q \to (p \to r)),q\mapsto (p \to (q \to r)),r\mapsto s\\ \text{(o)}& p\mapsto q,q\mapsto p,r\mapsto r& p\mapsto q,q\mapsto p,r\mapsto (p \to r),s\mapsto (q \to (p \to r))\\ \text{(p)}& p\mapsto p,q\mapsto r,r\mapsto s,s\mapsto q& p\mapsto (p \to (r \to s)),q\mapsto (p \to ((q \to r) \to (q \to s))),r\mapsto t\\ \text{(q)}& p\mapsto p,q\mapsto (p \to q),r\mapsto r& p\mapsto p,q\mapsto p,r\mapsto q,s\mapsto r,t\mapsto ((p \to q) \to (p \to r))\\ \end{array}$$

-
Well done! ${}$ –  Henning Makholm Dec 21 '11 at 13:48
Would you mind if I add a column to your first table showing the corresponding combinator names for comparison with the discussion between me and Zhen Lin in the comments? –  Henning Makholm Dec 21 '11 at 13:53
@Henning: That would be great, thanks! –  joriki Dec 21 '11 at 13:55
@Henning: Interesting -- so the answer actually fits well with your discussion, in that the hard part that I did by computer search was to deduce $\mathbf C$/permutation (up to step (j)), and the rest was known. –  joriki Dec 21 '11 at 14:29
@joriki It might interest you to know, if you don't already, that d) here (((p→q)→r)→(q→r)) is more general than a) (p→(q→p)) in the sense that we can get a) just from d), but not conversely. –  Doug Spoonwood Jun 14 '13 at 3:30

It seems to me that a much simpler and human readable proof is possible, unless I’m misunderstanding something. Using the Deduction Theorem, the result is relatively straightforward to prove. This motivated me to prove the Deduction Theorem for this logical system, which I found to be less straightforward, but still not particularly difficult.

To make sure we’re all on the same page, the logical system in question consists of the inference rule modus ponens (MP) and the following three axiom schema:

axiom 1 $\;\;\;\;\; p \; \rightarrow \; (q \rightarrow p)$

axiom 2 $\;\;\;\;\;(p \rightarrow q) \;\; \rightarrow \;\; [\; (q \rightarrow r) \rightarrow (p \rightarrow r) \; ]$

axiom 3 $\;\;\;\;\;[\; p \rightarrow (p \rightarrow q) \; ] \;\; \rightarrow \;\; (p \rightarrow q)$

We want to show that the following wff (well formed formula) is provable in this logical system:

$$[p \rightarrow (q \rightarrow r)] \;\; \rightarrow \;\; [(p \rightarrow q) \rightarrow (p \rightarrow r)]$$

By 3 applications of the Deduction Theorem (proved further below), it suffices to prove $r$ under the following assumptions: $p \rightarrow (q \rightarrow r),$ $p \rightarrow q,$ and $p.$ That is, it suffices to prove

$$p \rightarrow (q \rightarrow r), \; p \rightarrow q, \; p \;\vdash \; r$$

(1) $\;\;\;p \rightarrow q$

(2) $\;\;\;$(line 1) $\rightarrow [\;(q \rightarrow r) \rightarrow (p \rightarrow r)\;]$

(3) $\;\;\;(q \rightarrow r) \rightarrow (p \rightarrow r)$

(4) $\;\;\;p \rightarrow (q \rightarrow r)$

(5) $\;\;\;p$

(6) $\;\;\;q \rightarrow r$

(7) $\;\;\;p \rightarrow r$

(8) $\;\;\;r$

Reasons for the above steps

(1) $\;\;\;$assumption

(2) $\;\;\;$axiom 2

(3) $\;\;\;$MP (lines 1, 2)

(4) $\;\;\;$assumption

(5) $\;\;\;$assumption

(6) $\;\;\;$MP (lines 5, 4)

(7) $\;\;\;$MP (lines 6, 3)

(8) $\;\;\;$MP (lines 5, 7)

In trying to prove the Deduction Theorem for this logical system (i.e. $\Gamma, \;p \vdash q$ implies $\Gamma \vdash p \rightarrow q$), I simply followed the standard proof (which makes use of axiom 1 and the wff we originally wanted to prove), and noted that the standard proof only requires us to make use of the following 3 results:

1. If $q$ is an axiom or a member of $\Gamma$, then for any wff $p$ we can prove $p \rightarrow q$ in our logical system.

2. We can prove $p \rightarrow p$ in our logical system.

3. Given $p \rightarrow r$ and $p \rightarrow (r \rightarrow q)$, we can prove $p \rightarrow q$ in our logical system.

proof of 1: $\;\;\;$Apply MP to $q$ and $q \rightarrow (p \rightarrow q)$ (axiom 1).

proof of 2: $\;\;\;$Apply MP to $p \rightarrow (p \rightarrow p)$ (axiom 1) and axiom 3.

proof of 3: $\;\;\;$This is the difficult part. Below is a proof of what’s needed, namely

$$p \rightarrow r, \; p \rightarrow (r \rightarrow q) \;\vdash \; p \rightarrow q$$

(1) $\;\;\;p \rightarrow r$

(2) $\;\;\;p \rightarrow (r \rightarrow q)$

(3) $\;\;\;$(line 1) $\rightarrow \; [(r \rightarrow q) \rightarrow (p \rightarrow q)]$

(4) $\;\;\;(r \rightarrow q) \rightarrow (p \rightarrow q)$

(5) $\;\;\;$(line 2) $\;\;\rightarrow \;\; \{\;$(line 4)$\rightarrow [p \rightarrow (p \rightarrow q)] \; \}$

(6) $\;\;\;$(line 4) $\;\rightarrow \; [p \rightarrow (p \rightarrow q)]$

(7) $\;\;\;p \rightarrow (p \rightarrow q)$

(8) $\;\;\;[p \rightarrow (p \rightarrow q)] \; \rightarrow \; (p \rightarrow q)$

(9) $\;\;\;p \rightarrow q$

Reasons for the above steps

(1) $\;\;\;$assumption

(2) $\;\;\;$assumption

(3) $\;\;\;$axiom 2 ($r$ is $q$)

(4) $\;\;\;$MP (lines 1, 3)

(5) $\;\;\;$axiom 2 ($r$ is $p \rightarrow q$)

(6) $\;\;\;$MP (lines 2, 5)

(7) $\;\;\;$MP (lines 4, 6)

(8) $\;\;\;$axiom 3

(9) $\;\;\;$MP (lines 7, 8)

Here is how I discovered the above proof. Working backwards, I noticed that the conclusion of axiom 3 was what I wanted, so I made note of the fact that it would be enough to obtain $p \rightarrow (p \rightarrow q).$ Then I tried working forward. First, I applied axiom 2 followed by MP to the assumption $p \rightarrow r,$ using $q$ as the introduced suffix. (Since I already had $p$ and $r$ appearing, this seemed to be a natural way to get $q$ to appear.) Then I tried applying axiom 2 followed by MP to the assumption $p \rightarrow (r \rightarrow q).$ At some point (perhaps my 3rd attempt), I used $p \rightarrow q$ as the introduced suffix, motivated by the fact that this got line 4 to show up. After this, the proof immediately fell into place, since in line 5 the conclusion of the conclusion is $p \rightarrow (p \rightarrow q),$ which I had previouly noted was sufficient.

Incidentally, the logical system above is the same (in the sense of having the same set of provable wffs) as the logical system with the inference rule MP and the following two axioms: axiom 1 and the wff we originally wanted to prove. Each of these logical systems is also equal to the logical system with MP and Deductive Theorem as inference rules and no axioms (thus, one might call this system “DT Logic”). I think logicians call this the positive implicational fragment of intuitionistic propositional logic, but I like “DT Logic” better. Other axiomatizations of DT Logic can be found at the Wikipedia page “List of logic systems” under the category “Positive implicational calculus”.

For completeness, here’s a proof that DT Logic can be characterized by no axioms along with the inference rules MP and DT (and also the Rule of Assumptions, I suppose). It suffices to prove, in this no-axiom logical system, axiom 1 and the wff we were proving in this thread.

1. $\;\;\;p,\; q \vdash p\;$ implies $\;p \vdash q \rightarrow p\;$ implies $\;\vdash p \rightarrow (q \rightarrow p)$

2. $\;\;\;p \rightarrow (q \rightarrow r), \; p \rightarrow q, \; p \; \vdash \; r\;\;\;$ (MP, 3 times)

implies $\;p \rightarrow (q \rightarrow r), \; p \rightarrow q \; \vdash \; p \rightarrow r\;\;\;$ (DT)

implies $\;p \rightarrow (q \rightarrow r) \; \vdash \; (p \rightarrow q) \rightarrow (p \rightarrow r)\;\;\;$ (DT)

implies $\;\vdash \; [p \rightarrow (q \rightarrow r)] \;\; \rightarrow \;\; [(p \rightarrow q) \rightarrow (p \rightarrow r)] \;\;\;$ (DT)

-
Well done too. In combinator-logical notation, this amounts to using $\mathbf W(\mathbf A\;M\;(\mathbf A\;N))$ instead of $\mathbf S\;M\;N$ in the translation of an application -- which is indeed so simple that we ought to have been able to find it by hand. –  Henning Makholm Dec 27 '11 at 18:10
Incidentally, your "MP+DT" formulation is known (at least in computer-sciency contexts) as "natural deduction" for $\to$, and corresponds exactly, via the Curry-Howard isomorphism, to the simply typed lambda calculus. –  Henning Makholm Dec 27 '11 at 18:14
I only saw this now; great! –  joriki May 14 '12 at 7:55
Oh, I also really like the name "Deduction Theorem Logic" or what you might also call "Deduction Calculus" since it links it with the deduction metatheorem, better than "Positive Implication Calculus". The only difficultly here lies in that the deduction metatheorem might reasonably get argued as misnamed, since deduction is broader than what the deduction metatheorem implies. –  Doug Spoonwood Jun 14 '13 at 3:10
@Doug Spoonwood: Thanks for the comments. I haven't worked on logic in over 2 years, so I'm rather rusty on this stuff now, but I've made a note to myself about your comments for when I return to logic. Because I work full-time (non-academic work), I don't have a lot of time to devote to my math pursuits, so I generally tend to focus only on one or two topics at a time (for a few weeks to a few months), then move to something else when it starts getting stale to me. I've learned from experience it's better to move on, because once something gets stale, it's hard for me to continue it . . . –  Dave L. Renfro May 14 '14 at 13:49

For comparison, here is Joriki's solution in the combinator language we used in the comment thread between me and Zhen Lin: \begin{align} \mathbf X &= \mathbf A (\mathbf A \; \mathbf K \; \mathbf A) \mathbf W \\ \mathbf C &= \mathbf A \; \mathbf A (\mathbf A \; \mathbf X) \\ \mathbf B &= \mathbf C \; \mathbf A \\ \mathbf S &= \mathbf A (\mathbf B \; \mathbf B) \; (\mathbf A \; \mathbf C (\mathbf B \; \mathbf W)) \end{align} where $\mathbf X$ is an ad-hoc name for Joriki's "assertion" formula.

Zhen Lin's constuction for the final line $$\mathbf{S} = \mathbf{A A} ( \mathbf{A} ( \mathbf{B W} ) ( \mathbf{A A} ) )$$ is slightly more efficient than Joriki's because it contains only one $\mathbf B$ that needs to be unfolded. This yields the final term $$\mathbf S = \mathbf A\; \mathbf A\;(\mathbf A ( \mathbf A \; \mathbf A (\mathbf A \; (\mathbf A (\mathbf A \; \mathbf K \; \mathbf A) \mathbf W) ) \mathbf A \; \mathbf W) \; (\mathbf A\; \mathbf A))$$ which encodes a Hilbert-style proof with 15 fully substituted axiom instances and 14 modus ponens steps.

-
Thanks very much for this! An impressive demonstration of the conciseness of combinator logic :-) –  joriki Dec 21 '11 at 15:21

I found a 12 step proof (not counting the axioms) using the December 2007 version of Prover9 (it's free). Once the program started, it took my computer .19 seconds to find.

I'll write it up in Polish notation. Since we don't need to talk about negations for this proof, I'll re-write the formation rules for formulas as follows:

1. Lower case letters of the Latin alphabet are formulas.
2. If $\alpha$ and $\beta$ are formulas, then C$\alpha$$\beta is a formula. 3. Strings given by 1. and 2. are the only formulas in Polish notation for this answer. The notation Dx.y indicates that the formula to its left can get obtained using condensed detachment with formula x, or more likely one of it's substitution instances x', as the major premise and y, or one of it's substitution instances y', as the minor premise (I'm assuming that an output in the proof analysis from prooftrans like [hyper(2, a, 5, a, b, 5, a)] can get translated as D5.5). When using modus ponens, we have the major premise Cpq, and the minor premise as p. If working by hand, condensed detachment gives you an algorithmic way to find substitution instances of the antecedent of a potential major premise Cpq and a substitution instance of another formula p' such that their p' an p end up in one form (and we also end up with a variant q' or q also), and thus we can detach something (when such a unifier exists) without even having a clue as to what we'll detach beforehand. I'll use the numbering that the output of the proof from prooftrans that Prover9 gave me to reduce the probability that I'll make typographical errors. 3 CxCyx axiom 4 CCxCxyCxy axiom 5 CCxyCCyzCxz axiom 10 CCCCxyCzyuCCzxu D5.5 13 CCCxyzCyz D5.3 51 CCCxyxCCxyy D10.4 241 CxCCxyy D13.51 265 CCCCxyyzCxz D5.241 912 CCxCyzCyCxz D10.265 925 CCxyCCzxCzy D265.10 (also D.912.5, not mentioned/found by the program) 1809 CCxCyCyzCxCyz D925.4 17647 CCxyCCyCxzCxz D10.1809 20866 CCxCyzCCyxCyz D912.17647 21135 CCxyCCxCyzCxz D10.20866 21329 CCxCyzCCxyCxz D912.21135  So, the reason I can actually cite condensed detachment in the proof-analysis comes as that if we have modus ponens and uniform substitution, then condensed detachment is a derivable rule of inference. That said, I think it lacks a certain ease of comprehensibility, so I'll write up a proof which shows the substitutions in the proof analysis. The proof analysis will come before the derived formula. The notation x/y indicates that formula x gets substituted with formula y. The numeral that refers to the major premise gets listed on the left of the proof analysis. It gets separated by a "*" from the minor premise. The minor premise always has a "C" symbol before its numeral, and the raised line "-" after it followed by the numeral which refers to the thesis which we'll detach (we're finding the theses we'll detach as we go). I won't "normalize", or put variables in a certain order until the last step of the proof, because I find the substitutions easier to specify if I delay such a "normalization". Among other things, this method of proof analysis invented by Lukasiewicz indicates how the beginning student might easily expand everything if desired to write out the formulas with their substitution instances (it indicates that only theorems actually get used when performing a detachment), and also I think it indicates how everything can get thought of as one step... which at least seems to suggest condensed detachment. Let's begin: 3 CpCqp axiom 4 CCpCpqCpq axiom 5 CCpqCCqrCpr axiom  5 p/Cpq, q/CCqrCpr, r/s* C5-10  10 CCCCqrCprsCCpqs  5 q/Cqp, * C3-13  13 CCCqprCpr  10 p/Crq, r/q, s/CCrqq, q/r * C4 p/Crq-51  51 CCCrqrCCrqq  13 q/Crq, p/r, r/CCrqq * C13-241  241 CrCCrqq  5 p/r, q/CCrqq, r/p * C241-265  265 CCCCrqqpCrp  10 q/Crq, r/q, s/CrCpq * C265 p/Cpq-912  912 CCpCrqCrCpq  912 p/Cpq, r/Cqr, q/Cpr * C5-925  925 CCqrCCpqCpr  925 q/CpCpq, r/Cpq, p/r * C4-1809  1809 CCrCpCpqCrCpq  10 r/Cpq, q/r, s/CCrCpqCpq * C1809 r/CrCpq-17647  17647 CCprCCrCpqCpq  912 p/Cpq, r/CrCpq, q/Cpq * C17647-20866  20866 CCrCpqCCprCpq  10 r/q, q/r, s/CCpCrqCpq * C20866 r/Crq-21135  21135 CCprCCpCrqCpq  912 p/Cpr, r/CpCrq, q/Cpq * C21135-21329  21329 CCpCrqCCprCpq Now since p is the first variable in formula 21329, r the second variable, and q the third variable, and our usual sequence of variables goes (p, q, r, ...) having q as the second variable, and r as the third, in 21329 we simply r/q, q/r and obtain CCpCqrCCpqCpr as desired. - Using Dave L. Renfro's excellent derivation of the rule {Cpq, CpCqr} \vdash Cpr (with "p", "q", and "r" standing for metavariables in this sentence, but not elsewhere) we can turn a natural deduction proof into an axiomatic proof basically as follows. His proof tells us that to move from {\gamma, \alpha} \vdash \beta to \gamma \vdash C\alpha$$\beta$, where we had C$\phi$$\psi and \phi previously in the deduction, deducing \psi with \alpha as the hypothesis we want to discharge, we need C\alpha$$\phi$ and C$\alpha$C$\phi$$\psi. We'll get those initially since we have C\alpha$$\alpha$, and every step before detachment gets used consists of an axiom or assumption, both of which I'll denote as $\zeta$. Since we have CpCqp, we can obtain C$\alpha$$\zeta in a single detachment (hence I like to call CpCqp "recursive variable prefixing"). Then we apply CCpqCCqrCpr to both 1. C\alpha$$\phi$ and 2. C$\alpha$C$\phi$$\psi successively. The second formula obtained this way becomes the major premise (or some substitution instance thereof) and the first formula obtained this way becomes the minor premise (or some substitution instance thereof). We detach another formula, and let it become the minor premise. Then we use contraction "CCpCpqCpq" as the major premise, and then we'll extract C\alpha$$\psi$ in that step.

The variables {a, ..., o} happen in one alphabet and substitutions can get made for them. The variables {p, ..., z} happen in another and substitutions cannot get made for them, unless we have NO hypotheses or assumptions in place, only axioms. I'll refer to the first axiom CpCqp as "RVP" (short for "recursive variable prefixing"), the second axiom CCpCpqCpq as "CON" (short for "contraction") and the third axiom as HS (short for "hypothetical syllogism).

hypothesis  1 !  CpCqr
hypothesis  2 !@  Cpq
hypothesis  3 !@# p
D2.3        4 !@# q
D1.3        5 !@# Cqr
D5.4        6 !@# r


hypothesis  1 ! CpCqr  this is C3-5
hypothesis  2 !@ Cpq  this is C3-4
D[HS].1     3 !@ CCCqraCpa
D[HS].2     4 !@ CCqaCpa
D3.4        5 !@ CpCpr
D[CON].5    6 !@ Cpr ... C3-6


hypothesis  1 ! CpCqr
D[HS].1     2 ! CCCqraCpa
D[RVP].2    3 ! CaCCCqrbCpb ...  C2-3
HS          4 ! CCabCCbcCac ...  C2-4
D[HS].3     5 ! CCCCCqraCpabCcb
D5.6        7 ! CaCCbqCpCbr
D[CON].7    8 ! CCaqCpCar ... C2-5
D[RVP].CON  9 ! CaCCbCbcCbc ... C2-CON
D[HS].9    10 ! CCCCaCabCabcCdc
D[HS].8    11 ! CCCpCarbCCaqb
D10.11     12 ! CaCCpqCpr
D[CON].12  13 ! CCpqCpr


And now we'll write an axiomatic proof:

axiom    1 CpCqp
axiom    2 CCpqCCqrCpr ... C1-2
axiom    3 CCpCpqCpq
D3.1     4 Cpp ... C1-1
D1.1     5 CpCqCrq ... C1-RVP
D2.5     6 CCCpCqprCsr
D2.2     7 CCCCpqCrqsCCrps
D6.7     8 CpCCqrCsCCrtCqt
D3.8     9 CCpqCrCCqsCps ... C1-3
D1.2    10 CpCCqrCCrsCqs ... C1-4 ... C1-HS
D2.9    11 CCCpCCqrCsrtCCsqt
D2.10   12 CCCCpqCCqrCprsCts
D12.11  13 CpCCqrCCCCrsCqstCut
D3.13   14 CCpqCCCCqrCprsCts ... C1-5
D12.12  15 CpCqCCCCrsCtsuCCtru
D3.15   16 CpCCCCqrCsrtCCsqt ... C1-6
D2.14   17 CCCCCCpqCrqsCtsuCCrpu
D2.16   18 CCCCCCpqCrqsCCrpstCut
D17.18  19 CCpCqrCsCtCCuqCpCur
D3.19   20 CCpCqrCsCCtqCpCtr ... C1-7
D3.20   21 CCpCqrCCsqCpCsr ... C1-8 this is also D7.7


break...

D1.3    22 CpCCqCqrCqr
D1.22   23 CpCqCCrCrsCrs ... C1-9
D2.23   24 CCCpCCqCqrCqrsCts
D12.24  25 CpCqCCCCrCrsCrstCut
D3.25   26 CpCCCCqCqrCqrsCts ... C1-10
D2.21   27 CCCCpqCrCpstCCrCqst
D12.27  28 CpCCqCrsCCCqCtsuCCtru
D3.28   29 CCpCqrCCCpCsrtCCsqt ... C1-11
D2.26   30 CCCCCCpCpqCpqrCsrtCut
D2.29   31 CCCCCpCqrsCCqtsuCCpCtru
D30.31  32 CpCCqCrsCtCCqrCqs
D3.32   33 CCpCqrCsCCpqCpr ... C1-12
D3.33   34 CCpCqrCCpqCpr

-
One one can but marvel at your insistence in writing things in a way that is essentially opaque to anyone else by design. –  Mariano Suárez-Alvarez May 11 '14 at 3:29
@MarianoSuárez-Alvarez Um... do you really want to see what "CCCCCCpqCrqsCtsuCCrpu" or "CCCCCpCqrsCCqtsuCCpCtru" look like in infix notation? Also, let's look at D7.7, that is D[CCCCpqCrqsCCrps].[CCCCpqCrqsCCrps] here and suppose we actually wanted to carry out the substitutions by hand. We would have CCCCCqrCsrCpCsrCCsqCpCsrCCpCqrCCsqCpCsr as the major premise. Would you really want to see CCCCCqrCsrCpCsrCCsqCpCsrCCpCqrCCsqCpCsr in infix notation? –  Doug Spoonwood May 11 '14 at 23:25

I put the 1st three axioms into Prover9's assumptions along with a rule for condensed detachment, and selected "breadth-first", meaning that I'd try for a level-saturation approach. In 1.31 seconds, Prover9 threw back to me the following 8 step level 5 proof (alright, it has parentheses in it, but this will suffice).

            3 CxCyx                      K [level 0]

4 CCxyCCyzCxz                A [level 0]

5 CCxCxyCxy                  W [level 0]

D4.4        8 CCCCxyCzyuCCzxu           AA [level 1]

D4.5       11 CCCxyzCCxCxyz             AW [level 1]

D3.5       12 CxCCyCyzCyz               KW [level 1]

D8.8       17 CCxCyzCCuyCxCuz       AA(AA) [level 2]

D8.11      30 CCxyCCyCyzCxz         AA(AW) [level 2]

D17.12     57 CCxCyCyzCuCxCyz   AA((AA)(KW)) [level 3]

D30.17    250 CCCCxyCzCxuCCCxyCzCxuwCCzCyuw AA(AW)(AA(AA)(KW)) [level 4]

D250.57 10252 CCxCyzCCxyCxz AA(AW)(AA(AA)(KW))(AA((AA)KW))) [level 5]


Interestingly enough 30 CCxyCCyCyzCxz along with K or equivalently CxCyx suffices as a 2-axiom basis to prove S or equivalently CCxCyzCCxyCxz.

To follow this proof a little better...

4 C C x   y CCyzCxz
|   |
--- -------
4   CCxy CCyzCxz


Since "z" doesn't appear on the left hand side of 4, we can change it to a variable not appearing anywhere else in 4. So, if we made the substitutions suggested by this diagram we might infer CCCCyzCxzuCCxyu, which upon re-lettering making "x" into the first variable, "y" into the second, ..., "u" into the fourth, "w" into the fifth, v5 into the sixth, v6 into the seventh, etc. matches 8 above.

4 C C  x    y CCyzCxz
|    |
----- ---
5   C CxCxy Cxy


So, we can infer CCCxyzCCxCxyz.

3 C x C y x
|
---------
5  CCxCxyCxy


We just change "y" in 3 to x, "x" in 5 to "y", and "y" in 5 to "z" and we obtain CxCCyCyzCyz.

8 C CCC x    y  Czy u CCzxu
8 C CCC a    b  Ccb d CCcad
|    |  --- |
--- --- |   -----
8   CCC Cxy Czy u   CCzxu


So the diagram suggests that "a" gets substituted with Cxy, or equivalently a/Cxy, b/Czy, u/Ccb, d/CCzxu. But, that's not correct since substitutions have to come as uniform. "x" and "y" don't appear on the left hand side of any "/". So, a/Cxy is correct. "z" and "y" don't appear anywhere on the left-hand side of "/", so b/Czy is correct. Since "b" does appear on the left-side side of "/" we'll need to have u/CcCzy. And also, d/CCzxCcCzy. Thus, we can detach CCcCxyCCzxCcCzy.... which upon re-lettering becomes CCxCyzCCuyCxCuz.

8  CCCC x y Czy u CCzxu
8  CCCC a b Ccb d CCcad
| | --- |
| | |  -------
11  CCC x y z  CCxCxyz


So, we can write a/x, b/y, z/Ccb, d/CCxCxyz. Then we have z/Ccy, d/CCxCxyCcy. Thus, we can detach CCcxCCxCxyCcy or equivalently CCxyCCyCyzCxz.

17 C C x C   y   z CCuyCxCuz
|     |   |
|   ----- ---
12   C x C CyCyz Cyz


Thus, we can get CCuCyCyzCxCuCyz or CCxCyCyzCuCxCyz.

30 C C  x     y      CCyCyzCxz
|     |
----- ---------
17   C CxCyz CCuyCxCuz


Thus, we can infer CCCCuyCxCuzCCCuyCxCuzaCCxCyza or equivalently CCCCxyCzCxuCCCxyCzCxuwCCzCyuw.

250 CCC Cxy C z C x u C CCxyCzCxu w CCzCyuw
250 CCC Cab C c C a d C CCabCcCad e CCcCbde
---   |   | |   --------- |
|     |   | |   |         -----
57   CC x   C y C y z C u         CxCyz


So, x/Cab, c/y, a/y, d/z, u/CCabCcCad, e/CxCyz. Correcting that we have x/Cyb, c/y, a/y, d/z, u/CCybCyCyz, e/CCybCyz, and thus detach CCyCbzCCybCyz or equivalently CCxCyzCCxyCxz.

The level of a formula in a condensed detachment proof is one level greater than the greatest level of its parents. All axioms have level 0. A level-saturation approach means that all formulas of level 1 get deduced first, then all formulas of level 2, then those of level 3, and so on. A level saturation approach can find short proofs. It won't necessarily find the shortest proof, and it's also not necessarily feasible given a time constraint, the amount of memory available on the computer (sometime a formula of level k is MUCH longer than a formula of level k+1 or k+6), and the speed with which computations get done.

-