I was reading page 10-8 of this: https://faculty.washington.edu/smcohen/120/Chapter10.pdf and I was wondering if the distributive qualities could be derived, e.g. $\forall x (P \lor Q(x)) \Leftrightarrow P \lor \forall x Q(x)$, and the equivalent one for $\exists , \land$.

  • $\begingroup$ In the Lecture Notes of the website there are (in the chapters following the one tou are referencing) the rules for quantifiers : $\forall$-intro, $\forall$-elim,... They must be used to prove the theroem above. $\endgroup$ Jun 29, 2014 at 8:00

2 Answers 2


The following proof uses the rules of Chapter 12: Methods of Proof for Quantifiers.

I'll consider only the case : $∀x(P∨Q(x)) \Rightarrow P∨∀xQ(x)$; the other one is similar.

(1) $∀x(P∨Q(x))$ --- assumed

(2) $P∨Q(a)$ --- from (1) by universal instantiation, or $\forall$-elim

Now we need some "propositional" transformation : we use the equivalence between $A \lor B$ and $\lnot A \Rightarrow B$

(3) $\lnot P \Rightarrow Q(a)$ --- from (2) by tautological equivalence

(4) $\lnot P$ --- assumed

(5) $Q(a)$ --- by $\Rightarrow$-elim (or modus ponens)

(6) $\forall xQ(x)$ --- by universal introduction (or $\forall$-intro) : the constant $a$ is not free in the assumptions

(7) $\lnot P \Rightarrow \forall xQ(x)$ --- from (4) and (6) by $\Rightarrow$-intro

(8) $P \lor \forall xQ(x)$ --- from (7) by tautological equivalence

(9) $∀x(P∨Q(x)) \Rightarrow P \lor \forall xQ(x)$ --- from (1) by $\Rightarrow$-intro.


If we don't want to use the tautological equivalence in steps (3) and (8), we can use a "proof by cases".

From step :

(2) $P \lor Q(a)$

(3) $P$ --- assumed for $\lor$-elim

(4) $P \lor \forall x Q(x)$ --- from (3) by $\lor$-intro

(5) $Q(a)$ --- assumed for $\lor$-elim

(6) $\forall xQ(x)$ --- by universal introduction (or $\forall$-intro) : the constant $a$ is not free in the assumptions

(7) $P \lor \forall x Q(x)$ --- from (6) by $\lor$-intro

(8) $P \lor \forall x Q(x)$ --- from (2), (4) and (7) by $\lor$-elim, "discharging" the temporary assumptions (3) and (5).

Theorem follows as above, by $\Rightarrow$-intro.


The other "direction" is easier.

From the assumption : $P \lor \forall x Q(x)$, we derive from both $P$ and $\forall xQ(x)$ separately : $P \lor Q(a)$ [in one case by $\lor$-intro; in the other case by $\forall$-elim followed by $\lor$-intro].

Then we apply again proof by cases ($\lor$-elim) to conclude from : $P \lor \forall x Q(x)$ to : $P \lor Q(a)$.

Finally we apply $\forall$-intro to derive : $\forall x(P \lor Q(x))$ followed by a final $\Rightarrow$-intro.


Please note that, in general : $\forall xP(x) \lor \forall xQ(x) \vdash \forall x(P(x) \lor Q(x))$, but not vice versa, i.e. :

$\forall x(P(x) \lor Q(x)) \nvdash \forall xP(x) \lor \forall xQ(x)$.

In other words, the above proof does not works if $x$ is free in $P$.

Why so ?

Because (consider the first proof above) in step (6) we have to apply $\forall$-intro to $Q(a)$ to get $\forall xQ(x)$.

If $x$ is free in $P$ [and this is so if we try to apply the proof to the assumption $\forall x(P(x) \lor Q(x))$, because in step (2) we have instantiated it to $P(a) \lor Q(a)$], if we try to apply $\forall$-intro we have to violate the proviso that the constant $a$ must not be free in the assumptions, and at that step of the proof we still have an "undischarged" assumption containing $a$ : exactly $P(a)$.

  • $\begingroup$ Why can you assume $\neg P$ in step 4? $\endgroup$
    – user82004
    Jun 29, 2014 at 9:26
  • $\begingroup$ @Anthony - We can assume whatever we need, provided that we "discharge" it before the end of the proof, if - as in this case - we are proving a logical theorem, i.e. a valid formula which does not depend on assumptions. $\endgroup$ Jun 29, 2014 at 10:06
  • $\begingroup$ But don't you need to consider the situation where P is true as well? Or is it because the only thing you're really interested in with an implication is what happens when the antecedent is true? $\endgroup$
    – user82004
    Jun 29, 2014 at 20:38

It doesn't seem like the notes you're reading define any deductive system for FOL at all, and you can't derive anything before you have a deductive system to do it in.

However, once you have a deductive system for FOL (of which there are several to choose among), you will be able to derive these laws in it. Otherwise the system you have is not FOL!

  • $\begingroup$ Oof. I'm not sure what deductive system I normally use, I just was trying to figure out why Null Quantification makes sense. $\endgroup$
    – user82004
    Jun 29, 2014 at 2:33
  • $\begingroup$ @Anthony: If you're just trying to gain an intuitive understanding of why the rules hold, I think that's easier by thinking about the semantics rather than about derivations of them. To wit, in each possible world, $P$ is either true or false. So, depending on which of those is the case, the content of the rule is either $$\forall x({\sf True}\lor \cdots)\Leftrightarrow {\sf True}\lor \cdots$$ or $$\forall x(Q(x))\Leftrightarrow \forall x\,Q(x)$$ each of which is clearly always true. $\endgroup$ Jun 29, 2014 at 2:38
  • $\begingroup$ I suppose I did want more than intuition though- derivations are always nice. There are a few other cases to consider, no? $\endgroup$
    – user82004
    Jun 29, 2014 at 2:49
  • $\begingroup$ @Anthony: The semantics of FOL can (and should) be formalized; it is not just intuitive handwaving. And I don't see which other cases there would be to consider. (The rules are only valid if $P$ does not contain $x$ free, and therefore in any given interpretation $P$ has the same truth value no matter which value $x$ is considered to have). $\endgroup$ Jun 29, 2014 at 2:56

Your Answer

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