Quantifiers

Table of contents

1. Introduction
2. Quantifiers

Introduction

In the previous lesson we introduced predicates. In this lesson, we are going to see how we can express statements in logic using quantifiers. We will introduce two quantifiers, the universal and the existential quantifiers. There is a ton of commentary in the Lean Lab about predicate logic (which are further explained in the M/W lectures), and we don’t want to repeat the fundamental notions here. So we will keep the lessons short and more about the subtleties of predicate logic.

Quantifiers

The Idea

What makes first-order predicate logic powerful is that it allows us to make assertions using quantifiers¹. Consider the following examples:

• Every natural number is even or odd, but not both.
• If some natural number, $n$, is even, then so is $n^2$.

Let’s try to formalize these: First, we introduce the predicates $E \maps \mathbb{N} \to \props$ and $O \maps \mathbb{N} \to \props$ for “being even” and “being odd”, respectively. The first sentence then states that for every individual $n$ of the domain $\mathbb{N}$ of natural numbers, it is the case that $E(n) \lor O(n)$ but not $E(n) \land O(n)$. To express the phrase “for every” we introduce the universal quantifier $\forall$: The symbol $\forall$ followed by a variable $x$ is meant to represent the phrase “for every $x$”. In other words, it asserts that every value of $x$ has the property that follows it. A complete formalization of the first sentence is given by the formal sentence \[ \forall n : \mathbb{N} \; (E(n) \lor O(n)) \land \neg (E(n) \land O(n)) \, .\]

Similarly, a complete formal sentence of the second example above is given by \[ \forall n : \mathbb{N} \; (E(n) \To E(n^2)) \, . \]

Challenge

Write a formal sentence corresponding to each of the sentences in below:

• A natural number is even if and only if it is divisible by two.
• A natural number $n$ is odd if and only if $n+1$ is even.
• If a natural number, $n^2$, is even, then so is $n$.
• Any prime number that is greater than $2$ is odd.
• $\sqrt{2}$ is irrational.
• The Green-Tao theorem.
• The Fermat’s Last Theorem.

To be concise, it is common to combine multiple quantifiers of the same kind: For instance consider the following formalization of the sentence “For any three natural numbers $k$, $m$, and $n$, if $k$ divides $m$ and $m$ divides $n$, then $k$ divides $n$”:

\[ \forall k : \N, \forall m : \N, \forall n : \N \; (D(k,m) \wedge D(m,n) \to D(k,n)) \]

In above the predicate $D(x,y)$ denotes that $x$ divides $y$. We can combine all $\forall$ symbols into one:

\[ \forall k,m,n : \N \; ( D(k,m) \wedge D(m,n) \to D(k,n) ) \]

The existential quantifier is used to express assertions of the form “some x has the property $P$” or “for some x, $P(x)$” where $P$ is a property/predicate and $x$ is a variable ranging over the domain of $P$. Examples are “some number is even,” or, “there exists an odd composite number.”

We use the symbol $\exists$ to denote existence. The symbol $\exists$ followed by a variable $x$ is meant to represent the phrase “for some $x$” or “there exists some $x$ such that …”. With this in mind let us formalize the two examples above:

“Some number is even” becomes logicized (aka formalized) as

\[ \exists n : \N \; (E(n)) = \exists n : \N \; \exists k : \N \; (n=2k) \]

And “there exists an odd composite integer” becomes logicized (aka formalized) as

\[ \exists n : \Z \; \exists k : \Z \; \exists l : \Z \; \exists m : \Z \; (n=2k+1) \land (n=lm) \land \neg ((l=1) \land (m=1)) \]

Challenge

The following statements about the natural numbers assert the existence of some natural number. Write the corresponding formal sentences.

• (Remember that a natural number is composite if it is greater than 1 and not prime.)
• Every natural number greater than one has a prime divisor.
• For every $n : \N$, if $n$ has a prime divisor smaller than $n$ , then $n$ is composite.
• Between any two rational numbers there is a rational number.

Free and bound variables

Consider the expression \[ \displaystyle\sum_{i=1}^{i=n} a^i \] The value of this expression depends on $a$ but not on $i$. If we change $i$ to $j$ the result remains the same while if we change $a$ to $b$ we will have a different result.

Another example from calculus: consider the integral \[ \int_{0}^{\infty} \, x \, e^y \, dx \] whose value depends on $y$ but not on $x$.

After we write $\exists x$ or $\forall x$, all the occurrences of the variable $x$ are bound by the quantifier. For example, the expression $\forall x \; (E(x) \vee O(x))$ expresses that every number is even or odd. Notice that the variable $x$ does not appear anywhere in the informal statement. The statement is not about $x$ at all; rather $x$ is a dummy variable, a placeholder that stands for the “thing” referred to within a phrase that beings with the words “every thing.” or “some thing”. We think of the expression $\forall n : \N \; (E(n) \vee O(n))$ as being the same as the sentence $\forall m: \N \; (O(m) \vee O(m))$. Similarly, but perhaps less obviously, the two sentences \[ \exists n : \N \; \exists k : \N \; (n=2k) \] and \[ \exists k : \N \; \exists n : \N \; (n=2k) \] are the same.

