My attempt

  1. $(\forall x.P(x))\land(\forall y.P(y) \implies Q(y))$ [premise]
  2. $\forall y.P(y) \implies Q(y)$ [$\land$ elim 1]
  3. $\forall x.P(x)$ [$\land$ elim 1]
  4. $a, P(a)$ [$\forall$ elim 3]
  5. $a, P(a) \implies Q(a)$ [$\forall$ elim 2]
  6. $Q(a)$ [$\implies$ elim 4,5]
  7. $\forall z.Q(z)$

I feel steps 4-5 is not correct, because we used a for two different expressions. I'm also not so sure about whether it's okay to go from step 6-7. Could anyone tell me whether what I did is correct and if not how I should fix it?

  • $\begingroup$ Another instance in which making the domain of quantification explicit will greatly simplify the problem. It is easy and more intutitive to prove: $\forall x: [x\in U \implies P(x)] \land [\forall y:[y \in U \implies [P(y)\implies Q(y)]]\implies \forall z:[z\in U \implies Q(z)]$. $U$ could possibly be empty as well. $\endgroup$ – Dan Christensen Aug 22 '17 at 15:44
  • $\begingroup$ If you don't want to make the domain of quantification explicit, the simplest way may be a proof by contradiction. Suppose to the contrary that $\neg Q(z)$ to obtain a the contradiction $Q(z)\land \neg Q(z)$. $\endgroup$ – Dan Christensen Aug 22 '17 at 17:50
  • $\begingroup$ The proof term for this is: $\Lambda z.f[z](p[z])$ where $p : \forall x.P(x)$ and $f: \forall y.P(y)\to Q(y)$. $\endgroup$ – Derek Elkins Aug 22 '17 at 17:56

I would justify your steps 4 and 5 with "universal instantiation" and write down that $a$ in step 5 is the same $a$ as in step 4. (If step 2 is true for all $y$, then it is certainly true with the assignment $y = a$ for the same $a$ as in step 4.) Then step 6 is modus ponens on steps 5 and 4. (Not everything is elimination.) Then step 7 is universal generalization applied to 6.

But otherwise, this seems fine.

  • $\begingroup$ Well, modus ponens is conditional elimination. $\endgroup$ – Graham Kemp Aug 22 '17 at 6:26

The universal elimination ($\forall\textsf {Elim}$) steps are that : If the statement $S(w)$ holds for any entity $w$ of the domain, then $S(a)$ holds for an arbitrary value $a$ of the domain. $$\forall w~S(w)~\vdash~ S(a)$$

The universal introduction ($\forall\textsf{Intro}$) step is likewise that : If the statement $S(a)$ holds for an arbitrary value $a$ of the domain, then $S(z)$ holds for all values $z$ of the domain. $$S(a)~\vdash~\forall z~S(z)$$

The key criteria is that you must not violate the arbitrary nature of the free variable $a$ between assumption(s) and discharge.   However, it is fine to for two universal eliminations to assume the same arbitrary value; and there is not any problem with the bound variables using different tokens.   All steps are okay.

$$\dfrac{\dfrac{\dfrac{\dfrac{\forall x~P(x)~\wedge~\forall y~(P(y)\to Q(y))}{\forall y~(P(y)\to Q(y))}{\wedge\textsf E}}{P(a)\to Q(a)}{\forall\textsf E,a}\quad\dfrac{\dfrac{\forall x~P(x)~\wedge~\forall y~(P(y)\to Q(y))}{\forall x~P(x)}{\wedge\textsf E}}{P(a)}{\forall\textsf E,a}\quad}{Q(a)}{{\to}\textsf E,a}}{\forall z~Q(z)}{\forall\textsf I,\not a}$$


You can eliminate any universal with any term you wabnt, so there is no need to introduce $a$ on line 4 or 5.

However, you do need to introduce the $a$ in order to set up the Universal Introduction rule. That is, you need to basically say: "let $a$ be an arbitrary object. By $\forall x P(x)$ it follows that $P(a)$, and by $\forall y (P(y) \rightarrow Q(y))$ it follows that $P(A) \rightarrow Q(a)$. Hence, we have $Q(a)$. But since $a$ was arbitrary, it follows that $\forall z Q(z)$"

I don't know how exactly that proof formalizes in whatever system you are using, but here is one done in Fitch:

enter image description here


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.