Nested quantifiers and restrict domain

Question

Consider the following statement.

For each non-negative real number $s$, there exists a non-negative real number $t$ such that $s \geq t.$

(This statement happens to be true, just let $t = 0$, but that is not the goal of this question.)

I’m interested in translating this expression into symbols. For that, let $\mathbb{R}^{\text{nn}}$ be the set of all non-negative real numbers.

This is straightforward, and it goes as follows.

$$(\forall s \in \mathbb{R}^{\text{nn}})(\exists t \in \mathbb{R}^{\text{nn}}): s \geq t.$$

Although, I want to have a symbolic expression like this one, but considering the set of all real numbers $\mathbb{R}$ as the domain of $s$ and $t.$

First, I realize that $(\exists t \in \mathbb{R}^{\text{nn}}): s \geq t \iff (\exists t \in \mathbb{R}): [s \geq t \wedge t \geq 0].$

Substituting this in our first expression yields the following.

$$(\forall s \in \mathbb{R}^{\text{nn}})(\exists t \in \mathbb{R}): [s \geq t \wedge t \geq 0].$$

Second, let $Q(s)$ be the statement $(\exists t \in \mathbb{R}):[s \geq 0 \wedge t \geq 0].$ I realize that $(\forall s \in \mathbb{R}^{\text{nn}}):Q(s) \iff (\forall s \in \mathbb{R}):[s \geq 0 \to Q(s)].$

Finally, I have the following.

$$(\forall s \in \mathbb{R}):(s \geq 0 \to [(\exists t \in \mathbb{R}): s \geq t \wedge t \geq 0]).$$

Using the Null Quantification Rule, I get the following equivalent expression.

$$(\forall s \in \mathbb{R}) (\exists t \in \mathbb{R}):[s \geq 0 \to (s \geq t \wedge t \geq 0)].$$

(I can bring the existential quantifier outside because $t$ only appears in the expression that it is in its scope.)

Translating back into English, we get the following statement.

For each real number $s$, exists some real number $t$, such that if $s \geq 0$, then $s \geq t$ and $t \geq 0.$

---

Although, and this is the key point in my question, this last statement seems strange and different from the one introduced first.

$\underline{\text{Are they really equivalent$?$}}$ (and can you give some intuitive insight of that equivalence relation?) $\underline{\text{Is my work well done or has it some mistake$?$}}$

Any help is welcome!

Thank you so much in advance!

Answer 1

For each non-negative real number $s$, there exists a non-negative real number $t$ such that $s\geq t$.

1. First, we note that it is universally quantified at the start, $\forall s(\dots)$, and that the $s$ it quantifies over is greater than zero $\forall s((s\geq 0)\rightarrow\dots)$.
2. Next we note that the remaining quantifier is existential, $\forall s((s\geq 0)\rightarrow\exists t(\dots))$, and that it requires that $t$ is greater than $0$, $\forall s((s\geq 0)\rightarrow\exists t(t\geq0\dots))$.
3. Now we consider the thing it's trying to prove, ($s\geq t$), and slot that in at the end: $\forall s((s\geq 0)\rightarrow\exists t(t\geq0\land s\geq t))$
4. We can bring all the quantifiers out the front if we like: $\forall s\exists t((s\geq 0)\rightarrow(t\geq0\land s\geq t))$

Finally, we specify that we are talking about the reals, $(\forall s\in\mathbb{R})(\exists t\in\mathbb{R})[(s\geq 0)\rightarrow(t\geq0\land s\geq t)]$. In some sense this is a matter a personal preference, as we could just state that the statement refers to the reals in English, which in some, but not all cases would make the expression easier to read.

In general, when a statement is universally quantified over, the requirements that quantifier brings with it are usually of the form "if... then...". For instance, all men are mortal is written $\forall x(\text{man}(x)\rightarrow\text{mortal}(x))$. When a statement is existentially quantified over, they are of the form "... and ...". There is a dog that is red is written as $\exists x(\text{dog}(x)\land \text{red}(x))$.

---

I hope someone else can give an intuitive explanation why the statement at the start is equivalent to the one at the end. I was unable to think of a good one, feel free to post your own answer/comment which I'll advocate be accepted over mine.