how to discharge the assumption? [closed]

I want to prove (forall(x,y) ~(x=y)-->((x<y) or (y<x)) from (forall(x,y) ((x=y) or(x<y) or (x>y)) and (forall(x,y) ( (x>y)--> ~(y>x))

but how to discharge b>a? can anyone help me please?

• This probably belong on the mathematics page. Your question is entirely encapsulated within the rules of logic. Philosophy tends to branch out to wider concerns, because mathematics completely defines this kind of loigcI'm voting to close this question as off-topic because Apr 1 '15 at 17:47
• You can't eliminate universal quantifiers by introducing constants. Skolemizaton is a way of getting rid of existential quantifiers. Apr 2 '15 at 2:43
• But why do you think that (x>y) is different from : (y<x) ? In first-order arithmetic, we usually define : (y<x) as ∃z(x=y+(z+1)) and consequently we define (x>y) as (y<x). Apr 2 '15 at 8:00
• In order to correct it : throw away all the right part of the proof; after 9) assume : ~(a < b), apply Disjunctive Syllogism to derive directly 12) : (a < b) ∨ (a > b) and then conclude with 5) by →-introduction. Apr 2 '15 at 14:07