2
$\begingroup$

I want to write a full prove for $p\wedge q \rightarrow p$ without using deduction, using only ${\neg, \rightarrow}$ connectives.

I use the standard axiomatic system:

$\alpha\rightarrow(\beta\rightarrow\alpha)$

$\alpha\rightarrow(\beta\rightarrow\gamma)\rightarrow((\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\gamma))$

$(\neg\beta\rightarrow\neg\alpha)\rightarrow((\neg\beta\rightarrow\alpha)\rightarrow \beta)$

I only succeeded to prove it using deduction. I tried to work back from deduction to full proof using the general fact (on which deduction theorem proof relies) that $\alpha \vdash\beta \Rightarrow \vdash\alpha\rightarrow B_i$, for every $B_i\in\{B_i\}_1^n$ the prove sequence of $\beta$ from $\alpha$ , in order to find a formula $\gamma$ to apply $A2$ such that $(\neg(p\rightarrow\neg q)\rightarrow(\gamma \rightarrow p))\rightarrow((\neg(p\rightarrow\neg q)\rightarrow\gamma)\rightarrow(\neg(p\rightarrow\neg q)\rightarrow p))$

My proof using deduction:

First $p\wedge q \rightarrow p \equiv \neg(p\rightarrow\neg q)\rightarrow p$

  1. deduction: $\neg(p\rightarrow q)\vdash p$
  2. applying lemma: $\alpha\vdash\beta\Leftrightarrow\neg\beta\vdash\neg\alpha$ one may prove: $\neg p\vdash p\rightarrow q$
  3. deduction: $\neg p,p\vdash q$
  4. A3: $(\neg q\rightarrow\neg p)\rightarrow((\neg q\rightarrow\ p)\rightarrow q)$
  5. A1 : $\neg p\rightarrow (\neg q\rightarrow\neg p)$
  6. MP by assumption $(\neg q\rightarrow\neg p)$
  7. A1 : $p\rightarrow (\neg q\rightarrow p)$
  8. MP by assumption $(\neg q\rightarrow p)$
  9. MP 6 from 4:$(\neg q\rightarrow\ p)\rightarrow q$
  10. MP 8 from 9:$q$
$\endgroup$
  • $\begingroup$ Are you allowed to use the deduction theorem? $\endgroup$ – Bram28 Apr 29 '18 at 20:27
  • $\begingroup$ @Bram28 sorry, but I want a full proof (avoiding deduction theorem) $\endgroup$ – dan Apr 30 '18 at 10:39
1
$\begingroup$

HINT

Work backwards. Since you need to show $\vdash \neg (p \rightarrow \neg q) \rightarrow p$ you probably want to show $\neg (p \rightarrow \neg q) \vdash p$ and then use the Deduction theorem.

Second, since the goal is now $p$, you probably want to use axiom 3 and show $\neg p \rightarrow \varphi$ and $\neg p \rightarrow \neg \varphi$ for some $\varphi$.

What might be that $\varphi$? Well, you have as a premise $\neg (p \rightarrow \neg q)$, so that could be your $\neg \varphi$, so then the $\varphi$ would be $p \rightarrow \neg q$.

OK, so here's the basic proof strategy/plan:

  1. Show that $\vdash \neg p \rightarrow (p \rightarrow \neg q)$ (which is easy: prove $p, \neg p \vdash q$ and then apply Deduction theorem twice)

  2. Show that $\neg (p \rightarrow \neg q) \vdash \neg p \rightarrow \neg (p \rightarrow \neg q)$ (even easier, using axiom 1)

  3. Given 1 and 2, and using axiom 3, we can quickly get: $\neg (p \rightarrow \neg q) \vdash p$

  4. Apply Deduction theorem on 3 to get $\vdash \neg (p \rightarrow \neg q) \rightarrow p$, i.e. $\vdash (p \land q) \rightarrow p$

