# formal Proof of an inequality

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 ??

• is transitivity a law of logic ?? – user149368 Jul 1 '17 at 13:14
• On base of transitivity of $<$ you proved transitivity of $\leq$. What I am missing in your proof is the statement that $<$ is indeed a transitive relation. If your excuse for that is that $<$ is usually the notation of a transitive relation then you are implicitly saying that a proof is not needed: also $\leq$ is usually the notation of a transitive (and also reflexive) relation. – drhab Jul 1 '17 at 13:15
• (would just like to point out a format mistake in 'l' instead of 'L' for the 'implies' arrow in case 4) – Shuri2060 Jul 1 '17 at 13:27
• @user149368 Not sure what you're after - could you clarify? Are you after laws in logic as in the 3 laws (identity, non-contradiction, excluded middle)? en.wikipedia.org/wiki/Law_of_thought#The_law_of_identity – Shuri2060 Jul 1 '17 at 13:48

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 =$).

• Are, transitivity of < ,definition of equality, definition of less or equal, laws of logic?? – user149368 Jul 1 '17 at 13:35
• @user149368 No they're not. Was a little unsure on what you were looking for initially. Include the logic tag or similar if you're after that? – Shuri2060 Jul 1 '17 at 13:43

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:)

1. $a < b$ (Assumption)

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

1. $b < c$ (Assumption)

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

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

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

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

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

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

1. $b = c$ (Assumption)

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

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

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

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

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

(now start Case 2:)

1. $a = b$ (Assumption)

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

1. $b < c$ (Assumption)

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

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

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

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

1. $b=c$ (Assumption)

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

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

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

(wrap up Case 2 with:)

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

(and now wrap us Case 1 and 2):

1. $a \le c$ ($\lor$ Elim, 7,11-22,23-32)
• Surely a formal proof without showing the laws of logic taking place in the proof is not a formal proof – user149368 Jul 2 '17 at 21:32
• @user149368 True, but like I said, there many different formal proof systems, each with their own set of inference rules. So, if you want an answer to your question, you will have to tell me what formal proof system you are working with. As long as you don't this 'pseudo formal proof' is the best I can do. I can't read your mind! – Bram28 Jul 2 '17 at 21:37
• I did write in my OP ,within a natural deduction system – user149368 Jul 2 '17 at 21:45
• Let me also give you the appropriate axioms and definitions.1) the trichotomy law 2) transitive law < 3) addition law of < 4) multiplication law of < and 5) the definition of the relation les or equal – user149368 Jul 2 '17 at 21:48
• @user149368 There are still a lot of different natural deduction systems. Also, I can guess what the trichotomy and transitivity law for < are, but I am not too sure what you mean by the addition and multiplication laws for < (though I doubt you need those for this proof ...). The definition of less than or equal is of course crucial for this proof, What is the axiom for that? Is that the same as what I had in my post, i.e. $\forall x \forall y (x \le y \leftrightarrow (x < y \lor x = y))$? – Bram28 Jul 2 '17 at 22:55