# 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 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 at 0:49
The dots go back to Principia, and -- very influentially -- Alonzo Church's Introduction to Mathematical Logic. –  Peter Smith Apr 26 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 at 8:25
P6 is $(((A \to B) \to A) \to A)$, Pierce's Law. –  Joshua Taylor Apr 26 at 14:50