1
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 8 and 9 allow you to prove disjunctions. If ↔ means logical equivalence though, you need more axioms to prove the distributive equivalence that you referenced. $\endgroup$ – Doug Spoonwood Oct 24 '17 at 1:43
  • $\begingroup$ Though, one you have an equivalence axiom (you only need one actually), you basically can assume one side and prove the other via axiom 10. E. G. you have (q∨r). If q, then (p∧q), so the right. If r, then (p∧r), so the right. Then axiom 10 gets used to get to the right. From the right, if (p∧q), then q, so (q V r), thus the left. If (p∧r), then r, so (q V r), thus the right. Then use 10 to get to the left. (I've omitted some steps). Then from ((p→q)→((q→p)→(p↔q))) you have the equivalence. $\endgroup$ – Doug Spoonwood Oct 24 '17 at 1:58
  • $\begingroup$ I view $p \leftrightarrow q$ as a shorthand of $p \to q \land q \to p$, where your rule would just be 5. $\endgroup$ – Kenny Lau Oct 24 '17 at 2:03
  • $\begingroup$ @KennyLau I think that's possible. But, it could not be a shorthand also. $\endgroup$ – Doug Spoonwood Oct 24 '17 at 11:54
  • 1
    $\begingroup$ @ziggurism Well, Wikipedia dropped the ball ... We could easily add an axiom 'Hilbert-style': $(\phi \rightarrow \psi) \rightarrow ((\psi \rightarrow \phi) \rightarrow (\phi \leftrightarrow \psi))$ $\endgroup$ – Bram28 Oct 24 '17 at 16:21
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thank you Kenny. I followed all the steps, and agreed with each one, but am not sure I could've come up with them. I think studying the synopsis you wrote to try to get the big picture will be helpful. Thanks again. $\endgroup$ – ziggurism Oct 24 '17 at 18:42

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.