# Thread:

1. ## Proper use of Universal Instantiation

Is this a proper use of universal instantiation? If not, how could this proof be corrected?

Suppose:

$\forall x P(x) \rightarrow \exists x Q(x)$

Prove:

$\exists x (P(x) \rightarrow Q(x))$

Proof:

$y$ is arbitray, so $P(y)$
$P(y)$, so choose a $z_{0}$ such that $Q(z_{0})$
By universal instantiation let $y = z_{0}$.
Therefore $P(z_{0}) \rightarrow Q(z_{0})$.
$\square$

2. Originally Posted by Ontolog
Is this a proper use of universal instantiation?
No, it's not.

$y$ is arbitray, so $P(y)$
It seems that you start with ∀x P(x) and instantiate x with y. However, ∀x P(x) is not given: it is an assumption of an assumption and thus has to be proved. It is also not clear why you need to instantiate x since you can immediately derive ∃x Q(x) by MP and from there derive the conclusion.

If, on the other hand, you assume P(y), then you can conclude ∀x P(x) because the assumption contains y free. Also, it is not clear where you close the assumption P(y).

To say something more precise, you have to say what formalism you are using, even informally (e.g., natural deduction or sequent calculus).

This conclusion can't be proved without the law of excluded middle. Suppose that ∀x P(x) is true. Then ∃x Q(x) from the assumption, and so ∃x (P(x) -> Q(x)). If ∀x P(x) is false, then there exists an x0 such that P(x0) is false. Therefore, P(x0) -> Q(x0) is true.

3. Originally Posted by emakarov
No, it's not.

It seems that you start with ∀x P(x) and instantiate x with y. However, ∀x P(x) is not given: it is an assumption of an assumption and thus has to be proved.
I can see this, yes I should have added another assumption that $\forall x P(X)$.

Originally Posted by emakarov
It is also not clear why you need to instantiate x since you can immediately derive ∃x Q(x) by MP and from there derive the conclusion.

If, on the other hand, you assume P(y), then you can conclude ∀x P(x) because the assumption contains y free. Also, it is not clear where you close the assumption P(y).
Yes, I can see that by assuming $\forall x P(x)$ I wouldn't need to instantiate x to derive $\exists x Q(x)$. However, wouldn't I need to instantiate x to show that $\exists x(P(x) \rightarrow Q(x))$, since in this expression we are saying that the x for which P(x) is the same as the x for which Q(x).

Originally Posted by emakarov
To say something more precise, you have to say what formalism you are using, even informally (e.g., natural deduction or sequent calculus).
This is something I have been unclear on. I am studying from a book "How To Prove It" (Vellemen 2006) and I am (attempting to) use the formalism presented there. I believe it is "first-order logic."

Originally Posted by emakarov
This conclusion can't be proved without the law of excluded middle. Suppose that ∀x P(x) is true. Then ∃x Q(x) from the assumption, and so ∃x (P(x) -> Q(x)).
I don't follow this argument for the same reason I mentioned earlier. To show that $\exists x(P(x) \rightarrow Q(x))$ is true, don't we need to demonstrate that the x for which P(x) is the same as the x for which Q(x)?

Originally Posted by emakarov
If ∀x P(x) is false, then there exists an x0 such that P(x0) is false. Therefore, P(x0) -> Q(x0) is true.
Again I can't follow. Where is it shown that $\lnot Q(x0)$?

$\forall A x P(x) \rightarrow \exists x Q(x)$

Therefore, by modus tollens:

$\lnot \exists x Q(x) \rightarrow \lnot \forall A x P(x)$

But the converse is not necessarily true:

$\lnot \forall A x P(x) \rightarrow \lnot \exists x Q(x) ?$

I realize that there must be something blindingly obvious that I'm missing here so please bear with me!

4. Originally Posted by Ontolog
Suppose:
$\forall x P(x) \rightarrow \exists x Q(x)$

Prove:
$\exists x (P(x) \rightarrow Q(x))$
Is the above the exact statement of the exercise as it appears in the mentioned textbook?
From read his solution, it does not appear to be the complete quote.

5. Originally Posted by Plato
Is the above the exact statement of the exercise as it appears in the mentioned textbook?
From read his solution, it does not appear to be the complete quote.
OK, some context for how this problem came up. In the book there is a straightforward exercise:

Prove that if $\exists x (P(x) \rightarrow Q(x))$ is true, then $\forall x P(x) \rightarrow \exists x Q(x)$ is true.

Then there is a note that "The other direction of the equivalence is quite a bit harder to prove. See exercise 29 of Section 3.5", where we find the problem:

Prove that if $\forall x P(x) \rightarrow \exists x Q(x)$ then $\exists x (P(x) \rightarrow Q(x))$.

