I'm having a trouble with the understanding of how to derive logical identities of the following form:

  • $(1) \ \forall x \forall y, P \Leftrightarrow \forall y \forall x, P$
  • $(2)$ if $x$ is not free in $P$, then $$Q \wedge (\forall x, P(x)) \Leftrightarrow \forall x, (Q \wedge P(x))$$

I'm not very well-versed in logic, my motivation is pragmatic: to shorten proofs in "ordinary" mathematics. So far, I've been using them as axiom, but I wish to put and end to this.

The problem is, I've tried browsing introduction to logic and in particular to first-order logic, but they all seem to have a different focus, the one with is unhelpful to me and goes contrary to my goals.

In particular, we take $\neg, \vee$ and $\forall$ as our basic logical symbols, and define the rest of them as follows:

  • $P \wedge Q$ stands for $\neg (\neg P \vee \neg Q)$
  • $P \Rightarrow Q$ stands for $\neg P \vee Q$
  • $P \Leftrightarrow Q$ stands for $(P \Rightarrow Q) \wedge (Q \Rightarrow P)$
  • $\exists x, P$ stands for $\neg (\forall x, \neg P)$
  • 1
    I think there is a system of axioms and deduction rules that corresponds quite well to what mathematicians do. The deduction rules are called: universal instantiation, universal generalization, existential generalization and existential instantiation. With these four rules, I think you can prove pretty much anything related to quantifiers as they mimic exactly the way mathematicians do their proofs. – Keen Aug 22 '17 at 9:06
  • @Jxt921 I am unsure what your question is. You say you want to be pragmatic and shorten proofs ... so why not use these as your handy-dandy principles to do exactly that? Proving these principles would lengthen your proofs, not shorten them. I am also unclear where you are going with the end of your post ... is there a question there? – Bram28 Aug 22 '17 at 10:55
  • @Keen that seems interesting, I'll look it up and think about that. – Jxt921 Aug 22 '17 at 11:32
  • @Bram28 Well, I wanted to prove it one time and be done with this, knowing that my understanding is on a firm ground. That said, I'm not sure what "prove" should mean in this context... Concerning the end of my post, that was just to fix the notation. I think I've heard somewhere that some people take $\Leftrightarrow$ as their basic symbol instead of defining it using $\neg$ and $\vee$, which I figured could affect the way my question could be answered. – Jxt921 Aug 22 '17 at 11:35
  • @Jxt921 Ah, ok, thanks for the clarification, I get it now! OK, I'll post an Answer soon. – Bram28 Aug 22 '17 at 18:15
up vote 1 down vote accepted

There are various ways to prove these two equivalences, formally or semantically. But given the purpose of your question, let me give a somewhat informal proof that I think is fairly easy to follow conceptually yet is clear enough for your purposes:

A universal can be seen as kind of conjunction, that is, if $a,b,c,...$ denote the objects in your domain, then you can think of a universal like this:

$$\forall x \: P(x) \approx P(a) \land P(b) \land P(c) \land ...$$

So, if we have two universal quantifiers, we would get:

$$\forall x \forall y \ P(x,y) \approx$$

$$ \forall y \ P(a,y) \land \forall y \ P(b,y) \land \forall y \ P(c,y) \land ... \approx$$

$$(P(a,a) \land P(a,b) \land P(a,c) ..) \land (P(b,a) \land P(b,b) \land P(b,c) ..) \land (P(c,a) \land P(c,b) \land P(c,c) ..) \Leftrightarrow \text{(Reorder)}$$

$$(P(a,a) \land P(b,a) \land P(c,a) ..) \land (P(a,b) \land P(b,b) \land P(c,b) ..) \land (P(a,c) \land P(b,c) \land P(c,c) ..) \land ... \approx$$

$$\forall x \ P(x,a) \land \forall x \ P(x,b) \land \forall x \ P(x,c) \land ... \approx$$

$$\forall y \forall x \ P(x,y)$$