$\endgroup$
  • 1
    $\begingroup$ "Apply Deduction theorem on 3 to get ⊢¬(p→¬q)→p, i.e. ⊢(p∧q)→p" That won't work for this question. The Deduction Theorem just consists of a statement. Dan needs to apply a suitable proof of The Deduction Theorem. $\endgroup$ – Doug Spoonwood Apr 29 '18 at 19:53
  • $\begingroup$ @DougSpoonwood good point ... just asked the OP if the use of the Ded Thm is allowed. $\endgroup$ – Bram28 Apr 29 '18 at 20:28
  • $\begingroup$ @Bram28 thanks for your answer but as I mentioned in the previous comment, I want to avoid deduction. $\endgroup$ – dan Apr 30 '18 at 10:41
1
$\begingroup$

I use Polish notation. This means that (x$\rightarrow$y) gets translated Cxy and $\lnot$x gets translated to Nx. $\lnot$(p$\rightarrow$$\lnot$q) translates to NCpNq.

1 CpCqp axiom

2 CCpCqrCCpqCpr axiom

3 CCNpNqCCNpqp axiom

4 CCN Nq N p CCN Nq p Nq 3

5 C CCNNqNpCCNNqpNq C NCpNq CCNNqNpCCNNqpNq 1

6 CNCpNqCCNNqNpCCNNqpNq {5, 4}

7 C CCNNqNpCCNNqpNq C Np CCNNqNpCCNNqpNq 1

8 C CCCNNqNpCCNNqpNqCNpCCNNqNpCCNNqpNq C NCpNq CCCNNqNpCCNNqpNqCNpCCNNqNpCCNNqpNq 1

9 CNCpNqCCCNNqNpCCNNqpNqCNpCCNNqNpCCNNqpNq {8, 7}

10 CC NCpNq C CCNNqNpCCNNqpNq CNpCCNNqNpCCNNqpNq CC NCpNq CCNNqNpCCNNqpNq C NCpNq CNpCCNNqNpCCNNqpNq 2

11 CCNCpNqCCNNqNpCCNNqpNqCNCpNqCNpCCNNqNpCCNNqpNq {10, 9}

12 CNCpNqCNpCCNNqNpCCNNqpNq {11, 6}

13 CC Np C CNNqNp CCNNqpNq CC Np CNNqNp C Np CCNNqpNq 2

14 C CCNpCCNNqNpCCNNqpNqCCNpCNNqNpCNpCCNNqpNq C NCpNq CCNpCCNNqNpCCNNqpNqCCNpCNNqNpCNpCCNNqpNq 1

15 C NCpNq CCNpCCNNqNpCCNNqpNqCCNpCNNqNpCNpCCNNqpNq {14, 13}

16 CC NCpNq C CNpCCNNqNpCCNNqpNq CCNpCNNqNpCNpCCNNqpNq CC NCpNq CNpCCNNqNpCCNNqpNq C NCpNq CCNpCNNqNpCNpCCNNqpNq 2

17 CCNCpNqCNpCCNNqNpCCNqpNqCNCpNqCCNpCNNqNpCNpCCNNqpNq {16, 15}

18 CNCpNqCCNpCNNqNpCNpCCNNqpNq {17, 12}

19 C Np C NNq Np 1

20 C CNpCNNqNp C NCpNq CNpCNNqNp 1

21 CNCpNqCNpCNNqNp {20, 19}

22 CC NCpNq C CNpCNNqNp CNpCCNNqpNq CC NCpNq CNpCNNqNp C NCpNq CNpCCNNqpNq 2

23 CCNCpNqCNpCNNqNpCNCpNqCNpCCNNqpNq {22, 18}

24 CNCpNqCNpCCNNqpNq {23, 21}

25 C CCNNqpNq Cp CCNNqpNq 1

26 C CCCNNqpNqCpCCNNqpNq C NCpNq CCCNNqpNqCpCCNNqpNq 1

27 CNCpNqCCCNNqpNqCpCCNNqpNq {26, 25}

28 C CCCNNqpNqCpCCNNqpNq C Np CCCNNqpNqCpCCNNqpNq 1

