How Does the Supremum of -A Relate to Its Elements?

[Mr Davis 97]

Given that ##A## is a nonempty set of real numbers, and that ##-A = \{-x ~ | ~ x \in A\}##, I want to show the following:

##\forall a' \in -A, ~ \sup (-A) \ge a'## implies that ##\forall a \in A, ~\sup (-A) \ge -a##.

This is intuitively obvious, as we just "replace" ##a'## with ##-a##. But I don't see how to make the switch from one to the other rigorously.

 

[fresh_42]

Per definition we have ##\forall a \in A \,\exists \, a' \in -A \, : \, a'=-a \,\Longrightarrow \, \forall a \in A \,\exists \, a' \in -A \, : \, \operatorname{sup}(-A)\stackrel{given \, cond.}{\geq} a' = -a##

But I don't think this would be more helpful than a simple "thus".

 

[andrewkirk]

This is a case where the abbreviations we use obscure the meaning and make things more difficult.

The symbol string
$$\forall x\in S, (P(x))$$
is actually shorthand for
$$\forall x(x\in S\to P(x))$$
So
$$\forall a' \in -A, \sup (-A) \ge a'$$
means
$$\forall a'(a' \in -A \to \sup (-A) \ge a')$$
which, by the definition ##-A\equiv\{x\ :\ -x\in A\}##, means
$$\forall a'(-a' \in A \to \sup (-A) \ge a')$$
We then write down an instance of the Axiom Schema of Substitution in which we substitute ##-a## for ##a'## in the consequent, to give us:
$$
(\forall a'(-a' \in A \to \sup (-A) \ge a'))
\to
(-(-a) \in A \to \sup (-A) \ge (-a))
$$
Using Modus Ponens on this and the previous line, and replacing ##-(-a)## by ##a## we get
$$a \in A \to \sup (-A) \ge -a$$
We then universally quantify ##a##, which we can do because it is a free variable in the formula, under the Axiom Schema of Restricted Generalisation. This gives
$$\forall a(a \in A \to \sup (-A) \ge -a)$$
which is what we sought to prove.

As usual, when we have to resort to formal logic, proofs get rather longer!

 

[Mr Davis 97]

Per definition we have ##\forall a \in A \,\exists \, a' \in -A \, : \, a'=-a \,\Longrightarrow \, \forall a \in A \,\exists \, a' \in -A \, : \, \operatorname{sup}(-A)\stackrel{given \, cond.}{\geq} a' = -a##

But I don't think this would be more helpful than a simple "thus".

This is a case where the abbreviations we use obscure the meaning and make things more difficult.

The symbol string
$$\forall x\in S, (P(x))$$
is actually shorthand for
$$\forall x(x\in S\to P(x))$$
So
$$\forall a' \in -A, \sup (-A) \ge a'$$
means
$$\forall a'(a' \in -A \to \sup (-A) \ge a')$$
which, by the definition ##-A\equiv\{x\ :\ -x\in A\}##, means
$$\forall a'(-a' \in A \to \sup (-A) \ge a')$$
We then write down an instance of the Axiom Schema of Substitution in which we substitute ##-a## for ##a'## in the consequent, to give us:
$$
(\forall a'(-a' \in A \to \sup (-A) \ge a'))
\to
(-(-a) \in A \to \sup (-A) \ge (-a))
$$
Using Modus Ponens on this and the previous line, and replacing ##-(-a)## by ##a## we get
$$a \in A \to \sup (-A) \ge -a$$
We then universally quantify ##a##, which we can do because it is a free variable in the formula, under the Axiom Schema of Restricted Generalisation. This gives
$$\forall a(a \in A \to \sup (-A) \ge -a)$$
which is what we sought to prove.

As usual, when we have to resort to formal logic, proofs get rather longer!

Since for my purposes that is a tinge too formal, how would you suppose that I write out such a step in a proof (where the proof involves showing that ##\inf A = - \sup (-A)##)? It it enough to just say that ##\forall a' \in -A, ~ \sup (-A) \ge a'## implies that ##\forall a \in A, ~\sup (-A) \ge -a##?

 

[fresh_42]

Since for my purposes that is a tinge too formal, how would you suppose that I write out such a step in a proof (where the proof involves showing that ##\inf A = - \sup (-A)##)? It it enough to just say that ##\forall a' \in -A, ~ \sup (-A) \ge a'## implies that ##\forall a \in A, ~\sup (-A) \ge -a##?

Yes, I think it is sufficient. I first had to write it down to "see" whether the signs are not confused, and came up with the explanation:
##\forall a' \in -A, ~ \operatorname{sup}(-A) \geq a'## is shorthanded ##\operatorname{sup}(-A) \geq -A## and then it is obvious that both inequalities express the same fact.

 

[FactChecker]

You can express the proof in simple steps. Suppose a ∈ A. Then -a ∈ -A. So sup( -A ) ≥ -a.