# How does one prove a generalised conditional statement?

I'm trying to prove a statement of the form ∀x: P(x) → Q(x). Apparently the way to do it is to prove that Q(x) for some x such that P(x), assuming that x is arbitrarily chosen, and hence discharge the assumption and infer that the statement is true. I'm not sure how x can be arbitrary, given that it is bound (i.e. for the purpose of this proof, x ∈ {x | P(x)}) and I don't see how essentially proving that ∃x: P(x) ∧ Q(x) entails that ∀x: P(x) → Q(x). What am I missing?

This is called ∀-introduction or generalisation. It is not related to the conditional in the body of the quantifier (i.e., you can also apply it to ∀x:P(x)). If you can prove that P(x) for arbitrary x, then it must be true for all x.

When proving a conditional P(x) → Q(x) you assume P(x), because the case that ¬P(x) is trivially true (since a conditional with false antecedent is always true). So the assumption that P(x) is not really a restriction on the arbitrarily chosen x, it is rather the next step in the proof.

If it helps, you don't have to assume P(x) to prove P(x) → Q(x). You can also use the law of excluded middle:

For arbitrary x, either P(x) or ¬P(x).
(a) If P(x), then ... so Q(x). Hence, P(x) → Q(x).
(b) If ¬P(x), then P(x) → Q(x) is trivially true.
Therefore, P(x) → Q(x).

If you want to prove the universal, you can continue with:

Since P(x) → Q(x) for arbitrary x, we can conclude ∀x: P(x) → Q(x).

@Keelan is right, but let me belabor the main point a little.

It is not "There exists x such that P(x) implies Q(x)" you are proving. It is the open, un-quantified statement "P(x) implies Q(x)", which means the same thing in raw propositional logic as the universally quantified statement does in the full logic.

By using only the rules about x, forced upon it by P, and not the details of x's instantiation, you are stepping back from the full logic with actual elements into propositional logic, of which the full logic is a refinement. Raw propositional logic still works the same way it did before you introduced quantifiers.

In fact by proving the statement with the free variable x, you do not establish or require that any x exists. There is no problem picking an x that does not exist. You can still prove that "For all x P(x) implies Q(x)" when there is no x such that P(x) ever occurs. As he notes, it is trivially true in that case, but it is true.

The fact you are talking about this element by name, and imagine it as an instance is just a conceptual crutch, not a part of the actual logic. What you are really handling, when you talk about this fully-general element is the free variable x, which is constrained by what you know about P.