# Distributivity of quantifiers over logical connectives

I'm given the following expresssion: $$\forall a [\phi(a) \to \psi(a)] \wedge \forall a [\psi(a) \to \phi(a)]$$ that I wish to logically reduce to: $$\forall a [\phi(a) \leftrightarrow \psi(a)]$$

The only area I'm uncertain about is showing that universal quantification is distributive over conjunction, as trivial as it seems. Rather, I'm not sure where to find theorems or lemmas related to the topic. The set theory text from which this comes provides no insight and the introductory logic text I own also doesn't touch on the matter, at least in any great detail.

-
It is based on the trivial notion that $$\forall a P(a) \wedge \forall a Q(a) \rightarrow \forall a (P(a) \wedge Q(a))$$ – Dan Christensen Jan 2 '13 at 16:31

Given $$\forall x [\phi(x) \to \psi(x)] \wedge \forall x [\psi(x) \to \phi(x)]$$ eliminating the conjunction, you can infer $$\forall x [\phi(x) \to \psi(x)]$$ $$\forall x [\psi(x) \to \phi(x)]$$ Now use UE, universal quantifier elimination, to instantiate the quantifiers using an arbitrary parameter '$a$' to get $$\phi(a) \to \psi(a)$$ $$\psi(a) \to \phi(a)$$ whence, introducing the biconditional, $$\phi(a) \leftrightarrow \psi(a)$$ But $a$ is indeed arbitrary so we can use UI, universal quantifier introduction, to get $$\forall x[\phi(x) \leftrightarrow \psi(x)].$$ So, here we've just used the standard rules for the universal quantifier, plus the relevant rules for propositional connectives. Any standard logic text should be able to help here: Paul Teller's reliable and accessible Modern Formal Logic Primer is freely available at http://tellerprimer.ucdavis.edu

-

$$\forall a [\phi(a) \to \psi(a)] \wedge \forall a [\psi(a) \to \phi(a)],$$ relabel $$\forall a [\phi(a) \to \psi(a)] \wedge \forall b [\psi(b) \to \phi(b)],$$ move under the first quantifier $$\forall a [\phi(a) \to \psi(a) \wedge \forall b [\psi(b) \to \phi(b)]],$$ eliminate the quantifier by instantiating with $b = a$, $$\forall a [\phi(a) \to \psi(a) \wedge \psi(a) \to \phi(a)].$$
dtldarek: Exactly what rule is being invoked at your final step? You need to restrict it carefully, as you can't generally do this sort of quantifier elimination. For example, $\forall a(\forall b\varphi(b) \to \psi(a))$ does not imply $\forall a(\varphi(a) \to \psi(a))$. – Peter Smith Jan 2 '13 at 8:43
@PeterSmith Yep, but in your formula $FV(\forall b.\ \phi(b) \to \psi(a)) \cap \{a\} \neq \varnothing$. This is possible only because here those two are independent, and in fact the third step (moving inside) also depends on this. If I were to formalize this (draw the derivation tree), I think I would end up with your solution anyway. However, such lemmas (quantifier elimination somewhere inside) are useful if you had proven them before. This one is intuitive enough so there's no need to write out every detail. – dtldarek Jan 2 '13 at 12:46
@PeterSmith And, of course, one need a positive context, e.g. $\forall a.\ (\forall b.\ \phi(b)) \to \psi(a)$ also doesn't imply $\forall a.\ \phi(a) \to \psi(a)$. In a negative context you could do an existential quantifier elimination: $\forall a.\ (\exists b.\ \phi(b)) \to \psi(a)$ implies $\forall a.\ \phi(a) \to \psi(a)$ given that $FV(\phi(b)) \cap \{a\} = \varnothing$. – dtldarek Jan 2 '13 at 12:58