
Originally Posted by
emakarov
This is not the converse of the original statement. The original statement was (writing ∀ for "for all" and ∃ for "there exists"):
b = sup A => ∀ c < b ∃ a ∈ A. c < a (*)
In fact, the assumption b = sup A is too strong; it is enough to assume half of the definition of sup, namely, that b is <= all upper bounds of A. That is, we don't have to assume that b is itself an upper bound.
The converse of (*) is the following.
(∀ c < b ∃ a ∈ A. c < a) => b = sup A (**)
Again, (**) is not provable because the conclusion is too strong. From the given assumption we can only prove that b is <= all upper bounds of A. Either the conclusion has to be changed as in the previous sentence, or the fact that b is an upper bound of A has to be added to the assumption.
Now, the important point is that your version of (**) is this.
∀c [(c < b and (∃ a ∈ A. c < a)) => b = sup A] (***)
An essential difference between (**) and (***) is that in (**), the scope of ∀ c is limited to the assumption, while in (***) it extends to the end of the formula. This is what happens when you say "Let c be real" in the beginning. As a result, in (***) you need to show b = sup A for each single c. In contrast, the assumption in (**) requires that something holds for all c. This makes the assumption in (**) much stronger. And, of course, (***) is not a converse of (*) because in (*) the scope of ∀ c is limited to the conclusion only.