And just as I look up the original problem text I find that the author gives a hint: "Remember that $P \rightarrow Q$ is equivalent to $\lnot P \lor Q$." Which is something I'll have to think about...

6. The hint suggests considering the case ~AxPx and the case ExQx. Show that in either case we have Ex(Px -> Qx).

7. Originally Posted by Ontolog
I don't follow this argument for the same reason I mentioned earlier. To show that $\exists x(P(x) \rightarrow Q(x))$ is true, don't we need to demonstrate that the x for which P(x) is the same as the x for which Q(x)?
Recall that an implication is true iff the conclusion is true (regardless of the premise) or the premise is false (regardless of the conclusion).

Suppose ∀x P(x) is true, which also means that ∃x Q(x) is true. Fix x0 that makes Q true. Then P(x0) -> Q(x0) is true regardless of whether P(x0) is true or not. Similarly, if ∀x P(x) is false, suppose P(x0) is false. Then P(x0) -> Q(x0) is true regardless of whether Q(x0) is true.

8. Originally Posted by emakarov
Recall that an implication is true iff the conclusion is true (regardless of the premise) or the premise is false (regardless of the conclusion).

Suppose ∀x P(x) is true, which also means that ∃x Q(x) is true. Fix x0 that makes Q true. Then P(x0) -> Q(x0) is true regardless of whether P(x0) is true or not. Similarly, if ∀x P(x) is false, suppose P(x0) is false. Then P(x0) -> Q(x0) is true regardless of whether Q(x0) is true.
I understand now. I suppose there are some alternative systems of logic that treat implications differently? Because intuitively, an implication is defined by a premise and a consequence which follows from that premise. In fact, I wonder how many typical proofs in mathematics make use of the fact that if Q(x) then $P(x) \rightarrow Q(x)$ for any P and x. In other words, is this merely an idiosyncrasy of first-order logic or does it have any practical implications? (No pun intended )

9. Originally Posted by Ontolog
I wonder how many typical proofs in mathematics make use of the fact that if Q(x) then $P(x) \rightarrow Q(x)$ for any P and x. In other words, is this merely an idiosyncrasy of first-order logic or does it have any practical implications?
The statement that $A\subseteq B$ means that $\left( {\forall x} \right)\left[ {x \in A \to x \in B} \right]$.

We use the to say in the class of sets $\left( {\forall C} \right)\left[ {\emptyset \subseteq C} \right]$.

10. Yes, without the rule that true conclusion makes the whole implication true we would not be able to say general facts whose converse is false, both in mathematics and in real life. An example from Wikipedia:
Being at least 30 years old is necessary of serving in the U.S... That is, if you are a senator, it follows that you are at least 30 years old.
The converse of the intermediate value theorem is false: roughly speaking, if for all a, b and every u between f(a) and f(b) there exists a c such that f(c) = u, it does not follow that f is continuous.

Still another example: If f : A -> B and g : B -> C are injections, then so is the composition g o f, but not conversely (if g o f is injective, then so is f, but not necessarily g).

Other concepts of implications have been considered in philosophy and logic. See this Wikipedia section, for example. You can probably find a lot of information in the Stanford Encyclopedia of Philosophy.

11. Originally Posted by Plato
The statement that $A\subseteq B$ means that $\left( {\forall x} \right)\left[ {x \in A \to x \in B} \right]$.

We use the to say in the class of sets $\left( {\forall C} \right)\left[ {\emptyset \subseteq C} \right]$.
That's very interesting! I worked it out and have seen that it is true, so I think I'm starting to absorb this concept of "rigorously defined" logical implication. Thanks!

12. Originally Posted by emakarov
Yes, without the rule that true conclusion makes the whole implication true we would not be able to say general facts whose converse is false, both in mathematics and in real life. An example from Wikipedia:

The converse of the intermediate value theorem is false: roughly speaking, if for all a, b and every u between f(a) and f(b) there exists a c such that f(c) = u, it does not follow that f is continuous.

Still another example: If f : A -> B and g : B -> C are injections, then so is the composition g o f, but not conversely (if g o f is injective, then so is f, but not necessarily g).

Other concepts of implications have been considered in philosophy and logic. See this Wikipedia section, for example. You can probably find a lot of information in the Stanford Encyclopedia of Philosophy.
Fascinating Thanks for the link to that Wikipedia section, it basically laid out precisely the concerns I had with logical implication. I think my problem is that I get too philosophical when I should be more "hyper-literal" when dealing with mathematics. I'm slowly starting to get it. Thanks for all your help so far!
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 38, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9469203352928162, "perplexity_flag": "middle"}