Again, it's a little informal, but you see that the equivalence $\forall x \forall y \ P(x,y) \Leftrightarrow \forall y \forall x \ P(x,y)$ follows from the fact that the conjunction is associative and commutative. Similarly, you can regard an existential as a disjunction, and by the associativity and commutativity of the disjunction prove $\exists x \exists y \ P(x,y) \Leftrightarrow \exists y \exists x \ P(x,y)$

So, we have as a general equivalence principle:

Swapping Quantifiers of the Same Type That Are Next to Each Other

Where $Q$ is some quantifier:

$Q x Q y \ P(x,y) \Leftrightarrow Q y Q x \ P(x,y)$

And yes, they really need to be of the same type, since $\forall x \exists y \ P(x,y) \not \Leftrightarrow \exists y \forall x \ P(x,y)$. If you write out the quantifiers as conjunctions and disjunctions as suggested, you'll see why the equivalence does not hold, but as a simple counterexample: everyone loves someone is not the same as there is someone who loves everyone.

And yes, they also need to be right next to each other, e.g. $\forall x \exists y \forall z \ P(x,y,z) \not \Leftrightarrow \forall z \exists y \forall x \ P(x,y,z)$

By the way, I was assuming that both $x$ and $y$ occur in the formula $P$, which is why I wrote it as $P(x,y)$. If any of them do not occur in $P$, then you can simply drop the quantifier. That is, we can also prove the principle of:

Null Quantification

Where $Q$ is some quantifier and where $x$ does not occur free in $P$:

$Qx P \Leftrightarrow P$

Which makes sense from the conjunction/disjunction point of view as well: If we have $\forall x P$, and if $P$ does not have $x$ as a free variable, we basically just get $P \land P \land P \land ...$, and that is of course just $P$. For the existential we would get $P \lor P \lor P \lor ...$, which is also just $P$.

Finally, we can show your 2). Now, I think you meant to say 'If $x$ is not free in $Q$ ...', but actually in your case it doesn't matter, since if $x$ is free in $Q$ we have the following equivalence principles:

Distribution Universal over Conjunction, and Existential over Disjunction

$\forall x (P(x) \land Q(x)) \Leftrightarrow \forall x \ P(x) \land \forall x \ Q(x)$

$\exists x (P(x) \lor Q(x)) \Leftrightarrow \exists x \ P(x) \lor \exists x \ Q(x)$


$$\forall x (P(x) \land Q(x)) \approx$$

$$(P(a) \land Q(a)) \land (P(b) \land Q(b)) \land (P(c) \land Q(c)) \land ... \Leftrightarrow \text{(Reorder)}$$

