3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Oh man, huge undertaking. Why Java? Worst language ever. Im sure there are plenty better. I have never studied this level of logic so I cannot contribute much. But I do notice that the assertion youre trying to show is that "proof by contradiction" works. Am I mistaken? Isnt that what it boils down to? If it doesnt work, does that not imply that contradictions are not prohibited in your system? $\endgroup$ – CogitoErgoCogitoSum Apr 20 '18 at 16:21
  • $\begingroup$ Therre is huge literature on en.wikipedia.org/wiki/Automated_theorem_proving. Sophisticated systems like Prover9 or Vampire will have no difficulty finding this kind of proof. Unless you use powerful algorithms like resolution and an efficient implementation, you will be unlikely to get good results. $\endgroup$ – Rob Arthan Apr 20 '18 at 16:22
  • $\begingroup$ @CogitoErgoCogitoSum : I'm looking for a deduction. Possible steps: 1) premisses 2) axioms 3) MPs. Programming language: with C I would need 10 times more time... $\endgroup$ – PeptideChain Apr 20 '18 at 16:24
  • $\begingroup$ @RobArthan: thank you very much for the link and product names. I assumed that there were such libraries, but I needed less than two days to write the program and I learned a lot. $\endgroup$ – PeptideChain Apr 20 '18 at 16:27
  • $\begingroup$ The difference between Java and C is unlikely to make much difference. Unless you use a sophisticated algorithm to guide the proof search, the search space will grow far too fast. $\endgroup$ – Rob Arthan Apr 20 '18 at 16:28
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.