Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
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
up vote 8 down vote accepted

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

share|cite|improve this answer

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.


share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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