$$(P(a) \land P(b) \land P(c) \land ...) \land (Q(a) \land Q(b) \land Q(c) \land ... \approx$$

$$\forall x \ P(x) \land \forall x \ Q(x)$$

(Similar for $\exists x (P(x) \lor Q(x)) \Leftrightarrow \exists x \ P(x) \lor \exists x \ Q(x)$)

And if $x$ is not free in $Q$, we simply do:

$$\forall x (P(x) \land Q) \approx$$

$$(P(a) \land Q) \land (P(b) \land Q) \land (P(c) \land Q) \land ... \Leftrightarrow \text{(Reorder)}$$

$$(P(a) \land P(b) \land P(c) \land ...) \land (Q \land Q \land Q \land ... \Leftrightarrow$$

$$(P(a) \land P(b) \land P(c) \land ...) \land Q \approx$$

$$\forall x \ P(x) \land Q$$

Or, using the earlier established equivalences:

$$\forall x (P(x) \land Q) \Leftrightarrow \text{(Distribution } \forall \text{ over } \land )$$

$$\forall x P(x) \land \forall Q \Leftrightarrow \text{( Null Quantification)}$$

$$\forall x \ P(x) \land Q$$

Note that we do not have that the universal distributes over the $\lor$ or that the Existential distributes over the $\land$, and again, if you rewrite in terms of conjunctions and disjunctions, you'll see why. As a simple counterexample though: Saying that every natural number is even or odd is not the same as saying that either every natural numbers is even, or every natural number is odd. So, in general, $\forall x (P(x) \lor Q(x)) \not \Leftrightarrow \forall x \ P(x) \lor \forall x \ Q(x)$ and $\exists x (P(x) \land Q(x)) \not \Leftrightarrow \exists x \ P(x) \land \exists x \ Q(x)$

However, if $x$ is not free in $Q(x)$, then the following does hold:

Prenex Laws (well, some of them)

Where $x$ is not a free variable in $Q$:

$\forall x (P(x) \lor Q) \Leftrightarrow \forall x \ P(x) \lor Q$

$\exists x (P(x) \land Q)\Leftrightarrow \exists x \ P(x) \land Q$


$$\forall x (P(x) \lor Q) \approx$$

$$(P(a) \lor Q) \land (P(b) \lor Q) \land (P(c) \lor Q) \land ... \Leftrightarrow \text{(Distribution } \lor \text{ over } \land)$$

$$(P(a) \land P(b) \land P(c) \land ...) \lor Q \approx$$

$$\forall x \ P(x) \lor Q$$

I'm not very well-versed in logic, my motivation is pragmatic: to shorten proofs in "ordinary" mathematics. So far, I've been using them as axiom, but I wish to put and end to this.

The problem is, I've tried browsing introduction to logic and in particular to first-order logic, but they all seem to have a different focus, the one with is unhelpful to me and goes contrary to my goals.

I feel that you are looking for a general method of proving mathematical statements. So I will not offer a proof for a specific statement in your question, but I would if you want to.

Proof methods differ in degree of formality:

  • computerized proofs in formal languages are the most precise and reliable form,

  • informal proofs in natural languages found in books and articles.

Textbooks on logic fall into the following categories.

  • Practical logic, also known as proof writing. It is concerned with notations for proofs (textual or graphical), their practical advantages, techniques for inventing proofs. Actually, the word “logic” is rare in their titles. They would be titled “How to prove it”, “Introduction to advanced mathematics”, or “Introduction to mathematical thinking”. More often practical logic is just injected into a preliminary chapter in a textbook on another branch of mathematics: linear algebra, analysis, set theory, topology, whatever.

  • Theoretical logic, also known as metamathematics. It is study of logical systems as mathematical objects which reveals their properties and compare them. If a textbook has a title containing the word “logic” and is not written for philosophy students, the textbook is likely on theoretical logic.

I suppose you need a textbook on practical logic, but you encountered textbooks on theoretical logic. Unfortunately, textbooks on practical logic teach logic informally, and their proof methods are not much better than just accepting logical truths as axioms. Textbooks on theoretical logic comply to high standards of formality, but contain no practical examples, and described logical systems are more suited for theoretical investigation. I am yet to find a textbook or online course on practical logic that satisfies me, so I just give guidelines on what to look for.

  • Practical proof systems are called “natural deduction”. “Natural” for humans. First natural deduction systems were invented by Gentzen and Jaśkowski.

  • A proof consists of applications of inference rules. They are the smallest steps, the first principles. A logical system is a language for writing mathematical statements and a set of inference rules. The Wikipedia article on natural deduction contains a good sample of inference rules. The article is not sufficient for learning logic though. If a logical system contains, say, 2 times more inference rules, it is likely redundant, bloated.

  • Proofs depicted as trees are more readable than lists (of statements). A specific graphical format is called “Fitch notation” or “flag notation”.

  • Do not study logical systems with a small number (2) of primitive logical connectives. For example, thinking of $A\land B$ as $\lnot(A\to\lnot B)$ is quite unintuitive. In practice, we use all connectives anyway. I recommend a system where $\to, \land, \lor, \top, \perp$ are primitive and $\leftrightarrow, \lnot$ are defined via other logical connectives. So it should contain inference rules for all primitive logical connectives.

  • Logic is not sufficient for expressing all mathematical notions. A method of “constructing” mathematical objects like sets, functions, or relations is needed, and it is added on top of logic. Options are set theory and type theory. Set theory is more popular; you can find plenty of textbooks. Grappling with formal set theory is hard. If you want to be formal, go for a variant of type theory like Calculus of Inductive Constructions.

Your Answer


By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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