1
$\begingroup$

Using two forms of provability:

  • Identity Elimination/Transitivity
  • AnaCon: Analytical Consequence

Below, "Larger(x,y)" means "x is larger than y", "Smaller(x,y)" means "x is smaller than y", and "SameSize(x,y)" means "x is the same size as y".

What would be the best way (makes more logical sense) to prove the following:

  1. Larger(b, c)
  2. Smaller(b, d)
  3. SameSize(d, e)
    --> Larger(e, c) <-- this is what we are trying to prove

I have the following proofs:

Proof # 1

4) Smaller(b, e) AnaCon: 2, 3
5) Larger(e, b) AnaCon: 4
6) Larger(e, c) AnaCon: 5, 1

Proof # 2

4) Smaller(b, e) AnaCon: 2, 3
5) Larger(e, c) AnaCon: 4, 1

Proof # 3

4) Smaller(c, d) AnaCon: 1, 2
5) Larger(e, c) AnaCon: 4, 3

  • 2
    @KerxPhilo: There are likely *many* different ways at arriving at the same thing, some more circuitous than others. In some sense, you are being more explicit in #1 than in the others (e.g., in #4, you are first going from Smaller(c,d) to Larger(d,c), then using this and SameSize(e,d) to get (5); you skipped the first step, but you were explicit about in in #1). Every proof will touch the following "bases": b is larger than c and smaller than d, so d is larger than c, and therefore e is smaller than c.2011-03-07

1 Answers 1

1

As edited they now all look equivalent. Proof #1 is slightly more explicit when using the fact that Smaller(y,x) implies Larger(x,y) , which seems to be implicit in the others. You could also have another 3 step version

4) Larger(d, b) from 2 - reverse

5) Larger(d, c) from 4, 1 - transitive

6) Larger(e, c) from 5, 3 - substitution

and I suspect there are other variants