A variable that is not bound is called free. Notice that formulae in first-order predicate logic say things about their free variables. For example, in the domain of natural numbers, and with interpretation of $\le$ as “less than” relationship, the formula $\forall y \; (x \le y)$ says that natural number $x$ is less than or equal to every natural number. The formula $\forall z \; (x \le z)$ says exactly the same thing; we can always rename a bound variable (in this case the variable $y$ is renamed to $z$), as long as we pick a name that does not clash with another name that is already in use (i.e. we should not rename $y$ to $x$ since $x$ is already used in the expression; $\forall y \; (x \le x)$ says something completely different).

So, renaming a bound variable (module a caveat) is OK, but what about renaming a free variable? The formula $\forall y (w \le y)$ says that $w$ is less than or equal to every natural number. This statement says something about $w$, rather than $x$. So renaming a free variable changes the meaning of a formula.

Notice also that some formulas, like $\forall x, y \; (x \le y \vee y \le x)$, have no free variables at all. Such a formula is called a sentence, because it makes an outright assertion, a statement that is either true or false about the intended interpretation.

Challenge

In the sentences below first write down the formula in predicate logic and then identify which variables are bound and which are free:

1. For every integer $n$ there is a prime number $p$ between $n$ and $2n$.
2. If a real number $a$ is positive then it has a root.

Challenge

Suppose $P$ is a binary predicate where $P(x,y)$ asserts that “$x$ is a parent of $y$”, and Suppose $C$ is a binary predicate where $C(x,y)$ asserts that “$x$ and $y$ are a couple”. Determine the bound and free variables in the formulae below and explain, in plain English, what do they mean?

1. $\exists z \; P(x,z) \To \exists y \; C(x,y)$
2. $C(x,y) \land \neg \exists z \; P(x,z) \land P(y,z))$

Again, I hope the examples above could convey the fact that in a formula of the form $\forall x \; A(x)$ or $\exists x \; A(x)$ what the formula says is not about the bound variable at all; In determining what $\exists z \; P(x,z) \To \exists y \; C(x,y)$ says we observed that statement does not refer to $z$ at all.

Parsing and Binding Rules

The rules of binding of propositions applies in the larger setting of predicate logic, but we also have additional rules. Therefore, we modify the binding rules of propositional logic to include quantifiers as well.

1. Negation binds most tightly.
2. Then, the universal quantifier $\forall$ and conjunction ($\land$) bind from right to left.
3. Then, the existential quantifier $\exist$ and disjunctions ($\lor$) bind from right to left.
4. Finally, implications ($\To$) and bi-implications ($\iff$) bind from right to left.

For instance the expression $\exists x\; A(x) \land B(x)$ would parse as $(\exists x \; A(x) ) \land B(x)$. However, in Lean, concerning quantifiers, the state of affairs are a little bit different. Here are some warnings concerning the syntax of quantifiers:

• In symbolic logic, the universal quantifier is usually taken to bind tightly. For example, $\forall x \; P \vee Q$ is interpreted as $(\forall x \; P) \vee Q$, and we would write $\forall x \; (P \vee Q)$ to extend the scope of quantification.

• In computer science, and in particular in Lean, quantifiers are often given the widest scope possible. This is the case with Lean. For example, ∀ x, P ∨ Q is interpreted as ∀ x, (P ∨ Q), and we should write (∀ x \; P) ∨ Q to limit the scope (that is we wanted to say that it is either the case that for every x, P holds or it is the case that Q holds.).

• In Lean, the expression ∀ x y z, x ∣ y → y ∣ z → x ∣ z is interpreted as ∀ x y z, x ∣ y → (y ∣ z → x ∣ z), with parentheses associated to the right (Here, as before, the symbol | is for division predicate, e.g. 2 | 4 but not 3 | 28). The part of the expression after the universal quantifier can therefore be interpreted as saying “given that x divides y and given that y divides z, we infer that x divides z.” As we saw with currying for propositions, the expression is logically equivalent to ∀ x y z, x ∣ y ∧ y ∣ z → x ∣ z, but in Lean, it is often convenient to express facts like this as an iterated implication.

Challenge

1. Parse the following expressions both in symbolic logic: \[ \exists x \; D(x) \To \forall y \; D(y) \]
2. Does Lean parse this the same?
3. Is the above sentence equivalent to the following one? \[ \exists x \; ( D(x) \To \forall y \; D(y) ) \]

The Rules of Inference for $\forall$ and $\exists$

These rules are explained in the Summary Slides and also in the Lean Lab

Counterexample

A counterexample to a statement of the form $\forall x\; A(x)$ is a proof of $\exists x \; \neg A(x)$. Here are some examples:

1. A counter-example to the sentence “every prime integer is odd” is a provided by $2$.
2. A counter-example to the sentence “every integer has a prime factor” is a provided by $1$.

Challenge

What is the counter-example to the sentence “every perfect number is even”.

