Navigation
-
Content Actions
-
Recently Viewed
First-Order Logic: using quantifiers
Summary: Introducting quantifiers, to upgrade from propositional logic to first-order logic.
-
Links
-
Supplemental links
First-Order Equivalences
First-Order Waterworld AxiomsTalking about unnamed items
Suppose we want to express a statement like
“there is a location which has two neighbors”
(which is true, at least for the domain of WaterWorld board
locations), or
“all actors have co-starred with
Kevin Bacon”
(which isn't true, at least for the domain of all Hollywood actors).
As it stands, we can only formulate these in an awkward way —
by talking about
specific (constant) locations like
We'll redress this by introducing two quantifiers,
“
“For all” is really just an abbreviation for a large conjunction, while “exists” is a disjunction (it could also be called “for some”, though it's not). How large a conjunction/disjunction? As big as your domain — which actually could be very small, or it could be infinitely large. Even aside from the fact that we can't write down an infinitely large conjunction or disjunction, quantifiers let us form the conjunction without having to select a domain in advance.
To continue with our WaterWorld example,
how can we express the concept "
We use quantifiers all the time in natural language. Consider the following examples, where we provide a natural English wording together with an equivalent phrasing that makes the quantification more explicit. We'll take the translations with a grain of salt, since sometimes people can disagree on the exact details of the intended English meaning. Such ambiguity can sometimes be a rich source of creativity, but it's not tolerable when documenting safety properties of software. While some of these examples are a bit frivolous, in general quantifiers let us precisely capture more interesting concepts in type-checking, data structures such as trees and hash tables, circuit specifications, etc.
| Natural English | Formalized English |
|---|---|
| “If you don't love yourself, you can't love anybody else.” | “If you don't love you, there does not exists a person |
| “N*Sync is the best band ever!” | “For all bands |
| A casually subtle line from Something About Mary: “Every day is better than the next.” | “For all days |
| A buggy line from a song (Everybody Loves My Baby, Jack Palmer & Spencer Willson, 1924): “Everybody loves my baby; My baby don't love [anybody] but me.” | “For all persons |
| “Every neighbor of x is unsafe.” | “For all locations |
| “There is a safe location that is a neighbor of x, if num(x)<3.” | “If num(x)<3, then there exists a location y, such that y is safe, and y is a neighbor of x.” |
| “If you've seen one episode, you've seen 'em all.” | “If there exists one episode |
| “Somebody loves everybody.” | “There exists some person |
| “There is someone for everybody.” | “For all persons |
| “All's well that ends well.” |
“For all events |
Warning: The Ambiguous “Any”
The ambiguous “any”: I was playing a game with some friends, and we came across the rule: “If you have more cards than any other player, then discard a card.” Does this mean “than all other players”, or “than some other player”? Our group's opinion was divided (incl. across many native English speakers).
In our class terms, it's not always clear
whether “any” means for-all,
or for-some (there-exists).
Or maybe more accurately,
in the phrase “for any
aside:
Linguistics students, or those who are so sure the rule clearly intended “than all other players”: Switching “In your proof-writing (and your English writing, and your informal writing), think about replacing “any” with either “every” or with “some”, to make your meaning clear.
First-order logic: WFFs revisited
We originally defined a well-formed formula (WFF) for propositional logic; we'll extend this to WFFs for first-order logic, also known as predicate logic. At the same time, we'll more precisely define the binding of variables.
This logic allows use of both functions and relations. Since these functions' outputs are not Booleans (otherwise, we'd call them relations), but rather data than can be used as a relation's input, we separate the syntax into that of terms and formulas. Terms are all the possible inputs for a relation.
- Definition 1: term
- 1. A variable.
Example
a b - 2. A constant.
Example
WaterWorld location
F - 3. A function applied to one or more terms.
Example
successor 3
- Definition 2: Well-Formed Formula (WFF) for first-order logic
- 1. A constant:
true false - 2. An atomic formula: a relation symbol applied to one or more terms.
Example
nhbr x F - 3. A negation of a WFF,
φ - 4. A conjunction of WFFs,
φ ψ - 5. A disjunction of WFFs,
φ ψ - 6. An implication of WFFs,
φ ψ - 7. A universal quantification of a WFF,
x φ Example
x nhbr x F - 8. An existential quantification of a WFF,
x φ Example
x nhbr x F
While a formula is just a piece of syntax, the meaning of its connectives, including the quantifiers, is part of the definition of a WFF. However, as previously discussed, the meaning of a WFF also depends on the interpretation we give to its relations.
Examples
Example 1
Everybody likes John Cusack:
Example 2
Somebody likes Joan Cusack:
Example 3
Somebody likes everybody:
Example 4
Everybody likes somebody:
Exercise 1
How would you express “Somebody is liked by everybody”?
Solution 1
The cue
“Somebody …”
suggests one person who exists; we'll call them
Exercise 2
How would you express “Everybody is liked by somebody”?
Solution 2
The cue
“Everybody …”
suggests a universal; we'll call them
Example 5
The following formula is a simple application of symmetry.
While it is certainly true under the intended interpretation, it is also true under any interpretation. Such formulas are called valid. Valid first-order formulas are the natural analog of tautological propositional formulas.
Example 6
While technically not allowed by our term and formula syntax, we'll continue using infix notation for common mathematical functions and relations, as in the previous example.
Exercise 3
The
previous example used the relations
How would you define these two relations in terms of the basic
numerical functions (addition, multiplication, …)
and relations (
Solution 3
“Evenness” is a straightforward translation from
“An integer n is even, iff it is twice some other integer k”:
There are many equivalent ways to define primality, just as there
many algorithms for checking primality.
One straightforward solution is
aside:
1 is called a “unit”. If we consider the domain of all integers (not just natural numbers), the idea of primality still makes sense; -17 is also prime; and -1 is also another unit. Similarly, considering the domain of “complex integers”Exercise 4
One hypothesis about natural numbers is known as Goldbach's Conjecture. It states that all even integers greater than two can be expressed as the sum of two primes. It is one of the oldest still-unsolved problems about numbers. How would you write this conjecture as a WFF?
Solution 4
Enough about number theory. Let's look at some examples about common data structures and some about our favorite problem, WaterWorld.
Example 7
If your program uses binary search trees and your domain is
tree nodes, you need to know
Example 8
We would like to be able to state that the output of a sorting routine is, in fact, sorted. Let's assume we're sorting arrays into ascending order.
To talk about the elements of an array in a typical programming
language, we would write something like
To describe sortedness (in non-decreasing order),
we want to state that each element is greater than or equal to
the previous one. However, just like in a program, we need to
ensure our formula doesn't index outside the bounds of the array.
For this example, we'll assume that an array's indices are
zero to (but not including)
When proving things about programs, it's often useful to realize there are alternate ways of defining things. So, let's see a couple more definitions.
We could change our indexing slightly:
Or we could state that the ordering holds on every pair of elements:
Exercise 5
The two preceding examples used functions like
As an example, rewrite
Solution 5
We need a new relation that combines the syntax of
Exercise 6
One simple WaterWorld fact is that if a location has no unsafe neighbors, then its number of adjacent pirates is zero. Furthermore, the implication goes both ways. How would you state that as a WFF?
Solution 6
Exercise 7
How would you make a similar statement about the number of adjacent pirates being one?
Solution 7
There are various solutions, but they all must capture the same idea: there exists exactly one unsafe neighbor. This solution states that in two parts:
-
There exists an unsafe neighbor,
u -
Every unsafe neighbor is
u
These statements are very similar to, and provable from, the first-order WaterWorld domain axioms.
A hint on deciphering formulas' meanings
Some formulas can get pretty hairy:
The top-down way would be to read this formula left-to-right.
Is the whole formula true?
Well, it's only true if, for every possible value of x,
some smaller formula is true
(namely,
“there exists a
Most people prefer approaching the problems in a bottom-up manner (or if you prefer, right-to-left or inside-out): First consider at the small inner bits alone, figure out what they mean, and only then figure out how they relate.
-
What does the innermost formula
“
likes x y likes y z x y y z x y z -
Working outward, what does
“
z likes x y likes y z x y y -
Keep on going:
“
y z likes x y likes y z x -
Now it's clear:
“
x y z likes x y likes y z
“Forall”'s friend “if”
We have already seen quite a few formulas of the general form