29 C CCCCNNqpNqCpCCNNqpNqCNpCCCNNqpNqCpCCNNqpNq C NCpNq CCCCNNqpNqCpCCNNqpNqCNpCCCNNqpNqCpCCNNqpNq 1

30 CNCpNqCCCCNNqpNqCpCCNNqpNqCNpCCCNNqpNqCpCCNNqpNq {29, 28}

31 CC NCpNq C CCCNNqpNqCpCCNNqpNq CNpCCCNNqpNqCpCCNNqpNq CC NCpNq CCCNNqpNqCpCCNNqpNq C NCpNq CNpCCCNNqpNqCpCCNNqpNq 2

32 CCNCpNqCCCNNqpNqCpCCNNqpNqCNCpNqCNpCCCNNqpNqCpCCNNqpNq {31, 30}

33 CNCpNqCNpCCCNNqpNqCpCCNNqpNq {32, 27}

34 CC Np C CCNNqpNq CpCCNNqpNq CC Np CCNNqpNq C Np CpCCNNqpNq 2

35 C CCNpCCCNNqpNqCpCCNNqpNqCCNpCCNNqpNqCNpCpCCNNqpNq C NCpNq CCNpCCCNNqpNqCpCCNNqpNqCCNpCCNNqpNqCNpCpCCNNqpNq 1

36 CNCpNqCCNpCCCNNqpNqCpCCNNqpNqCCNpCCNNqpNqCNpCpCCNNqpNq {35, 34}

37 CC NCpNq C CNpCCCNNqpNqCpCCNNqpNq CCNpCCNNqpNqCNpCpCCNNqpNq CC NCpNq CNpCCCNNqpNqCpCCNNqpNq C NCpNq CCNpCCNNqpNqCNpCpCCNNqpNq 2

38 CCNCpNqCNpCCCNNqpNqCpCCNNqpNqCNCpNqCCNpCCNNqpNqCNpCpCCNNqpNq {37, 36}

39 CNCpNqCCNpCCNNqpNqCNpCpCCNNqpNq {38, 33}

40 CC NCpNq C CNpCCNNqpNq CNpCpCCNNqpNq CC NCpNq CNpCCNNqpNq C NCpNq CNpCpCCNNqpNq 2

41 CCNCpNqCNpCCNNqpNqCNCpNqCNpCpCCNNqpNq {40, 39}

42 CNCpNqCNpCpCCNNqpNq {41, 24}

43 CC p C CNNqp Nq CC p CNNqp C p Nq 2

44 C CCpCCNNqpNqCCpCNNqpCpNq C NCpNq CCpCCNNqpNqCCpCNNqpCpNq 1

45 CNCpNqCCpCCNNqpNqCCpCNNqpCpNq {44, 43}

46 C CCpCCNNqpNqCCpCNNqpCpNq C Np CCpCCNNqpNqCCpCNNqpCpNq 1

47 C CCCpCCNNqpNqCCpCNNqpCpNqCNpCCpCCNNqpNqCCpCNNqpCpNq C NCpNq CCCpCCNNqpNqCCpCNNqpCpNqCNpCCpCCNNqpNqCCpCNNqpCpNq 1

48 CNCpNqCCCpCCNNqpNqCCpCNNqpCpNqCNpCCpCCNNqpNqCCpCNNqpCpNq {47, 46}

49 CC NCpNq C CCpCCNNqpNqCCpCNNqpCpNq CNpCCpCCNNqpNqCCpCNNqpCpNq CC NCpNq CCpCCNNqpNqCCpCNNqpCpNq C NCpNq CNpCCpCCNNqpNqCCpCNNqpCpNq 2

50 CCNCpNqCCpCCNNqpNqCCpCNNqpCpNqCNCpNqCNpCCpCCNNqpNqCCpCNNqpCpNq {49, 48}

51 CNCpNqCNpCCpCCNNqpNqCCpCNNqpCpNq {50, 45}

