Deducing $((\neg a \to \neg b) \to ((\neg a \to b) \to b)))$ from axioms

Question

I have seen many questions here, using a different set of axioms than mine.

Here is mine :

$$1) (a \to (b \to a))$$ $$2) ((a \to (b \to c)) \to ((a \to b) \to (a \to c)))$$ $$3) ((\neg b \to \neg a) \to (a \to b))$$

Is it possible to deduce the following from these: $((a \to b) \to ((\neg a \to b) \to b))$.

I couldn't find a proof myself or online.

Thank you very much!!!

Answer 1

It helps to know:

• Two logical expressions are equivalent iff they have the same truth table
• $(a \rightarrow b) \leftrightarrow (\neg a \vee b) $ (One can proof that using the truth table)
• $(a \rightarrow b) \leftrightarrow (\neg b \rightarrow \neg a) $ (One can proof that using the truth table)
• $(a \vee \neg a) =1$ (Tautology)
• $\neg \neg a = a$ (Double negation)
• $1$ is the neutral element of the logical conjuction: $1\wedge a = a$

---

Here is my approach to deduce the given expression from elementary propositions:

Let $a$ and $b$ be two propositions, with $$a \rightarrow b$$ $$ \leftrightarrow \neg a \vee b$$ $$\leftrightarrow (\neg a \wedge b)\vee(\neg a \vee b)$$ $$\leftrightarrow (\neg (a \vee \neg b))\vee(\neg a \vee b)$$ $$\leftrightarrow (a \vee \neg b)\rightarrow (\neg a \vee b)$$ $$\leftrightarrow (a \vee \neg b)\rightarrow (b \vee \neg a)$$ $$\leftrightarrow (a \vee \neg b)\rightarrow (b \vee \neg a) \wedge 1 $$ $$\leftrightarrow (a \vee \neg b)\rightarrow (b \vee \neg a) \wedge (b \vee \neg b) $$ $$\leftrightarrow (a \vee \neg b)\rightarrow b \vee( \neg a \wedge \neg b) $$ $$\leftrightarrow (a \vee \neg b)\rightarrow b \vee \neg(a \vee b) $$ $$\leftrightarrow (a \vee \neg b)\rightarrow b \vee \neg(\neg \neg a \vee b) $$ $$\leftrightarrow (a \vee \neg b)\rightarrow b \vee \neg( \neg a \rightarrow b) $$ $$\leftrightarrow (a \vee \neg b)\rightarrow \neg( \neg a \rightarrow b) \vee b $$ $$\leftrightarrow (a \vee \neg b)\rightarrow (( \neg a \rightarrow b) \rightarrow b) $$ $$\leftrightarrow (\neg b \vee a)\rightarrow (( \neg a \rightarrow b) \rightarrow b) $$ $$\leftrightarrow (b \rightarrow a)\rightarrow (( \neg a \rightarrow b) \rightarrow b) $$ $$\leftrightarrow (\neg a \rightarrow \neg b)\rightarrow (( \neg a \rightarrow b) \rightarrow b)$$

Answer 2

Undoubtedly a shorter proof exists, but here's a Prover9 proof:

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

% Proof 1 at 208.84 (+ 24.69) seconds.

% Length of proof is 53.

% Level of proof is 20.

% Maximum clause weight is 24.

% Given clauses 9783.

1 P((x -> y) -> ((-x -> y) -> y)) # label(non_clause) # label(goal). [goal].

2 -P(x -> y) | -P(x) | P(y). [assumption].

3 P(x -> (y -> x)). [assumption].

4 P((x -> (y -> z)) -> ((x -> y) -> (x -> z))). [assumption].

5 P((-x -> -y) -> (y -> x)). [assumption].

6 -P((c1 -> c2) -> ((-c1 -> c2) -> c2)). [deny(1)].

7 P(x -> (y -> (z -> y))). [hyper(2,a,3,a,b,3,a)].