We can constructively prove that $\exists x \; \neg A(x) \To \neg \forall x\; A(x)$ is a tautology. For the converse, however, we need to use classical reasoning (e.g. double negation). From a constructive standpoint, however, knowing that it is not the case that every $x$ satisfies $A(x)$ is strictly weaker condition than having a particular $x$ that satisfies $\neg A(x)$. If I tell you that not everybody in this class will pass, I gave you less information than if I told you the name of the person who is going to fail.

But classically, somewhat strangely, $\exists x \; \neg A(x)$ and $\neg \forall x\; A(x)$ become the same thing, and therefore, a counterexample is nothing more or less than a proof of $\neg \forall x\; A(x)$.

Constructive vs Classical Existence

For us a proof of $\exists x \; A (x)$ is provided by an element $a$ from the domain of discourse of $A$ with a proof that $a$ satisfies $A$, i.e. the proposition $A(a)$ holds. In other words, if we want to prove an existential statement we must find a witness for it. Classical logic demands less; it says if we want to prove $\exists x \; A (x)$ it is also good enough to show that it is not the case that all elements $a$ of the domain of discourse fail to satisfy $A$. Therefor classical logic gives a scape way to prove $\exists x \; A (x)$ without actually finding $a$.

Why is such round-about reasoning justified in classical logic? It is again because of the Law of Excluded Middle which implies that the sentences $\exists x \; A (x)$ and $\neg \forall x \; \neg A (x)$ are logically equivalent. Hence proving $\exists x \; A (x)$ is the same as proving doubly-negated $\neg \forall x \; \neg A (x)$.

The tension between constructive and classical extension is vividly clear in the following super-famous proof of the following theorem.

Theorem

There are irrational numbers $x$ and $y$ such that $x^y$ is a rational number.

Classical Proof

By the Law of Excluded Middle either $\sqrt{2}^{\sqrt{2}}$ is either rational or it is not. We now argue by cases: If $\sqrt{2}^{\sqrt{2}}$ is rational then take $x$ to be $\sqrt{2}^{\sqrt{2}}$ and $y$ to be $\sqrt{2}$. $y$ is irrational because we proved in the last lecture that $\sqrt{2}$ is not rational – insert that proof here. We now have \[ x^y = (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{ {\sqrt{2}} \times \sqrt{2} } = \sqrt{2}^2 = 2\] and therefore $x^y$ is rational. However, if $\sqrt{2}^{\sqrt{2}}$ is irrational, then we are done by taking both $x$ and $y$ to be $\sqrt{2}$. $\; \qed$

Does this proof convince you of the truth of the theorem? What is strange to me is that the proof does not find/pinpoint a single pair $(x,y)$ such that $x^y$ is rational. The proof is branching at its start, and afterwards we do not know in which branch we are. It’s like using a toolkit which has only hammer and a screwdriver in it and we manage to use a tool in this toolkit to put a nail into a wall but we don’t know which tool we used to put that nail into that wall. All we can say is it was either a hammer or a screwdriver which did the job.

That was a classical proof of the theorem above; interestingly we can also give a constructive proof.

Constructive Proof

Take $x$ to be $10$ and $y$ to be $log …$

Maximally Negated Formulae

In maximally negated propositional formulae we saw that how one can push all the negations of a forumla down to the propositional atoms, using classical principles of reasoning. For instance, while $ \neg (P \To Q) $ is not maximally negated, the classically equivalent propositions $P \land \neg Q$ is maximally negated.

In predicate logic we can do the same but with a bit more complexity added by the quantifiers. The classical equivalences which aid us to achieve are:²

\[\forall x \; \neg A(x) \iff \neg \exists x\; A(x) \]

Quantifier Elimination

A collection of deep results in logic are about quantifier elimination. Formulas with less depth of quantifier alternation are thought of as being simpler, with the quantifier-free formulae (i.e. propositional formulae) as the simplest.

Consider how we formalize the notion of continuity of functions from the real line $\RR$ to $\RR$:

\[ \forall a \in \RR \; \forall \varepsilon > 0 \; \exists \delta > 0 \; \forall x \in \RR \; (|x - a| < \delta \To |f(x) - f(a)| < \varepsilon) \]

Quantifier alternation has the pattern \[ \forall \exists \forall \ \]

We can even introduce the predicate of continuity on function from $\RR$ to $\RR$. In Lean that would be

is_continuous_at (f : ℝ → ℝ) (x₀ : ℝ) :=
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - f x₀| ≤ ε

An example from high school mathematics says that a single-variable quadratic polynomial has a real root if and only if its discriminant is non-negative

\[ \exists x\in \mathbb{R} \; (a\neq 0\wedge ax^{2}+bx+c=0)\ \ \Longleftrightarrow \ \ a\neq 0\wedge b^{2}-4ac\geq 0 \]

Note that the left forumla has an existential quantifier while the right side one does not.

The great logician Alfred Tarski showed that for every formula including quantifiers there is always an equivalent quantifier free formula. Obtaining the latter from the former is called quantifier elimination. More precisely he proved that for every first­ order formula over the real field there exists an equivalent quantifier­ free formula. Furthermore, there is an explicit algorithm to compute this quantifier­ free formula.

Footnotes