Logical Deduction an example

Question

I'm trying to prove the Negation introduction (a natural deduction rule) $$ \{(\alpha\to\beta),(\alpha\to(\neg\beta))\}\vdash(\neg\alpha) $$

The axioms of the chosen logical system are:

• $(\alpha\to(\beta\to\alpha))$,
• $((\alpha\to(\beta \to\gamma))\to ((\alpha\to\beta)\to(\alpha\to\gamma)))$,
• $(((\lnot\beta)\to(\lnot\alpha))\to(((\lnot\beta)\to\alpha)\to\beta))$.

The only inference rule is Modus Ponens (MP).

For this purpose I've written a Java program that iteratively generate new axioms and check for MP. Even if I let the program generates 20'000 steps (a part of which are MPs), I do not get $(\neg\alpha)$.

I assume that I have a program error, but I formulate my question as follows:

• Do I have a conceptional error?
• Do someone has the mathematical solution? (This would help me to debug the program)

EDIT after the problem has been solved.

The program seems to work correctly and is able to solve:

1. $\{\alpha\to\beta,\beta\to\gamma\}\vdash\alpha\to\gamma$ is solved in 12 iterantions
2. $\{\alpha,\alpha\to\beta\}\vdash\beta$ is solved in 1 iterantion
3. $\vdash\alpha\to\alpha$ is solved in 3 iterantions
4. $\{\alpha\to(\beta\to\gamma),\beta\}\vdash\alpha\to\gamma$ is solved in 3 iterantions
5. $\vdash(\neg\neg\alpha)\to\alpha$ is solved in 130 iterantions!

For the 5th solution I give the last part of the log (+2M steps and +6M subformulas):

DEGUG end step 130 [Steps 2254228, formulas 6642034, results 0/1]
DEGUG Step, 131
DEGUG Next formula I(I(N(1),N(N(1))),1)
DEGUG MP, 1
DEGUG MP, 2
DEGUG MP, 3
DEGUG Found result I(N(N(1)),1)
DEGUG MP, 4
DEGUG MP, 5
DEGUG MP, 6
DEGUG MP, 7
DEGUG MP, 8
DEGUG MP, 9
DEGUG end step 131 [Steps 2306683, formulas 6796093, results 1/1]
DEGUG successfull = true
DEGUG END successfull = true [Steps 2306683, formulas 6796093, results 1/1]


Deduction:
--------------------------------------------------------------------------
  9 : A3                   (((¬1) → (¬(¬1))) → (((¬1) → (¬1)) → 1))
156 : A1                   ((¬1) → ((¬(¬1)) → (¬1)))
162 : A1                   ((¬(¬1)) → ((¬1) → (¬(¬1))))
185 : A2                   (((¬1) → ((¬(¬1)) → (¬1))) → (((¬1) → (¬(¬1))) → ((¬1) → (¬1))))
226 : 156 185 MP           (((¬1) → (¬(¬1))) → ((¬1) → (¬1)))
53102 : A2                   ((((¬1) → (¬(¬1))) → (((¬1) → (¬1)) → 1)) → ((((¬1) → (¬(¬1))) → ((¬1) → (¬1))) → (((¬1) → (¬(¬1))) → 1)))
53659 : A2                   (((¬(¬1)) → (((¬1) → (¬(¬1))) → 1)) → (((¬(¬1)) → ((¬1) → (¬(¬1)))) → ((¬(¬1)) → 1)))
55067 : 9 53102 MP           ((((¬1) → (¬(¬1))) → ((¬1) → (¬1))) → (((¬1) → (¬(¬1))) → 1))
56341 : 226 55067 MP         (((¬1) → (¬(¬1))) → 1)
7079229 : A1                   ((((¬1) → (¬(¬1))) → 1) → ((¬(¬1)) → (((¬1) → (¬(¬1))) → 1)))
7158204 : 56341 7079229 MP     ((¬(¬1)) → (((¬1) → (¬(¬1))) → 1))
7160210 : 7158204 53659 MP     (((¬(¬1)) → ((¬1) → (¬(¬1)))) → ((¬(¬1)) → 1))
7215262 : 162 7160210 MP       ((¬(¬1)) → 1)

This explains why I'm not able to solve the problem of the question. For a brute force method it is too complex.

Answer 1

Hypothetical Syllogism : $\alpha \to \beta, \beta \to \gamma \vdash \alpha \to \gamma$

Double Negation 1 : $\vdash \lnot \lnot \alpha \to \alpha$

Double Negation 2 : $\vdash \alpha \to \lnot \lnot \alpha$

---

1) $(α→β)$ --- premise

2) $(α→ ¬β)$ --- premise

3) $\vdash (¬¬α → ¬β ) → ((¬¬α → β) → ¬α)$ --- Ax.3

4) $(¬¬α → ¬β )$ --- from 2) and DN-1 by HS

5) $(¬¬α → β )$ --- from 1) and DN-1 by HS

6) $¬α$ --- from 3), 4) and 5) by modus ponens twice.