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)
Best Answer
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.