Proving $\alpha \implies \alpha$ is derivable

logicpropositional-calculus

I'm going through Goldblatt's "Topoi", and one of the exercises there depends upon proving that a certain axiom system entails $\alpha \implies \alpha$ for any proposition $\alpha$.

The axiom system in question is as follows (paragraph 6.3):

  1. $ \alpha \implies (\alpha \land \alpha) $
  2. $ (\alpha \land \beta) \implies (\beta \land \alpha) $
  3. $ (\alpha \implies \beta) \implies ((\alpha \land \gamma) \implies (\beta \land \gamma)) $
  4. $ ((\alpha \implies \beta) \land (\beta \implies \gamma)) \implies (\alpha \implies \gamma) $
  5. $ \beta \implies (\alpha \implies \beta) $
  6. $ (\alpha \land (\alpha \implies \beta)) \implies \beta $
  7. $ \alpha \implies (\alpha \lor \beta) $
  8. $ (\alpha \lor \beta) \implies (\beta \lor \alpha) $
  9. $ ((\alpha \implies \gamma) \land (\beta \implies \gamma)) \implies ((\alpha \lor \beta) \implies \gamma) $
  10. $ \lnot \alpha \implies (\alpha \implies \beta) $
  11. $ ((\alpha \implies \beta) \land (\alpha \implies \lnot \beta)) \implies \lnot \alpha $
  12. $ \alpha \lor \lnot \alpha $

The sole inference rule is the usual modus ponens.

So, it feels like the axiom (9) together with (12) can be used as the last step of the derivation (instantiating $\alpha$ to $\alpha$, $\beta$ to $\lnot \alpha$ and $\gamma$ to $\alpha \implies \alpha$). Then, the left-hand side of the $\land$ in (9) can be derived using (5), and the right-hand side can be derived using (10). But how do I combine those under a $\land$? Looks like I don't have a usual $\land$-introduction rule — axiomatic systems I've seen before typically have something of the form $\alpha \implies (\beta \implies (\alpha \land \beta))$.

Also, resorting to the (non-constructive) axiom of excluded middle for this obviously constructive statement feels just wrong.

So what's the right way to prove $\alpha \implies \alpha$ in this system?

Best Answer

Well, before I lose it, here's what Prover9 gave me after translation into a prefix notation. C(x, y) gets used instead of (x⟹y). K(x,y) instead of (x∧y). N(x) instead of $\lnot$x. And A(x,y) instead of (x$\lor$y).:

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

% Proof 1 at 1.19 (+ 0.56) seconds.

% Length of proof is 16.

% Level of proof is 6.

% Maximum clause weight is 14.

% Given clauses 812.

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

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

3 P(C(x,K(x,x))). [assumption].

5 P(C(C(x,y),C(K(x,z),K(y,z)))). [assumption].

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

11 P(C(K(C(x,y),C(z,y)),C(A(x,z),y))). [assumption].

12 P(C(N(x),C(x,y))). [assumption].

14 P(A(x,N(x))). [assumption].

15 -P(C(c1,c1)). [deny(1)].

24 P(C(x,C(y,C(z,y)))). [hyper(2,a,7,a,b,7,a)].

55 P(K(C(N(x),C(x,y)),C(N(x),C(x,y)))). [hyper(2,a,3,a,b,12,a)].

99 P(C(K(x,y),K(C(z,C(u,z)),y))). [hyper(2,a,5,a,b,24,a)].

1001 P(K(C(x,C(y,x)),C(N(z),C(z,u)))). [hyper(2,a,99,a,b,55,a)].

11705 P(C(A(x,N(y)),C(y,x))). [hyper(2,a,11,a,b,1001,a)].

11723 P(C(x,x)). [hyper(2,a,11705,a,b,14,a)].

11724 $F. [resolve(11723,a,15,a)].

Related Question