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 $< 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<ε, \forall ε >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 $\neg$P, once P involves >2 predicates.

Am I barking up the wrong tree?