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

enter image description here

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

  • 3
    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 – Cort Ammon 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. – Atamiri Apr 2 '15 at 2:43
  • 2
    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). – Mauro ALLEGRANZA 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. – Mauro ALLEGRANZA Apr 2 '15 at 14:07

It follows directly from the definition of implication.

x=y ∨ φ ≡ ¬¬(x=y) ∨ φ ≡ ¬(x=y) ⊃ φ

φ can be any formula. You don't need the other axiom.

| improve this answer | |
  • can you please show me how to prove it? – free23 Apr 1 '15 at 19:28
  • What I wrote is the proof. – Atamiri Apr 1 '15 at 21:07
  • but what I want to prove is not ¬(x=y) ⊃ φ, in the first implication φ is ( (x<y) or (x>y), but what I want to prove is ¬(x=y) ⊃ ((x<y) or (y<x)) ,which is a little bit different, so we should use the other axiom. – free23 Apr 1 '15 at 21:20
  • Can you use resolution? Just add the negation of what you want to prove to the set of clauses. You'll arrive at a contradiction. – Atamiri Apr 1 '15 at 22:11
  • I don't think so, could you please tell me what is wrong in my proof? I cannot discharge an assumption – free23 Apr 1 '15 at 22:21

Not the answer you're looking for? Browse other questions tagged or ask your own question.