8 P(((x -> (y -> z)) -> (x -> y)) -> ((x -> (y -> z)) -> (x -> z))). [hyper(2,a,4,a,b,4,a)].

9 P(x -> ((y -> (z -> u)) -> ((y -> z) -> (y -> u)))). [hyper(2,a,3,a,b,4,a)].

10 P((x -> y) -> (x -> x)). [hyper(2,a,4,a,b,3,a)].

11 P(((-x -> -y) -> y) -> ((-x -> -y) -> x)). [hyper(2,a,4,a,b,5,a)].

12 P(x -> ((-y -> -z) -> (z -> y))). [hyper(2,a,3,a,b,5,a)].

14 P(x -> (y -> (z -> (u -> z)))). [hyper(2,a,3,a,b,7,a)].

17 P(x -> x). [hyper(2,a,10,a,b,7,a)].

18 P(((x -> y) -> x) -> ((x -> y) -> y)). [hyper(2,a,4,a,b,17,a)].

26 P((x -> ((y -> x) -> z)) -> (x -> z)). [hyper(2,a,8,a,b,7,a)].

44 P((x -> ((y -> (z -> y)) -> u)) -> (x -> u)). [hyper(2,a,8,a,b,14,a)].

48 P(((x -> (y -> z)) -> (((x -> y) -> (x -> z)) -> u)) -> ((x -> (y -> z)) -> u)). [hyper(2,a,8,a,b,9,a)].

71 P((x -> (-y -> -z)) -> (x -> (z -> y))). [hyper(2,a,4,a,b,12,a)].

159 P(-x -> (x -> y)). [hyper(2,a,26,a,b,12,a)].

160 P((x -> y) -> ((z -> x) -> (z -> y))). [hyper(2,a,26,a,b,9,a)].

166 P(x -> (-y -> (y -> z))). [hyper(2,a,3,a,b,159,a)].

197 P(((-x -> (x -> y)) -> z) -> z). [hyper(2,a,18,a,b,166,a)].

815 P(((x -> y) -> z) -> (y -> z)). [hyper(2,a,44,a,b,160,a)].

835 P(x -> (((y -> z) -> u) -> (z -> u))). [hyper(2,a,3,a,b,815,a)].

841 P(x -> ((x -> y) -> y)). [hyper(2,a,815,a,b,18,a)].

842 P(x -> ((-y -> -x) -> y)). [hyper(2,a,815,a,b,11,a)].

915 P(((x -> ((x -> y) -> y)) -> z) -> z). [hyper(2,a,841,a,b,841,a)].

918 P((x -> y) -> (x -> ((y -> z) -> z))). [hyper(2,a,160,a,b,841,a)].

1299 P((x -> (-y -> -x)) -> (x -> y)). [hyper(2,a,4,a,b,842,a)].

3180 P((x -> (y -> z)) -> (y -> (x -> z))). [hyper(2,a,48,a,b,835,a)].

3224 P(x -> ((((x -> y) -> y) -> z) -> z)). [hyper(2,a,915,a,b,918,a)].

4594 P(--x -> x). [hyper(2,a,197,a,b,1299,a)].

4644 P(--x -> ((x -> y) -> y)). [hyper(2,a,918,a,b,4594,a)].

4672 P(x -> --x). [hyper(2,a,5,a,b,4594,a)].

4728 P((x -> y) -> (x -> --y)). [hyper(2,a,160,a,b,4672,a)].

7577 P((-x -> y) -> (-y -> x)). [hyper(2,a,71,a,b,4728,a)].

19603 P(x -> ((x -> y) -> --y)). [hyper(2,a,3180,a,b,4728,a)].

19609 P((x -> y) -> (--x -> y)). [hyper(2,a,3180,a,b,4644,a)].

19633 P((x -> y) -> ((y -> z) -> (x -> z))). [hyper(2,a,3180,a,b,160,a)].

20528 P(--x -> ((x -> y) -> --y)). [hyper(2,a,19609,a,b,19603,a)].

