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

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.

  • 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.