**Competition** Shortest Proof of Lukasiewicz's 13 Letter Axiom for Implicational Calculus from Tarski-Bernays

Question

Spurred on by Willemien's competition, I thought I'd post my own.

In 1948 a paper by Jan Lukasiewicz got published that established a 13 letter formula as (one of?) the shortest single axioms, under detachment, for the pure implicational calculus of propositions (Lukasiewicz had claimed the following as a single axiom as far back as 1937, but no proof got published until 1948).

L. CCCpqrCCrpCsp       (((p→q)→r)→((r→p)→(s→p)))

The original formulation of implicational propositional calculus by Tarski and Bernays had three axioms along with detachment.

1. CCpqCCqrCpr      ((p→q)→((q→r)→(p→r)))
2. CpCqp            (p→(q→p))
3. CCCpqpp          (((p→q)→p)→p)

Suppose that we start with 1., 2., 3. and want to deduce L. and have two rules of inference 1. condensed detachment, and 2, condensed syllogism, as follows:

Condensed detachment allows us to infer from C$\alpha$$\beta$ and $\alpha$' to $\beta$", where $\alpha$' and $\alpha$ have a most general unifier, and any variables not affected by the unification of $\alpha$' and $\alpha$ get changed to variables distinct from other variables. By a unifier, I mean to say that there exists a common form obtainable from $\alpha$ and also from $\alpha$' just by making substitutions in $\alpha$ and $\alpha$', which is unique up to re-lettering of variables. Let us denote an application of condensed detachment with x as C$\alpha$$\beta$, and y as $\alpha$' by "Dx.y".

