"$\forall x$ s.t. $\phi(x), \exists y$ s.t $\phi'(x,y)$" versus "$\forall x, \big( \phi(x)\implies \exists y $ s.t $\phi'(x,y)\big)$"

Question

I am trying to gain some insight into how one understands proofs that can be generically described as fitting this mold:

Let $x$ be some object that has a specific list of properties. Show that some other object $y$ exists with a specific property that relates to $x$.

(An example of such a proof that follows this form can be found here: Proof of a proposition about recursion definition (Terence Tao's Analysis I)).

To tackle such a proof, I would do the following:

Firstly, I would note that this statement can be formally restated as:

$$\forall x \text{ such that } \phi(x), \exists y \text { such that } \phi'(x,y)$$

Then, I would pick an arbitrary element $x^*$ that satisfies $\phi(x^*)$. From this, I would try to construct a corresponding $y^*$ that satisfies $\phi'(x^*,y^*)$.

Because $x^*$ was arbitrary, I have thus proven that "$\forall x \text{ such that } \phi(x), \exists y \text { such that } \phi'(x,y)$" is a true statement.

I believe this is the standard strategy.

---

I have always wondered how (and if) the aforementioned strategy can be reformulated using implications. An author of an "Answer Post" from a question posed here (Conceptual question about assuming the existence of a function in order to prove the existence of another function) made the following (paraphrased) comment:

The "such that $\phi(x)$" statement can actually be reformulated as an antecedent of an implication. Additionally, the "$\exists y \text{ such that } \phi'(x,y)$" can be reformulated as the consequent of the same implication. Therefore, "$\forall x \text{ such that } \phi(x), \exists y \text { such that } \phi'(x,y)$" is actually logically equivalent to "$\forall x, \big( \phi(x)\implies \exists y \text { such that } \phi'(x,y)\big) $."

Could some please elaborate on this a little more?

Edit: The proper format may actually be "$\forall x, \exists y \big( \phi(x)\implies \phi'(x,y)\big) $"

(however I am not sure)

Answer 1

The exact same strategy works for the reformulated statement, since they're equivalent. If you want to prove $$\forall x(\phi(x)\implies \exists y,\phi'(xy))$$ what do you do? Pick an arbitrary $x$ such that $\phi(x)$ holds and then try to find a $y$ such that $\phi'(x,y)$ holds, or show that the non-existence of such a $y$ would lead to a contradiction.

If you try to state them in words, both statements mean something like, "Any time we have an $x$ such that $\phi(x)$ holds, there is a $y$ such that $\phi'(x,y)$ holds."

Formally, the second alternative you give $$\forall x, \exists y \big( \phi(x)\implies \phi'(x,y)\big)$$ means the same thing, but it seems a little unnatural to me. However, I'm by no means a logician.

Answer 2

Short answer : mathematical symbolism sometimes conceals conditional form in the same manner as natural language does ; in a proof, the proper conditional form of the goal has to be recovered in order to adopt the right strategy ( consistng in assuming the antecedent , in order to derive the consequent, under the initial assumption).

---

• The question is a grammatical one, and amounts to asking how to formalize sentences such as :

[ Every X + relative clause] + Verb + Attribute / Object.

[ An X + adjective} + Verb + Attribute/ Object.

[ An X + participle clause] + Verb + Object/ Attribute

All these grammatical forms are abbreviating devices used by natural language; logic teaches us that the logical structure ( beyond the surface grammar form) involves a conditional.

• The point is that, mathematics also uses this abbreviating device. Sometimes, a change in typography ( with the use of indices) accompanies this sort of writing.

For example, in order to say ( note the relative clauses below) :

For all $\epsilon$ that is strictly greater than 0, there is a $\delta$ that is strictly greater than 0, such that if ($0 < | x-a| < \delta$) then ($ | f(x)-L| < \epsilon$)

one will write

$\forall\epsilon_{(>0)}\exists \delta_{(>0)} [(0 < | x-a| < \delta)\rightarrow ( | f(x)-L| < \epsilon)]$.

But this is an abbreviation, and in fact, it " hides" a conditional form: for all $\epsilon$ , if $\epsilon$ is strictly greater than 0, then, there exists some $\delta$ such that, if.... then... .

• So how to formalize?

[ Every X + relative clause] + Verb + Attribute / Object.

Every natural number that is different from 0 is the successor of some natural number.

$\forall (x) {[ (x\in\mathbb N) \wedge (x\neq0)] \rightarrow [\exists (y) (y\in\mathbb N) \wedge (x=S(y)]}$

or

$\forall (x)_{ (x\in\mathbb N)} [ (x\neq0) \rightarrow (\exists (y) (y\in\mathbb N) \wedge (x=S(y)) ] $

[ An X + adjective} + Verb + Attribute/ Object.

Every even integer has an even square.

$\forall(x) [( x \in \mathbb Z \wedge x/2\in\mathbb Z) \rightarrow ( x^2 / 2 \in \mathbb Z)] $

[ An X + participle clause ] + Verb + Object/ Attribute

All sets having no element are identical ( with |A| = cardinal of set A) :

$\forall (S)(T) [ (|S|=0 \wedge |T| = 0 ) \rightarrow ( S=T)$]

Note : there are certainly some parenthesis mistakes I haven't corrected.