23007 P((((x -> y) -> y) -> z) -> (x -> z)). [hyper(2,a,3180,a,b,3224,a)].

25963 P(((--x -> y) -> z) -> ((x -> y) -> z)). [hyper(2,a,19633,a,b,19609,a)].

26004 P(((-x -> y) -> z) -> ((-y -> x) -> z)). [hyper(2,a,19633,a,b,7577,a)].

26321 P((x -> y) -> (--x -> --y)). [hyper(2,a,3180,a,b,20528,a)].

27746 P((x -> y) -> (-y -> -x)). [hyper(2,a,71,a,b,26321,a)].

27754 P(x -> (-y -> -(x -> y))). [hyper(2,a,23007,a,b,27746,a)].

28030 P(-x -> (y -> -(y -> x))). [hyper(2,a,3180,a,b,27754,a)].

28135 P((-x -> y) -> (-x -> -(y -> x))). [hyper(2,a,4,a,b,28030,a)].

29738 P((-x -> y) -> ((y -> x) -> x)). [hyper(2,a,71,a,b,28135,a)].

34389 P((-x -> y) -> ((x -> y) -> y)). [hyper(2,a,26004,a,b,29738,a)].

34398 P((x -> y) -> ((-x -> y) -> y)). [hyper(2,a,25963,a,b,34389,a)].

34399 $F. [resolve(34398,a,6,a)].

Edit: Here's a shorter proof via OTTER. OTTER has found shorter proofs also, but they took more time for OTTER to find.

----> UNIT CONFLICT at 2.23 sec ----> 8034 [binary,8033.1,2.1] $F.

Length of proof is 36. Level of proof is 18.

---------------- PROOF ----------------

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

2 [] -P(C(C(a,b),C(C(N(a),b),b))).

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(N(x),N(y)),C(y,x))).

6 [hyper,1,3,3] P(C(x,C(y,C(z,y)))).

7 [hyper,1,3,4] P(C(x,C(C(y,C(z,u)),C(C(y,z),C(y,u))))).

8 [hyper,1,4,3] P(C(C(x,y),C(x,x))).

9 [hyper,1,3,5] P(C(x,C(C(N(y),N(z)),C(z,y)))).

10 [hyper,1,4,6] P(C(C(x,y),C(x,C(z,y)))).

15 [hyper,1,8,3] P(C(x,x)).

16 [hyper,1,4,15] P(C(C(C(x,y),x),C(C(x,y),y))).

21 [hyper,1,3,10] P(C(x,C(C(y,z),C(y,C(u,z))))).

23 [hyper,1,10,4] P(C(C(x,C(y,z)),C(u,C(C(x,y),C(x,z))))).

35 [hyper,1,3,16] P(C(x,C(C(C(y,z),y),C(C(y,z),z)))).

39 [hyper,1,16,6] P(C(C(C(x,C(y,x)),z),z)).

58 [hyper,1,4,21] P(C(C(x,C(y,z)),C(x,C(y,C(u,z))))).

74 [hyper,1,3,39] P(C(x,C(C(C(y,C(z,y)),u),u))).

136 [hyper,1,4,74] P(C(C(x,C(C(y,C(z,y)),u)),C(x,u))).

191 [hyper,1,136,5] P(C(C(N(x),N(C(y,C(z,y)))),x)).

192 [hyper,1,136,4] P(C(C(x,C(C(y,x),z)),C(x,z))).

199 [hyper,1,192,35] P(C(x,C(C(x,y),y))).

200 [hyper,1,192,9] P(C(N(x),C(x,y))).

201 [hyper,1,192,7] P(C(C(x,y),C(C(z,x),C(z,y)))).

215 [hyper,1,4,200] P(C(C(N(x),x),C(N(x),y))).

216 [hyper,1,3,200] P(C(x,C(N(y),C(y,z)))).

230 [hyper,1,3,215] P(C(x,C(C(N(y),y),C(N(y),z)))).

