Proving $A\to (¬A \to B)$ with Łukasiewicz's axioms and modus ponens?

Question

I am trying to answer the following exercise from Hao's Fundamentals of Logic and Computation: With Practical Automated Reasoning and Verification.

Using only modus ponens and the following axioms:

I'm stuck for some days on it, I've even made a small program in Mathematica to help me with the substitutions but got nothing. Can you help me?

Answer 1

Hou gives the rule of transitivity of implication (TI) on p. 17, but does not give the theorem $A\rightarrow\neg\neg A$. So, I copy the proof of this theorem from my answer and paste it here (lines 1—23) and the rest follows:

1. $(\neg\neg\neg\neg\neg A\rightarrow\neg\neg\neg A)\rightarrow (\neg\neg A\rightarrow\neg\neg\neg\neg A)\qquad\text{Ax 3}$

2. $\big((\neg\neg\neg\neg\neg A\rightarrow\neg\neg\neg A)\rightarrow (\neg\neg A\rightarrow\neg\neg\neg\neg A)\big)\rightarrow\Big(\neg\neg\neg A\rightarrow\big((\neg\neg\neg\neg\neg A\rightarrow\neg\neg\neg A)\rightarrow(\neg\neg A\rightarrow\neg\neg\neg\neg A)\big)\Big)\qquad\text{Ax 1}$

3. $\neg\neg\neg A\rightarrow\big((\neg\neg\neg\neg\neg A\rightarrow\neg\neg\neg A)\rightarrow(\neg\neg A\rightarrow\neg\neg\neg\neg A)\big)\qquad\text{MP 1, 2}$

4. $\Big(\neg\neg\neg A\rightarrow\big((\neg\neg\neg\neg\neg A\rightarrow\neg\neg\neg A)\rightarrow(\neg\neg A\rightarrow\neg\neg\neg\neg A)\big)\Big)\rightarrow\Big(\big(\neg\neg\neg A\rightarrow(\neg\neg\neg\neg\neg A\rightarrow\neg\neg\neg A)\big)\rightarrow\big(\neg\neg\neg A\rightarrow(\neg\neg A\rightarrow\neg\neg\neg\neg A)\big)\Big)\qquad\text{Ax 2}$

5. $\big(\neg\neg\neg A\rightarrow(\neg\neg\neg\neg\neg A\rightarrow\neg\neg\neg A)\big)\rightarrow\big(\neg\neg\neg A\rightarrow(\neg\neg A\rightarrow\neg\neg\neg\neg A)\big)\qquad\text{MP 3, 4}$

6. $\neg\neg\neg A\rightarrow(\neg\neg\neg\neg\neg A\rightarrow\neg\neg\neg A)\qquad\text{Ax 1}$

7. $\neg\neg\neg A\rightarrow(\neg\neg A\rightarrow\neg\neg\neg\neg A)\qquad\text{MP 5, 6}$

8. $(\neg\neg A\rightarrow\neg\neg\neg\neg A)\rightarrow (\neg\neg\neg A\rightarrow\neg A)\qquad\text{Ax 3}$

9. $\Big((\neg\neg A\rightarrow\neg\neg\neg\neg A)\rightarrow (\neg\neg\neg A\rightarrow\neg A)\Big)\rightarrow\Big(\neg\neg\neg A\rightarrow\big((\neg\neg A\rightarrow\neg\neg\neg\neg A)\rightarrow (\neg\neg\neg A\rightarrow\neg A)\big)\Big)\qquad\text{Ax 1}$

10. $\neg\neg\neg A\rightarrow\big((\neg\neg A\rightarrow\neg\neg\neg\neg A)\rightarrow (\neg\neg\neg A\rightarrow\neg A)\big)\qquad\text{MP 8, 9}$

11. $\Big(\neg\neg\neg A\rightarrow\big((\neg\neg A\rightarrow\neg\neg\neg\neg A)\rightarrow (\neg\neg\neg A\rightarrow\neg A)\big)\Big)\rightarrow\Big(\big(\neg\neg\neg A\rightarrow(\neg\neg A\rightarrow\neg\neg\neg\neg A)\big)\rightarrow\big(\neg\neg\neg A\rightarrow (\neg\neg\neg A\rightarrow\neg A)\big)\Big)\qquad\text{Ax 2}$

