I 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.