Using only PropositionalLogic, we can express a simple version of a famous argument:
- Socrates is a man.
- If Socrates is a man, then Socrates is mortal.
- Therefore, Socrates is mortal.
This is an application of the inference rule (see InferenceRules) called modus ponens, which says that from p and p ⇒ q you can deduce q. The first two statements are axioms (meaning we are given them as true without proof), and the last is the conclusion of the argument.
What if we encounter Socrates's infinitely more logical cousin Spocrates? We'd like to argue
- Spocrates is a man.
- If Spocrates is a man, then Spocrates is mortal.
- Therefore, Spocrates is mortal.
Unfortunately, the second step depends on knowing that humanity implies mortality for everybody, not just Socrates. If we are unlucky in our choice of axioms, we may not know this. What we would like is a general way to say that humanity implies mortality for everybody, but with just PropositionalLogic, we can't write this fact down.
1. Variables and predicates
The solution is to extend our language to allow formulas that involve variables. So we might let x, y, z, etc. stand for any element of our universe of discourse or domain—essentially whatever things we happen to be talking about at the moment. We can now write statements like:
- "x is human."
- "x is the parent of y."
"x + 2 = x2."
These are not propositions because they have variables in them. Instead, they are predicates; statements whose truth-value depends on what concrete object takes the place of the variable. Predicates are often abbreviated by single capital letters followed by a list of arguments, the variables that appear in the predicate, e.g.:
- H(x) = "x is human."
- P(x,y) = "x is the parent of y."
Q(x) = "x + 2 = x2."
We can also fill in specific values for the variables, e.g. H(Spocrates) = "Spocrates is human." If we fill in specific values for all the variables, we have a proposition again, and can talk about that proposition being true (e.g. H(2) and H(-1) are true) or false (H(0) is false).
2. Quantifiers
What we really want though is to be able to say when H or P or Q is true for many different values of their arguments. This means we have to be able to talk about the truth or falsehood of statements that include variables. To do this, we bind the variables using quantifiers, which state whether the claim we are making applies to all values of the variable (universal quantification), or whether it may only apply to some (existential quantification).
2.1. Universal quantifier
The universal quantifier ∀ (pronounced "for all") says that a statement must be true for all values of a variable within some universe of allowed values (which is often implicit). For example, "all humans are mortal" could be written ∀x: Human(x) ⇒ Mortal(x) and "if x is positive then x+1 is positive" could be written ∀x: x > 0 ⇒ x+1 > 0.
If you want to make the universe explicit, use set membership notation, e.g. ∀x∈Z: x > 0 ⇒ x+1 > 0. This is logically equivalent to writing ∀x: x∈Z ⇒ (x > 0 ⇒ x+1 > 0) or to writing ∀x: (x∈Z ∧ x > 0) ⇒ x+1 > 0, but the short form makes it more clear that the intent of x∈Z is to restrict the range of x.1
The statement ∀x: P(x) is equivalent to a very large AND; for example, ∀x∈N: P(x) could be rewritten (if you had an infinite amount of paper) as P(0) ∧ P(1) ∧ P(2) ∧ P(3) ∧ ... . Normal first-order logic doesn't allow infinite expressions like this, but it may help in visualizing what ∀x: P(x) actually means. Another way of thinking about it is to imagine that x is supplied by some adversary and you are responsible for showing that P(x) is true; in this sense, the universal quantifier chooses the worst case value of x.
2.2. Existential quantifier
The existential quantifier ∃ (pronounced "there exists") says that a statement must be true for at least one value of the variable. So "some human is mortal" becomes ∃x: Human(x) ∧ Mortal(x). Note that we use AND rather than implication here; the statement ∃x: Human(x) ⇒ Mortal(x) makes the much weaker claim that "there is some thing x, such that if x is human, then x is mortal", which is true in any universe that contains an immortal purple penguin—since it isn't human, Human(penguin) ⇒ Mortal(penguin) is true.
As with ∀, ∃ can be limited to an explicit universe with set membership notation, e.g. ∃x∈Z: x = x2. This is equivalent to writing ∃x: x∈Z ∧ x = x2.
The formula ∃ x: P(x) is equivalent to a very large OR, so that ∃x∈N: P(x) could be rewritten as P(0) ∨ P(1) ∨ P(2) ∨ P(3) ∨ ... . Again, you can't generally write an expression like this if there are infinitely many terms, but it gets the idea across.
2.3. Negation and quantifiers
- ¬∀ x: P(x) ≡ ∃ x: ¬P(x).
- ¬∃ x: P(x) ≡ ∀ x: ¬P(x).
These are essentially the quantifier version of De Morgan's laws: the first says that if you want to show that not all humans are mortal, it's equivalent to finding some human that is not mortal. The second says that to show that no human is mortal, you have to show that all humans are not mortal.
2.4. Restricting the scope of a quantifier
Sometimes we want to limit the universe over which we quantify to some restricted set, e.g. all positive integers or all baseball teams. We can do this explicitly using implication, e.g.
∀x: x > 0 ⇒ x-1 ≥ 0
or we can abbreviate by including the restriction in the quantifier expression itself
∀ x>0: x-1 ≥ 0.
Similarly
∃x: x > 0 ∧ x2 = 81
can be written as
∃x>0: x2 = 81.
Note that constraints on ∃ get expressed using AND rather than implication.
The use of set membership notation to restrict a quantifier is a special case of this. Suppose we want to say that 79 is not a perfect square, by which we mean that there is no integer whose square is 79. If we are otherwise talking about real numbers (two of which happen to be square roots of 79), we can exclude the numbers we don't want by writing
¬∃x∈ℤ x2 = 79
which is interpreted as
¬∃x (x∈ℤ ∧ x2 = 79)
or, equivalently
∀x x∈ℤ ⇒ x2 ≠ 79.
(Here ℤ = { ..., -2, -1, 0, 1, 2, ... } is the standard set of integers. See SetTheory for more about ∈.)
2.5. Nested quantifiers
It is possible to nest quantifiers, meaning that the statement bound by a quantifier itself contains quantifiers. For example, the statement "there is no largest prime number" could be written as
¬∃ x: (Prime(x) ∧ ∀ y: y > x ⇒ ¬Prime(y))
i.e., "there does not exist an x that is prime and any y greater than x is not prime." Or in a shorter (though not strictly equivalent) form:
∀ x ∃ y: y > x ∧ Prime(y)
"for any x there is a bigger y that is prime."
To read a statement like this, treat it as a game between the ∀ player and the ∃ player. Because the ∀ comes first in this statement, the for-all player gets to pick any x it likes. The ∃ player then picks a y to make the rest of the statement true. The statement as a whole is true if the ∃ player always wins the game. So if you are trying to make a statement true, you should think of the universal quantifier as the enemy (the adversary in algorithm analysis) who says "nya-nya: try to make this work, bucko!", while the existential quantifier is the friend who supplies the one working response.
Naturally, such games can go on for more than two steps, or allow the same player more than one move in a row. For example
∀ x ∀ y ∃ z x2 + y2 = z2
is a kind of two-person challenge version of the Pythagorean_theorem where the universal player gets to pick x and y and the existential player has to respond with a winning z. (Whether the statement itself is true or false depends on the range of the quantifiers; it's false, for example, if x, y, and z are all NaturalNumbers or rationals but true if they are all real or complex. Note that the universal player only needs to find one bad (x,y) pair to make it false.)
One thing to note about nested quantifiers is that we can switch the order of two universal quantifiers or two existential quantifiers, but we can swap a universal quantifier for an existential quantifier or vice versa. So for example ∀x∀y (x = y ⇒ x+1 = y+1) is logically equivalent to ∀y∀x (x = y ⇒ y+1 = x+1), but ∀x∃y y < x is not logically equivalent to ∃y∀x y < x. This is obvious if you think about it in terms of playing games: if I get to choose two things in a row, it doesn't really matter which order I choose them in, but if I choose something and then you respond it might make a big difference if we make you go first instead.
One measure of the complexity of a mathematical statement is how many layers of quantifiers it has, where a layer is a sequence of all-universal or all-existential quantifiers. Here's a standard mathematical definition that involves three layers of quantifiers, which is about the limit for most humans:

Now that we know how to read nested quantifiers, it's easy to see what the right-hand side means:
- The adversary picks ε, which must be greater than 0.
- We pick N.
- The adversary picks x, which must be greater than N.
- We win if f(x) is within ε of y.
So, for example, a proof of
![\[
\lim_{x \rightarrow \infty} 1/x = 0
\] \[
\lim_{x \rightarrow \infty} 1/x = 0
\]](/pinewiki/PredicateLogic?action=AttachFile&do=get&target=latex_0c0dcca6d1a86f1c66be3a6c13399f6262b7e69e_p1.png)
would follow exactly this game plan:
Choose some ε > 0.
Let N > 1/ε. (Note that we can make our choice depend on previous choices.)
Choose any x > N.
Then x > N > 1/ε > 0, so 1/x < 1/N < ε ⇒ |1/x - 0| < ε. QED!
2.6. Examples
Here are some more examples of translating English into statements in predicate logic:
English |
Logic |
Other variations |
All crows are black. |
∀x Crow(x) ⇒ Black(x) |
Equivalent to ¬∃x Crow(x) ∧ ¬Black(x) or ∀x ¬Black(x) ⇒ ¬Crow(x). The latter is the core of a classic "paradox of induction" in philosophy: if seeing a black crow makes me think it's more likely that all crows are black, shouldn't seeing a logically equivalent non-black non-crow (e.g. a banana yellow AMC_Gremlin) also make me think all non-black objects are non-crows, i.e., that all crows are black? (I think this mostly illustrates that logical equivalence only works for true/false and not for probabilities.) |
Some cows are brown. |
∃x Cow(x) ∧ Brown(x) |
|
No cows are blue. |
¬∃x Cow(x) ∧ Blue(x) |
≡ ∀x ¬(Cow(x) ∧ Blue(x) ≡ ∀x (¬Cow(x) ∨ ¬Blue(x)) ≡ ∀x Cow(x) ⇒ ¬Blue(x) ≡ ∀x Blue(x) ⇒ ¬Cow(x). (But see Paul_Bunyan.) |
All that glitters is not gold. |
¬∀x Glitters(x) ⇒ Gold(x) |
≡ ∃x Glitters(x) ∧ ¬Gold(x). Note that the English syntax is a bit ambiguous: a literal translation might look like ∀x Glitters(x) ⇒ ¬Gold(x), which is not logically equivalent. This is why predicate logic is often safer than natural language. |
No shirt, no service. |
∀x ¬Shirt(x) ⇒ ¬Served(x) |
|
Every event has a cause. |
∀x∃y Causes(y,x) |
|
Every even number greater than 2 can be expressed as the sum of two primes. |
∀x (Even(x) ∧ x > 2) ⇒ (∃p ∃q Prime(p) ∧ Prime(q) ∧ x = p+q) |
Note: the truth value of this statement is currently unknown. See Goldbach's conjecture. |
3. Inference rules for quantifiers
See InferenceRules.
4. Functions and equality
A function symbol looks like a predicate but instead of computing a truth value it returns a new object. So for example the successor function S in the PeanoAxioms for the natural numbers returns x+1 when applied as S(x). Sometimes when there is only a single argument we omit the parentheses, e.g. Sx = S(x), SSSx = S(S(S(x))).
Often we include a special equality predicate =, written x=y. The interpretation of x=y is that x and y are the same element of the domain. It satisfies the reflexivity axiom ∀x x=x and the substitution axiom schema
- ∀x∀y (x=y ⇒ (Px ⇔ Py))
where P is any predicate; this immediately gives a substitution rule that says x = y, P(x) ⊢ P(y). It's likely that almost every proof you ever wrote down in high school algebra consisted only of many applications of the substitution rule.
- Example
- We'll prove ∀x∀y (x=y ⇒ y=x) from the above axioms. Apply substitution to the predicate Px ≡ y=x to get ∀x∀y (x=y ⇒ (y=x ⇔ x=x)). Use reflexivity to rewrite this as ∀x∀y (x=y ⇒ (y=x ⇔ T)) or ∀x∀y (x=y ⇒ y=x) as claimed.
- Exercise
- Prove ∀x∀y∀z (x=y ∧ y=z ⇒ x=z).
5. Uniqueness
An occasionally useful abbreviation is ∃!x P(x), which stands for "there exists a unique x such that P(x)." This is short for
- (∃x P(x)) ∧ (∀x∀y P(x) ∧ P(y) ⇒ x = y).
An example is ∃!x x+1 = 12. To prove this we'd have to show not only that there is some x for which x+1 = 12 (11 comes to mind), but that if we have any two values x and y such that x+1 = 12 and y+1 = 12, then x=y (this is not hard to do). So the exclamation point encodes quite a bit of extra work, which is why we usually hope that ∃x x+1 = 12 is good enough.
Programmers will recognize this as a form of SyntacticSugar. (1)
PineWiki