12. $\big(\neg\neg\neg A\rightarrow(\neg\neg A\rightarrow\neg\neg\neg\neg A)\big)\rightarrow\big(\neg\neg\neg A\rightarrow (\neg\neg\neg A\rightarrow\neg A)\big)\qquad\text{MP 10, 11}$

13. $\neg\neg\neg A\rightarrow (\neg\neg\neg A\rightarrow\neg A)\qquad\text{MP 7, 12}$

14. $\big(\neg\neg\neg A\rightarrow (\neg\neg\neg A\rightarrow\neg A)\big)\rightarrow\big((\neg\neg\neg A\rightarrow\neg\neg\neg A)\rightarrow(\neg\neg\neg A\rightarrow\neg A)\big)\qquad\text{Ax 2}$

15. $(\neg\neg\neg A\rightarrow\neg\neg\neg A)\rightarrow(\neg\neg\neg A\rightarrow\neg A)\qquad\text{MP 13, 14}$

16. $\neg\neg\neg A\rightarrow\big((\neg\neg\neg A\rightarrow\neg\neg\neg A)\rightarrow\neg\neg\neg A\big)\qquad\text{Ax 1}$

17. $\Big(\neg\neg\neg A\rightarrow\big((\neg\neg\neg A\rightarrow\neg\neg\neg A)\rightarrow\neg\neg\neg A\big)\Big)\rightarrow\Big(\big(\neg\neg\neg A\rightarrow(\neg\neg\neg A\rightarrow\neg\neg\neg A)\big)\rightarrow\big(\neg\neg\neg A\rightarrow\neg\neg\neg A\big)\Big)\qquad\text{Ax 2}$

18. $\big(\neg\neg\neg A\rightarrow(\neg\neg\neg A\rightarrow\neg\neg\neg A)\big)\rightarrow\big(\neg\neg\neg A\rightarrow\neg\neg\neg A\big)\qquad\text{MP 16, 17}$

19. $\neg\neg\neg A\rightarrow(\neg\neg\neg A\rightarrow\neg\neg\neg A)\qquad\text{Ax 1}$

20. $(\neg\neg\neg A\rightarrow\neg\neg\neg A)\qquad\text{MP 18, 19}$

21. $(\neg\neg\neg A\rightarrow\neg A)\qquad\text{MP 15, 20}$

22. $(\neg\neg\neg A\rightarrow\neg A)\rightarrow (A\rightarrow\neg\neg A)\qquad\text{Ax 3}$

23. $A\rightarrow\neg\neg A\qquad\text{MP 21, 22}$

24. $\neg\neg A\rightarrow(\neg B\rightarrow\neg\neg A)\qquad\text{Ax 1}$

25. $(\neg B\rightarrow\neg\neg A)\rightarrow(\neg A\rightarrow B)\qquad\text{Ax 3}$

26. $\neg\neg A\rightarrow(\neg A\rightarrow B)\qquad\text{TI 24, 25}$

27. $A\rightarrow(\neg A\rightarrow B)\qquad\text{TI 23, 26}$

Answer 2

Name the first two axioms as follows: $$K: a → b → a,\quad S: (a → b → c) → (a → b) → a → c,$$ where we adopt the prevailing convention of of associating to the right, i.e. $a → b → c = a → (b → c)$. Name the third axiom $$Z: (¬a → ¬b) → b → a,$$ and for modus ponens, applied to $f: a → b$ and $g: a$, write $fg: b$. Adopt the prevailing convention of associating products to the left, i.e. $fgh = (fg)h$. As is well-known, and as you can verify, there is an equivalence of proofs given by the following: $$K f g = f,\quad S f g h = f h (g h).$$

Important lemmas can be stated as follows: $$\begin{align} I = S K K:& a → a,\\ B = S (K S) K:& (b → c) → (a → b) → a → c,\\ C = S (B B S) (K K):& (a → b → c) → b → a → c. \end{align}$$ The corresponding formulas, derivable from those above, are $$I f = f,\quad B f g h = f (g h),\quad C f g h = f h g.$$

The formulas are identical to those seen in Combinatory Logic and may be interpreted as a system of type templates (and proof conversion rules), e.g. where the type for the combinator $I$ is the template consisting of all types of the form $a → a$, and a type $a → b$, in general, denotes the type of all functions that take arguments of type $a$ and return arguments of type $b$. This is none other than the Curry-Howard Correspondence.

