# A substitution inference in predicate calculus

I'm not sure what I'm missing here, but I have this lemma I am trying to prove, and it is giving me a lot of trouble. I'm technically working in ZF set theory, but this part doesn't need much more than basic predicate calculus (except for the defintion of a function). In symbols, I'd like to prove:

$$\forall x:P(x)\to Q(f(x))$$ $$\exists x:P(x)$$ $$\Rightarrow\exists y:Q(y)$$

In words, this says that if for every set $x$ that satisfies $P$ there is an associated set $y$ (which depends on $x$) which satisfies $Q$, and some set satisfies $P$, then some set also satisfies $Q$. This is intuitively obvious, as I can just find that $x$, so that the $f(x)$ associated to it satisfies $Q$, and so something satisfies $Q$. However, I'm having trouble getting from point A to point B using the axioms.

I'm working with Metamath, which has a fairly complete selection of axioms and theorems to work with, but it is still on a pretty basic level, so just make deductions you feel comfortable with, and I will tell you if I have difficulty with a hidden assumption being made.

Edit: An alternative formalization, which eliminates the function usage:

$$\forall a:P(a)\to Q$$ $$\exists x:P(x)$$ $$\Rightarrow Q$$

-

You are perhaps tripping over your own notation. The premiss you intend seems to be

$1.\quad\quad \forall x (P(x) \to Q(f(x))$

for some function $f$. You are also given

$2. \quad\quad \exists x P(x)$

So start a sub-proof by assuming

$3\quad\quad|\quad P(a)$

Then you can of course continue the proof

$4\quad\quad|\quad(P(a) \to Q(f(a))$

$5\quad\quad|\quad Q(f(a))$

But you have existential quantifier introduction in the form, if $\tau$ is a term, from $\varphi(\tau)$ you can infer $\exists \nu\varphi(\nu)$ for any [new] variable, so we have

$6\quad\quad|\quad \exists yQ(y)$

Given $\exists xP(x)$ and the subproof from (3) to (6) where the sub-proof's conclusion doesn't depend on $a$, the desired conclusion

$7\quad\quad \exists yQ(y)$

now follows by existential quantifier elimination. Job done!

-
Actually, I don't seem to be able to make that first step: Although I can go from $P(a)$ to $\exists x P(x)$, I can't go the other way (since there is no reason to believe that the wff $P(a)$, with free variable $a$, is true regardless of the value of $a$). Part of my restriction is that I can't spawn "subproofs" in this sense, nor can I use deduction to prove material implication. What would this look like if all statements were properly quantified? – Mario Carneiro Jan 5 '13 at 23:25
There is no question here of inferring $P(a)$ from $\exists xP(x)$. At line 3 a new assumption is temporarily made, to be discharged later. Of course, if you want to make life difficult for yourself by using a Hilbert-style proof system which doesn't allow subproofs, then so be it! You'll just have to (quite pointlessly!!) hack through the entirely boring details. The key thing though is that your mis-use of the variable symbol y in your first premiss was confusing you. You need a function symbol there, and then you can just do the Hilbert version of my proof. – Peter Smith Jan 5 '13 at 23:39
I think you've hit the nail on the head with your characterization of Hilbert-style proofs, and I do believe I am working with one. But the result of your subproof, if I understand correctly, is $P(a)\to\exists y Q(y)$, which I know how to derive (by similar means). But since I can't derive $P(a)$, I can't use MP, and I feel like there is still a missing generalization argument to get me there. I've simplified the problem to indicate what I mean. – Mario Carneiro Jan 5 '13 at 23:59
Looking at MetaMath, use Theorem exim 1551 – Peter Smith Jan 6 '13 at 0:12
LOL I was just writing up the solution using theorem exim. That, plus modus ponens and removal of the existential quantifier where $x$ is not free in $Q$ (thm 19.9), gets me to where I want to be. Thanks! – Mario Carneiro Jan 6 '13 at 0:21