# Formally proving $p\wedge q \rightarrow p$

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

I want to 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$$
• Are you allowed to use the deduction theorem? Apr 29, 2018 at 20:27
• @Bram28 sorry, but I want a full proof (avoiding deduction theorem) Apr 30, 2018 at 10:39
• You're missing something very big here. The deduction theorem is a completely constructive theorem; it tells you precisely how to transform a proof for $S+A ⊢ B$ to a proof for $S ⊢ A→B$. So just keep applying that transformation to the proof you already have and you would be done. Sep 10, 2020 at 4:14

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$

• "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. Apr 29, 2018 at 19:53
• @DougSpoonwood good point ... just asked the OP if the use of the Ded Thm is allowed. Apr 29, 2018 at 20:28
• @Bram28 thanks for your answer but as I mentioned in the previous comment, I want to avoid deduction. Apr 30, 2018 at 10:41

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}