Condensed syllogism, similarly, allows us to infer from C$\alpha$$\beta$ and C$\beta$'$\gamma$ to C$\alpha$"$\gamma$", where $\beta$ and $\beta$' have a most general unifier and any variables not affected by the unification of $\beta$' and $\beta$ get changed to variables distinct from other variables. Again, I mean to say that there exists a common form obtainable from $\beta$ and $\beta$' by substitution alone (substitutions can get made in both $\beta$ and in $\beta$') which is unique to re-lettering of variables. Let us denote an application of condensed syllogism with x as C$\alpha$$\beta$, and y as C$\beta$'$\gamma$ by "Sx.y".

For condensed detachment we can draw something like this,

1 C C p q CCqrCpr
    | | |
    | | ---
2   C p Cqp

Thus, D1.2 yields 4 CCCqprCpr.

4 C CC q   p r Cpr
    || |   | |
    || --- | |
3   CC Cpq p p

So, D4.3 yields 5 Cpp.

For condensed syllogism we can draw something like this:

2 Cp C q   p
     | |   |
     | --- |
3  C C Cpq p p

So, S2.3 yields Cpp.

Using just the rules of condensed syllogism and condensed detachment, what is the shortest proof in terms of number of steps of CCCpqrCCrpCsp?

Please annotate your proofs in the following fashion (though infix notation is fine):

     1 CCpqCCqrCpr
     2 CpCqp
     3 CCCpqpp
S3.2 4 CCCpqpCqp
S4.1 5 CCCqpqCCprCqr
D1.4 6 CCCqprCCCpqpr.

Competition rules:

I will give the person who comes with the shortest proof a reward of 200 (unmarked) reputation points. I can only add a bounty in a couple of days from now, but you can post your answer now.

The length of a proof is measured by the number of numbered lines in the proof (see the proof above as an example, the first formula is at line number 1, and every proof line gets counted equally no matter if you used condensed detachment or condensed syllogism)

Tiebreaker rule : If there is more than one person with the shortest answer the reward goes to the poster with the most instances of condensed detachment used. If that does not resolve any ties, then the reward will go to the poster who posted the proof with the shortest symbol count (excluding parentheses) of the longest formula in the proof.

The answer must have the form of a complete axiomatic deduction as the proof of CCCqprCCCpqpr above.

You may give more than one answer, answers in more than one proof method etc, but do post them as seperate answers, and be aware that only the proof that uses the axiomatic method with the rules of condensed detachment and/or condensed syllogism above is competing, and other participants can peek at your answers.

Please don't delete your answers.

Re-lettering of variables will get ignored, by which I mean to say that if you post a proof of CCCabcCCcaCda that will get counted as a proof in the same way that a proof of CCCpqrCCrpCsp will get counted, and the like.

You may use a theorem prover, but please put your answer into standard Polish notation or standard infix notation (reverse Polish notation with "C" as the connective I'll accept also).

Best of success, and may the best one win.

Answer 1

To orient ourselves, we first note that Axiom $1$ can be specialized to

((p→q)→r)→((r→p)→((p→q)→p)),

which is quite close to what we want to prove. Moreover, the proposition (p→q)→p, if true, could be used to infer p (by detachment using Axiom $3$) and then s→p (by detachment using Axiom $2$). The idea we need to justify is that these inference steps can be carried out inside a hypothesis. It will suffice to show that

(a→b)→((c→a)→(c→b))

in general. Here is one path to that theorem (discovered with an automated search):

      1  (p→q)→((q→r)→(p→r))
      2  p→(q→p)
      3  ((p→q)→p)→p
S2.1  4  a→((a→b)→(c→b))
S1.3  5  (a→(a→b))→(a→b)
S4.5  6  a→((a→b)→b)
D1.1  7  (((a→b)→(c→b))→d)→((c→a)→d)
S6.7  8  (a→b)→((c→a)→(c→b))

We can now formalize the informal reasoning above to complete the proof of the Lukasiewicz axiom:

S3.2    9  ((a→b)→a)→(c→a)
D8.9   10  (a→((b→c)→b))→(a→(d→b))
D8.10  11  (a→(b→((c→d)→c)))→(a→(b→(e→c)))
D11.1  12  ((p→q)→r)→((r→p)→(s→p))

(Note that theorems $4$ through $7$ were only used to derive theorem $8$.) The proof uses condensed syllogism five times and condensed detachment four times.

Answer 2

Using OTTER [1], I've found a 7 step, level 4 proof.

axiom       4 CxCyx                           level 0

axiom       5 CCxyCCyzCxz                     0

axiom       6 CCCxyxx                         0

D4.4        8 CxCyCzy                         1

S5.5        9 CCxyCCCxzuCCyzu                 1

D5.8       31 CCCxCyxzCuz                     2

D9.6       37 CCCCCxyxzuCCxzu                 2

S31.6     115 CCCxCyxzz                       3

S9.37     144 CCCxyzCCxuCCzxu                 3

S144.115  585 CCCxyzCCzxCux                   4

Here's the input file for OTTER:

set(hyper_res).
set(sos_queue).
assign(max_weight, 6).
assign(max_distinct_vars,5).
assign(max_proofs, 5).
clear(print_kept).
clear(back_sub).
assign(max_mem,10000000).
set(input_sos_first).
set(back_sub).
set(order_history).
assign(report, 3600).
% set(ancestor_subsume).
clear(print_back_sub).




weight_list(pick_and_purge).
weight(P(C(x,C(y,x))),2).
weight(C(x,C(y,x)),1).
weight(C(y,x),1).
weight(P(C(C(x,y),C(C(y,z),C(x,z)))),2).
weight(P(C(C(C(x,y),x),x)),2).
weight(P(C(C(C(x,y),z),C(C(z,x),C(u,x)))),2).
weight(C(C(x,y),C(C(y,z),C(x,z))),1).
weight(C(x,y),1).
weight(C(C(y,z),C(x,z)),1).
weight(C(y,z),1).
weight(C(x,z),1).
weight(C(C(C(x,y),x),x),1).
weight(C(C(x,y),x),1).
weight(C(C(C(x,y),z),C(C(z,x),C(u,x))),1).
weight(C(C(x,y),z),1).
weight(C(C(z,x),C(u,x)),1).
weight(C(z,x),1).
weight(C(u,x),1).
end_of_list.

list(usable).
-P(C(x,y))| -P(x)|P(y).
-P(C(C(C(p,q),r),C(C(r,p),C(s,p)))).
-P(C(x,y))| -P(C(y,z)) | P(C(x,z)).
end_of_list.

list(sos).
P(C(x,C(y,x))).
P(C(C(x,y),C(C(y,z),C(x,z)))).
P(C(C(C(x,y),x),x)).
end_of_list.

[1]- W. McCune, "OTTER and Mace2", http://www.mcs.anl.gov/research/projects/AR/otter/, 1988-2014.