Derivable rules with quantifiers in first-order logic

Question

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)$

Answer 1

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)$

'Proof':

$$\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$

'Proof':

$$\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$$

Answer 2

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.