258 [hyper,1,3,199] P(C(x,C(y,C(C(y,z),z)))).

271 [hyper,1,23,201] P(C(x,C(C(C(y,z),C(u,y)),C(C(y,z),C(u,z))))).

274 [hyper,1,4,201] P(C(C(C(x,y),C(z,x)),C(C(x,y),C(z,y)))).

1921 [hyper,1,192,271] P(C(C(x,y),C(C(y,z),C(x,z)))).

2066 [hyper,1,274,258] P(C(C(C(C(x,y),y),z),C(x,z))).

2070 [hyper,1,274,230] P(C(C(C(N(x),y),z),C(C(N(x),x),z))).

2072 [hyper,1,274,216] P(C(C(C(x,y),z),C(N(x),z))).

2197 [hyper,1,2070,191] P(C(C(N(x),x),x)).

2204 [hyper,1,201,2197] P(C(C(x,C(N(y),y)),C(x,y))).

7657 [hyper,1,2204,2066] P(C(C(C(C(N(x),y),y),x),x)).

7700 [hyper,1,2072,7657] P(C(N(C(C(N(x),y),y)),x)).

7727 [hyper,1,1921,7700] P(C(C(x,y),C(N(C(C(N(x),z),z)),y))).

7831 [hyper,1,58,7727] P(C(C(x,y),C(N(C(C(N(x),z),z)),C(u,y)))).

8033 [hyper,1,2204,7831] P(C(C(x,y),C(C(N(x),y),y))).

8034 [binary,8033.1,2.1] $F.

------------ end of proof -------------

Answer 3

I have a fairly simple proof which when fully expanded is likely to be longer than the proofs found by Prover9 and Otter.

Beyond making use of the deduction theorem, it requires the following three lemmas (I give the lengths of the proofs found by my own amateurish theorem prover):

1. 33 lines: $(\lnot x \to y) \to (\lnot y \to x)$
2. 7 lines: $(y \to z) \to (x \to y) \to (x \to z)$
3. 23 lines: $(\lnot x \to x) \to x$

Proof: assume $(\lnot a \to b)$ and $(a \to b)$. By $(\lnot a \to b)$ and lemma 1 $[a/x, b/y]$ conclude $(\lnot b \to a)$. By this and the assumption $(a \to b)$ plus lemma 2, conclude $(\lnot b \to b)$. By lemma 3, conclude $b$.

Convert this to an assumption-free proof of $(\lnot a \to b) \to (a \to b) \to b$ by applying the deduction theorem unwinding algorithm.

Proof, now with more symbols and fewer words:

1. $(\lnot a \to b), (a \to b) \vdash \lnot a \to b \quad$ [assumption]
2. $(\lnot a \to b), (a \to b) \vdash (\lnot a \to b) \to (\lnot b \to a) \quad$ [lemma 1]
3. $(\lnot a \to b), (a \to b) \vdash \lnot b \to a \quad$ [modus ponens, $2 \sim (1 \to 3)$]
4. $(\lnot a \to b), (a \to b) \vdash (a \to b) \to (\lnot b \to a) \to (\lnot b \to b) \quad$ [lemma 2]
5. $(\lnot a \to b), (a \to b) \vdash (a \to b) \quad$ [assumption]
6. $(\lnot a \to b), (a \to b) \vdash (\lnot b \to a) \to (\lnot b \to b) \quad$ [modus ponens, $4 \sim (5 \to 6)$]
7. $(\lnot a \to b), (a \to b) \vdash (\lnot b \to b) \quad$ [modus ponens, $6 \sim (3 \to 7)$]
8. $(\lnot a \to b), (a \to b) \vdash (\lnot b \to b) \to b \quad$ [lemma 3]
9. $(\lnot a \to b), (a \to b) \vdash b \quad$ [modus ponens, $8 \sim (7 \to 9)$]

Proofs of the lemmas are available on request.