(That's why this question popped up in my feed, after I got through answering a bunch of combinator questions.)

One example of a proof derived by the η-rule (which corresponds to proof by discharge of hypothesis) is that since $S (K f) g h = K f h (g h) = f (g h) = B f g h$, then $S (K f) g = B f g$ and $S (K f) = B f$. I won't make direct use of that, other than to note a simplification of another reply given here.

As an example, the development of the proof for $B$ is given here: $$\begin{align} S:& (d → e → f) → (d → e) → d → f,\\ K:& g → d → g,\\ S:& (a → b → c) → (a → b) → a → c,\\ K S:& d → (a → b → c) → (a → b) → a → c,\\ S (K S):& (d → a → b → c) → d → (a → b) → a → c,\\ K:& d → a → d,\\ B = S (K S) K:& (b → c) → (a → b) → a → c,\\ \end{align}$$ where modus ponens is matched at the relevant points by the conditions $$ d = b → c,\quad e = a → b → c,\quad f = (a → b) → a → c,\quad g = e → f. $$

You can work out the development for the proofs of $I$ and $C$.

The (27 line) answer given in another reply corresponds to the term $$B (B Z K) (Z (S (S (K Z) (S (K Z) K)) I))$$ as you can determine, for yourself, by carefully reading the attributions in the proof and constructing the term based on them. Since $S (K Z) = B Z$ (up to η-equivalence), this can be just as well written as $$B V (Z (S (B Z V) I))$$ where $V = B Z K$.

Do we really need all that? What is the $V$ proof? $$\begin{align} B:& (d → e) → (c → d) → c → e,\\ Z:& (¬b → ¬a) → a → b,\\ B Z:& (c → ¬b → ¬a) → c → a → b,\\ K:& c → f → c,\\ B Z K:& ¬a → a → b,\\ \end{align}$$ where $$c = ¬a,\quad d = ¬b → ¬a,\quad e = a → b,\quad f = ¬b$$ ensures Modus Ponens matches up at the relevant points. Run $C$ on this - which is why I brought it up: $$\begin{align} C:& (d → a → b) → a → d → b,\\ B Z K:& ¬a → a → b,\\ C (B Z K):& a → ¬a → b, \end{align}$$ where $$d = ¬a.$$

If you want to simplify it, run it through the combinator formulae: $$C f = S (B B S) (K K) f = B B S f (K K f) = B (S f) K\quad (f = B Z K).$$ Thus, the proof is: $$B (S (B Z K)) K = S (K (S (S (K Z) K))) K.$$

Just to check, I ran them all through Combo, applying the extensionality axiom (i.e. the η-rule), and $$B (S (B Z K)) K,\quad S (K (S (S (K Z) K))) K,$$ both reduce to $C (B Z K)$.

If you want to see the proof in line-by-line form, the best recommendation is to develop the expression $B (S (B Z K)) K$, since you've already seen the proof for $B$ above, which you can treat as a lemma.

If you use $C$, the proof is the 7 lines that make up the construction of $C (B Z K)$. With $B$, it's 11 lines, and if using the pure $S-K-Z$ expression, it's 15 lines. It's always $2n - 1$ lines, where $n$ is the number of combinators involved.

Is there an extension of Curry-Howard that directly incorporates $Z$ as another combinator of some kind? Supposedly, you can integrate this in Lambda-Mu Calculus, but I have no experience with that (yet). It is closely and deeply intertwined with Continuation-Passing Semantics which is the gold standard for programming language semantics, and is also the semantics formalism that's used to integrate Functional Programming and Imperative Programming. It's probably why they finally got the courage to stick λ-terms from Lambda Calculus (the sibling of Combinatory Logic) in languages like C++ in the early 2010's.

Edit: Just for the sake of completeness, I lay out the proof with $C$ below: $$\begin{align} C:& (c → a → b) → a → c → b,\\ B:& (d → e) → (c → d) → c → e,\\ Z:& (¬b → ¬a) → a → b,\\ BZ:& (c → d) → c → e,\\ K:& c → f → c,\\ BZK:& c → e,\\ C(BZK):& a → c → b, \end{align}$$ where $$c = ¬a,\quad d = ¬b → ¬a,\quad e = a → b,\quad f = ¬b,$$ ensures that the applications of Modus Ponens match up.