formal Proof of an inequality

Question

In trying to prove , $a\leq b\wedge b\leq c\Longrightarrow a\leq c$ I come up with the following:

Proof: (intuitively)

case 1: $a<b\wedge b<c\Longrightarrow a<c\Longrightarrow a\leq c$

case 2: $a<b\wedge b=c\Longrightarrow a<c\Longrightarrow a\leq c$

case 3: $a=b\wedge b<c\Longrightarrow a<c\Longrightarrow a\leq c$

case 4 : $ a=b\wedge b=c\Longrightarrow a=c\Longrightarrow a\leq c$

My question is :

What is the corresponding formal proof of the above proof within a natural deduction system ??

Answer 1

You are trying to prove the transitivity of $≤$.

For the first implication you assumed the transitivity of $<$ in case 1. In cases 2, 3 and 4, you used the definition of equality.

For the final implication in each case, you used the definition of $≤$ which is $≤ \,\,\, := \,\,\, (< \lor =$).

Answer 2

Here is a formal proof, using fairly standard logical inference rules

1. $\forall x \forall y \forall z \ ((x < y \land y < z) \rightarrow x < z)$ (Axiom)

2. $\forall x \forall y \ (x \le y \leftrightarrow (x < y \lor x = y))$ (Axiom)

3. $a \le b \land b \le c$ (Assumption)

4. $a \le b$ ($\land $ Elim, 4)

5. $b \le c$ ($\land $ Elim, 4)

6. $a \le b \leftrightarrow (a < b \lor a = b)$ ($\forall$ Elim, 2)

7. $a < b \lor a = b$ ($\leftrightarrow$ Elim, 4,7)

8. $b \le c \leftrightarrow (b < c \lor b = c)$ ($\forall$ Elim, 2)

9. $b < c \lor b = c$ ($\leftrightarrow$ Elim, 5,8)

10. $a \le c \leftrightarrow (a < c \lor a = c)$ ($\forall$ Elim, 2)

(and now you do cases. First on 7: Case 1:)

11. $a < b$ (Assumption)

(And now cases on 9: Case 1A: (this corresponds to your case 1))

12. $b < c$ (Assumption)

13. $a < b \land b < c$ ($\land$ Intro, 11,12)

14. $(a < b \land b < c) \rightarrow a < c$ ($\forall$ Elim, 1)

15. $a < c$ ($\rightarrow$ Elim,13, 14)

16. $a < c \lor a = c$ ($\lor$ Intro, 15)

17. $a \le c$ ($\leftrightarrow$ Elim, 10,16)

(that completed Case 1A, Now do Case 1B (corresponding to your case 2))

18. $b = c$ (Assumption)

19. $a < c$ ($=$ Elim, 11,18)

20. $a < c \lor a = c$ ($\lor$ Intro, 19)

21. $a \le c$ ($\leftrightarrow$ Elim, 10,20)

(and that completes 1B. Wrap up with:)

22. $a \le c$ ($\lor$ Elim, 9,12-17,18-21)

(now start Case 2:)

23. $a = b$ (Assumption)

(This one splits as well. Case 2A: (your case 3)

24. $b < c$ (Assumption)

25. $a < c$ ($=$ Elim, 23,24)

26. $a < c \lor a = c$ ($\lor$ Intro, 25)

27. $a \le c$ ($\leftrightarrow$ Elim, 10,26)

(finally, Case 2B (your case 4):)

28. $b=c$ (Assumption)

29. $a= c$ ($=$ Elim, 23, 28)

30. $a < c \lor a = c$ ($\lor$ Intro, 29)

31. $a \le c$ ($\leftrightarrow$ Elim, 10,30)

(wrap up Case 2 with:)

32. $a \le c$ ($\lor$ Elim, 9,24-27,28-31)

(and now wrap us Case 1 and 2):

33. $a \le c$ ($\lor$ Elim, 7,11-22,23-32)