# Equivalence of two very specific propositional calculi

Let $H$ and $L$ be two propositional calculi. $H$ has as inference rule modus ponens only, and three axiom schemes:

• P1: $A\rightarrow . B\rightarrow A$
• P2: $(A\rightarrow . B\rightarrow C)\rightarrow . A\rightarrow B\rightarrow . A\rightarrow C$
• P3: $\neg B\rightarrow\neg A\rightarrow . A\rightarrow B$

$L$ has as inference rule modus ponens only, and P1, P2 as axiom schemata and three additional axiom schemata:

• P4: $(A\rightarrow\neg A)\rightarrow\neg A$
• P5: $A\rightarrow . \neg A\rightarrow B$
• P6: $A\rightarrow B\rightarrow A\rightarrow A$

It's easy to show that:

• $\vdash_H (A\rightarrow\neg A)\rightarrow\neg A$
• $\vdash_H A\rightarrow . \neg A\rightarrow B$
• $\vdash_H A\rightarrow B\rightarrow A\rightarrow A$

How to show that:

• $\vdash_L \neg B\rightarrow\neg A\rightarrow . A\rightarrow B$?
-
What is the significance of the dot that is found scattered through these formulas? –  Harald Hanche-Olsen Apr 25 '13 at 22:14
'$\rightarrow .$' is an abbreviation that is expanded by replacing '$\rightarrow .$' by '$\rightarrow($' and matching the left parenthesis placed as far as possible to the right without going through a right parenthesis mated with a left parenthesis to the left of the occurrence of '$\rightarrow .$'. For example, P1 is '$(A\rightarrow (B\rightarrow A))$'. The outermost parentheses are dropped. –  Quique Ruiz Apr 26 '13 at 0:49
The dots go back to Principia, and -- very influentially -- Alonzo Church's Introduction to Mathematical Logic. –  Peter Smith Apr 26 '13 at 6:36
Ah, thanks for the history lesson. I think the modern approach is to let the arrow associate to the right, so that you can write $(A\to(B\to C))$ as $A\to B\to C$, while you cannot drop the parentheses in $(A\to B)\to C$. But this raises a new question: What is the meaning of P6? Three arrows, no dots, no parentheses. –  Harald Hanche-Olsen Apr 26 '13 at 8:25
Would you accept a formal (but most likely hard-to-read) proof from an automated theorem prover? –  Petr Pudlák Apr 27 '13 at 11:25

The left column is the axiom schema in your abbreviated notation. The right is the axiom in Prover9/OTTER notation, along with a predicate "P" which you can interpret as "$\vdash$". The following periods in the right hand column are part of Prover9's notation:

P1: A→.B→A                 P(C(x,C(y,x))).

P2: (A→.B→C)→.A→B→.A→C     P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))).

P4: (A→¬A)→¬A              P(C(C(x,N(x)),N(x))).

P5: A→.¬A→B                P(C(x,C(N(x),y))).

P6: A→B→A→A                P(C(C(C(x,y),x),x)).


You want to prove:

P3 ¬B→¬A→.A→B              P(C(C(N(x),N(y)),C(y,x))).


Prover9 is a resolution based theorem prover. This enables us to join

-P(C(x,y)) | -P(x) | P(y).

as an axiom to produce results just like condensed detachment does. "-" is negation, and "|" means "or"). "C" and "N" get interpreted as non-specified functions, and I believe their arity gets determined by the symbols around them. It took Prover9 247.34 seconds to find the first form of the proof here (I've tried to give you a more easily read form). The only supplementary input using the "formula(hints)" command I gave it was the axioms (other than the "or-not" axiom) and the targeted theorem. The notation [2,3,4]. The first formula is always formula 2 here "-P(C(x,y)) | -P(x) | P(y).", since it's the only formula by which another formula can get inferred by hyperresolution. The second formula has form P(C(x,y)). The third formula has form P(x). The formulas you see on the lefthand side, such as P(C(x,C(C(y,N(y)),N(y)))). and P(C(x,C(y,C(N(x),z)))). in the following have form P(y).

% -------- Comments from original proof --------

% Proof 1 at 0.01 (+ 0.00) seconds.

% Length of proof is 36.

% Level of proof is 11.

% Maximum clause weight is 24.

% Given clauses 33.

1 P(C(C(N(x),N(y)),C(y,x))) # label(non_clause) # label(goal). [].

2 -P(C(x,y)) | -P(x) | P(y). [].

3 P(C(x,C(y,x))). [].

4 P(C(C(x,C(y,z)),C(C(x,y),C(x,z)))). [].

5 P(C(C(x,N(x)),N(x))). [].

6 P(C(x,C(N(x),y))). [].

7 P(C(C(C(x,y),x),x)). [].

8 -P(C(C(N(c3),N(c4)),C(c4,c3))). 1.

9 P(C(x,C(y,C(z,y)))). [2,3,3].

10 P(C(C(C(x,C(y,z)),C(x,y)),C(C(x,C(y,z)),C(x,z)))). [2,4,4].

11 P(C(x,C(C(y,C(z,u)),C(C(y,z),C(y,u))))). [2,3,4].

12 P(C(x,C(C(y,N(y)),N(y)))). [2,3,5].

13 P(C(x,C(C(C(y,z),y),y))). [2,3,7].

14 P(C(C(x,y),C(x,C(z,y)))). [2,4,9].

15 P(C(x,C(y,C(z,C(u,z))))). [2,3,9].

16 P(C(C(x,C(C(y,z),y)),C(x,y))). [2,4,13].

17 P(C(x,C(y,C(N(x),z)))). [2,14,6].

18 P(C(C(x,C(y,z)),C(u,C(C(x,y),C(x,z))))). [2,14,4].

19 P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))). [2,10,15].

20 P(C(C(C(x,N(x)),C(N(x),y)),C(C(x,N(x)),y))). [2,10,12].

21 P(C(C(C(x,C(y,z)),C(C(C(x,y),C(x,z)),u)),C(C(x,C(y,z)),u))). [2,10,11].

22 P(C(C(x,C(C(y,x),z)),C(x,z))). [2,10,9].

23 P(C(C(x,y),C(C(z,x),C(z,y)))). [2,22,11].

24 P(C(C(C(x,y),z),C(y,z))). [2,19,23].

25 P(C(x,C(C(C(y,z),u),C(z,u)))). [2,3,24].

26 P(C(C(C(x,N(x)),C(N(x),x)),x)). [2,16,20].

27 P(C(C(N(x),x),x)). [2,24,26].

28 P(C(x,C(C(N(y),y),y))). [2,3,27].

29 P(C(x,C(C(y,C(N(z),z)),C(y,z)))). [2,18,28].

30 P(C(C(N(x),C(y,x)),C(C(N(x),y),x))). [2,21,29].

31 P(C(C(x,C(y,z)),C(y,C(x,z)))). [2,21,25].

32 P(C(C(x,y),C(C(y,z),C(x,z)))). [2,31,23].

33 P(C(C(C(x,C(N(y),z)),u),C(y,u))). [2,32,17].

34 P(C(x,C(C(N(y),N(x)),y))). [2,33,30].

35 P(C(C(N(x),N(y)),C(y,x))) # label(non_clause) # label(goal). [2,31,34].

36 \$F. [35,8].

-