I wish I could manipulate universal quantifiers better

[Atomised]

Homework Statement

I am asked to prove by contradiction that:

A real number x that is less than every positive real cannot be positive.

Homework Equations

Axiom of Order ('A14'):

a <= b and 0 < c → ac <= bc

The Attempt at a Solution

I believe I can prove it analytically as follows:

Assume otherwise, then x is less than every positive real and x is positive, therefore it is the least positive number. But consider the number ½ x. Substituting into the above axiom letting a = 0, b = ½, c = x we obtain 0 < ½x, demonstrating that as well as being &lt; x, ½ x is also positive. Contradiction since x was assumed to be the least positive real.

But I would love to be able to throw around a few quantifiers, negate them etc and prove it far more easily. So far not so good...

 

[az_lender]

Don't be silly. Your proof is optimal. In actual substance, it is 100% efficient.

 

[Atomised]

Thank you, I was very pleased with it even though it doesn't use the technique I set out to use and I am aware that I have not explicitly demonstrated that ½x < x by axiom.

Even so I am very interested in being able to usefully manipulate quantifiers - not always apparent to me how to negate statements...or even what the lists of symbols I end up with actually mean.

For example in the case of the statement I have proved above my plan was to express it as:

\exists x\in R^{+} | x&lt;ε, \forall ε &gt;0

making that line 2

negate it thereby making a true statement in line 1,

then derive a contradiction from line 2, assuring the truth of line 1.

Any ideas?

 

[D H]

You found a contradiction. Why do you want to go all formal?

What you need here for a more formal approach is universal elimination. Assuming there exists an x>0 means x/2>0. By universal elimination, you can substitute $x/2$ for $\varepsilon$ in $\forall \varepsilon > 0, x < \varepsilon$ yielding $x<x/2$, which is a contradiction.

 

[Atomised]

Thanks D H I like your proof.

The question in the back of my mind is how useful is the technique of being able to negate statements using \forall,\exists to derrive proofs by contradiction. No doubt it will often fail, but I would like to be able to examine it as an option, however it is far from clear to me what the rules are for forming \negP, once P involves >2 predicates.

Am I barking up the wrong tree?