Example 4.1
Everybody likes John Cusack: ∀x : (likes (x, John Cusack)).
Example 4.2
Somebody likes Joan Cusack: ∃x : (likes (x, Joan Cusack)).
Example 4.3
Somebody likes everybody: ∃x :(∀y : (likes (x, y))). (We use n for "needy"?)
Example 4.4
Everybody likes somebody: ∀y :(∃x : (likes (y, x))). Careful; this formula looks similar to the preceding one, but it has a very different meaning!
Exercise 4.1.1.1
How would you express "Somebody is liked by everybody"?
Exercise 4.1.1.2
How would your express “Everybody is liked by everybody”?
Example 4.5
The following formula is a simple application of symmetry. ∀x :(∀y : (near (x, y) ⇒ near (y,
x))) ∧ near (Sue, Joe) ⇒ near (Joe, Sue).
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 4.6
∀x : (even (x) ∧ prime (x) ⇒ (x = 2)) is a mathematical fact, in the standard interpretation of arithmetic.
While technically not allowed by our term (Definition: "term", p. 91) and formula (Definition: "Well-Formed Formula (WFF) for first-order logic", p. 91) syntax, we'll continue using infix notation for common mathematical functions and relations, as in the previous example (Example 4.6).
Exercise 4.1.1.3
The previous example (Example 4.6) used the relations even and prime. Of course, to use such relations, they must either be defined
directly by the interpretation, or be defined in terms of functions and relations provided by the interpretation.
How would you define these two relations in terms of the basic numerical functions (addition, multiplication, ...) and relations (= , <, >)?
Exercise 4.1.1.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?
Enough about number theory. Let's look at some examples about common data structures and some about our favorite problem, WaterWorld.
Example 4.7
If your program uses binary search trees and your domain is tree nodes, you need to know
.
If these trees are also balanced, you need to know
Again, these assume the implied interpretations.
Example 4.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 a[i]. For this example, we'll use that notation, even though it doesn't quite fit the logic's syntax.
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) size(a).
sorted (a) ≡∀i : ((1 ≤ i) ∧ (i<
size (a)) ⇒ (a [i − 1] <a [i]))
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: sorted (a) ≡∀i : ((0 ≤ i) ∧ (i< size (a) − 1) ⇒ (a [i] <a [i + 1])).
Or we could state that the ordering holds on every pair of elements: sorted (a) ≡∀i : (∀j : ((0 ≤ i) ∧ (i< size (a)) ∧ (0 ≤ j) ∧ (j< size (a)) ∧ (i<j) ⇒ (a [i] ≤ a [j]))). This definition isn't any stronger, but it makes an additional property explicit. Generally, you'd find it harder to prove that this formula was true, but once you did, you'd find it easier to use this formula to prove other statements.
Exercise 4.1.1.5
The two preceding examples used functions like left, size, and subtraction, although our logic syntax doesn't include such functions. However, we can rewrite any use of functions with
appropriate new relations.
As an example, rewrite i< size (a) in proper first-order syntax.
Exercise 4.1.1.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?
Exercise 4.1.1.7
How would you make a similar statement about the number of adjacent pirates being one? These statements are very similar to, and provable from, the first-order WaterWorld The domain axioms.
- 3494 reads