52 CC Np C CpCCNNqpNq CCpCNNqpCpNq CC Np CpCCNNqpNq C Np CCpCNNqpCpNq 2

53 C CCNpCCpCCNNqpNqCCpCNNqpCpNqCCNpCpCCNNqpNqCNpCCpCNNqpCpNq C NCpNq CCNpCCpCCNNqpNqCCpCNNqpCpNqCCNpCpCCNNqpNqCNpCCpCNNqpCpNq 1

54 CNCpNqCCNpCCpCCNNqpNqCCpCNNqpCpNqCCNpCpCCNNqpNqCNpCCpCNNqpCpNq {53, 52}

55 CC NCpNq C CNpCCpCCNNqpNqCCpCNNqpCpNq CCNpCpCCNNqpNqCNpCCpCNNqpCpNq CC NCpNq CNpCCpCCNNqpNqCCpCNNqpCpNq C NCpNq CCNpCpCCNNqpNqCNpCCpCNNqpCpNq 2

56 CCNCpNqCNpCCpCCNNqpNqCCpCNNqpCpNqCNCpNqCCNpCpCCNNqpNqCNpCCpCNNqpCpNq {55, 54}

57 CNCpNqCCNpCpCCNNqpNqCNpCCpCNNqpCpNq {56, 51}

58 CC NCpNq C CNpCpCCNNqpNq CNpCCpCNNqpCpNq CC NCpNq CNpCpCCNNqpNq C NCpNq CNpCCpCNNqpCpNq 2

59 CCNCpNqCNpCpCCNNqpNqCNCpNqCNpCCpCNNqpCpNq {58, 57}

60 CNCpNqCNpCCpCNNqpCpNq {59, 42}

61 CC Np C CpCNNqp CpNq CC Np CpCNNqp C Np CpNq 2

62 C CCNpCCpCNNqpCpNqCCNpCpCNNqpCNpCpNq C NCpNq CCNpCCpCNNqpCpNqCCNpCpCNNqpCNpCpNq 1

63 CNCpNqCCNpCCpCNNqpCpNqCCNpCpCNNqpCNpCpNq {62, 61}

64 CC NCpNq C CNpCCpCNNqpCpNq CCNpCpCNNqpCNpCpNq CC NCpNq CNpCCpCNNqpCpNq C NCpNq CCNpCpCNNqpCNpCpNq 2

65 CCNCpNqCNpCCpCNNqpCpNqCNCpNqCCNpCpCNNqpCNpCpNq {64, 63}

66 CNCpNqCCNpCpCNNqpCNpCpNq {65, 60}

67 CC NCpNq C CNpCpCNNqp CNpCpNq CC NCpNq CNpCpCNNqp C NCpNq CNpCpNq

68 CCNCpNqCNpCpCNNqpCNCpNqCNpCpNq {67, 66}

69 CpCNNqp 1

70 C CpCNNqp C Np CpCNNqp 1

71 CNpCpCNNqp {70, 69}

72 C CNpCpCNNqp C NCpNq CNpCpCNNqp 1

73 CNCpNqCNpCpCNNqp {72, 71}

74 CNCpNqCNpCpNq {68, 73}

75 CCNpNCpNqCCNpCpNqp 3

76 C CCNpNCpNqCCNpCpNqp C NCpNq CCNpNCpNqCCNpCpNqp 1

77 CNCpNqCCNpNCpNqCCNpCpNqp {76, 75}

78 CC NCpNq C CNpNCpNq CCNpCpNqp CC NCpNq CNpNCpNq C NCpNq CCNpCpNqp 2

79 CCNCpNqCNpNCpNqCNCpNqCCNpCpNqp {78, 77}

80 C NCpNq C Np NCpNq 1

81 CNCpNqCCNpCpNqp {80, 79}

82 CC NCpNq C CNpCpNq p CC NCpNq CNpCpNq C NCpNq p 2

83 CCNCpNqCNpCpNqCNCpNqp {82, 81}

84 CNCpNqp {83, 74}

$\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.