Distributivity of quantifiers over logical connectives

Question

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.

Answer 1

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

Answer 2

Peter's answer is fine, another approach might be as follows. Start with

$$ \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)]. $$

There is no way to skip the elimination (you start with two quantifiers and want to arrive at one), but this way you don't need to deal with any unbound variables, parameters or special constants.

Cheers!