Prove distributive law in Hilbert system

Question

Using the logical axioms of the Hilbert system

1. $\phi\to\phi$
2. $\phi\to(\psi\to\phi)$
3. $\left( \phi \to \left( \psi \rightarrow \xi \right) \right) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right)$
4. $\left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right)$
5. $\alpha\to\beta\to\alpha\land\beta$
6. $\alpha\wedge\beta\to\alpha$
7. $\alpha\wedge\beta\to\beta$
8. $\alpha\to\alpha\vee\beta$
9. $\beta\to\alpha\vee\beta$
10. $(\alpha\to\gamma)\to (\beta\to\gamma) \to \alpha\vee\beta \to \gamma$

along with the inference rule modus ponens MP $\dfrac{\alpha,\alpha\to\beta}{\beta}$,

how can we prove the distributive law $p\wedge(q\vee r) \leftrightarrow(p\wedge q)\vee(p\wedge r)$? I'm sure I'm probably missing something quite obvious, but I can't see how any of these axioms can prove any disjunction at all.

Answer 1

For the forward direction: you need to split the premise into $p$ and $q \lor r$, then use prove by cases (i.e. 10) on $q \lor r$ along with $p$.

---

01 p→q→(p∧q)                   5
02 p∧q→(p∧q)∨(p∧r)             8
03 (p∧q→(p∧q)∨(p∧r))→(q→p∧q→(p∧q)∨(p∧r)) 2
04 q→p∧q→(p∧q)∨(p∧r)           MP 02 03
05 (q→p∧q→(p∧q)∨(p∧r))→(q→p∧q)→(q→(p∧q)∨(p∧r)) 3
06 (q→p∧q)→(q→(p∧q)∨(p∧r))     MP 04 05
07 ((q→p∧q)→(q→(p∧q)∨(p∧r)))→p→(q→p∧q)→(q→(p∧q)∨(p∧r)) 2
08 p→(q→p∧q)→(q→(p∧q)∨(p∧r))   MP 06 07
09 (p→(q→p∧q)→(q→(p∧q)∨(p∧r)))→(p→(q→p∧q))→(p→(q→(p∧q)∨(p∧r))) 3
10 (p→q→p∧q)→(p→q→(p∧q)∨(p∧r)) MP 08 09
11 p→q→(p∧q)∨(p∧r)             MP 01 10

12 p→r→(p∧r)                   5
13 p∧r→(p∧q)∨(p∧r)             9
14 (p∧r→(p∧q)∨(p∧r))→(r→p∧r→(p∧q)∨(p∧r)) 2
15 r→p∧r→(p∧q)∨(p∧r)           MP 13 14
16 (r→p∧r→(p∧q)∨(p∧r))→(r→p∧r)→(r→(p∧q)∨(p∧r)) 3
17 (r→p∧r)→(r→(p∧q)∨(p∧r))     MP 15 16
18 ((r→p∧r)→(r→(p∧q)∨(p∧r)))→p→(r→p∧r)→(r→(p∧q)∨(p∧r)) 2
19 p→(r→p∧r)→(r→(p∧q)∨(p∧r))   MP 17 18
20 (p→(r→p∧r)→(r→(p∧q)∨(p∧r)))→(p→(r→p∧r))→(p→(r→(p∧q)∨(p∧r))) 3
21 (p→r→p∧r)→(p→r→(p∧q)∨(p∧r)) MP 19 20
22 p→r→(p∧q)∨(p∧r)             MP 12 21

23 (q→(p∧q)∨(p∧r))→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r) 10
24 ((q→(p∧q)∨(p∧r))→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r))→p→((q→(p∧q)∨(p∧r))→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r)) 2
25 p→((q→(p∧q)∨(p∧r))→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r)) MP 23 24
26 (p→(q→(p∧q)∨(p∧r))→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r))→(p→(q→(p∧q)∨(p∧r)))→(p→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r)) 3
27 (p→(q→(p∧q)∨(p∧r)))→(p→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r)) MP 25 26
28 p→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r) MP 11 27
29 (p→(r→(p∧q)∨(p∧r))→(q∨r)→(p∧q)∨(p∧r))→(p→(r→(p∧q)∨(p∧r)))→(p→(q∨r)→(p∧q)∨(p∧r)) 3
30 (p→(r→(p∧q)∨(p∧r)))→(p→(q∨r)→(p∧q)∨(p∧r)) MP 28 29
31 p→(q∨r)→(p∧q)∨(p∧r) MP 22 30

32 (p→(q∨r)→(p∧q)∨(p∧r))→p∧(q∨r)→p→(q∨r)→(p∧q)∨(p∧r) 2
33 p∧(q∨r)→p→(q∨r)→(p∧q)∨(p∧r) MP 31 32
34 (p∧(q∨r)→p→(q∨r)→(p∧q)∨(p∧r))→(p∧(q∨r)→p)→(p∧(q∨r)→(q∨r→(p∧q)∨(p∧r))) 3
35 (p∧(q∨r)→p)→(p∧(q∨r)→(q∨r→(p∧q)∨(p∧r))) MP 33 34
36 p∧(q∨r)→p 6
37 p∧(q∨r)→(q∨r→(p∧q)∨(p∧r)) MP 36 35

38 (p∧(q∨r)→(q∨r→(p∧q)∨(p∧r)))→(p∧(q∨r)→q∨r)→(p∧(q∨r)→(p∧q)∨(p∧r)) 3
39 (p∧(q∨r)→q∨r)→(p∧(q∨r)→(p∧q)∨(p∧r)) MP 37 38
40 p∧(q∨r)→q∨r 7
41 p∧(q∨r)→(p∧q)∨(p∧r) MP 39 40

Synopsis:

11 p→q→(p∧q)∨(p∧r)
22 p→r→(p∧q)∨(p∧r)
31 p→(q∨r)→(p∧q)∨(p∧r)
37 p∧(q∨r)→(q∨r→(p∧q)∨(p∧r))
41 p∧(q∨r)→(p∧q)∨(p∧r)

---

The backward direction is left as an exercise to the reader.