Formally proving $p\wedge q \rightarrow p$

Question

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$

Answer 1

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$

Answer 2

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}