Quantifier Use
Yannis Kassios February 20, 2009
To illustrate how we use quantifiers in formalization problems, here is the solution to Exercise 89(a) of the textbook. We are asked to formalize:
natural n is the largest proper (neither 1 nor m) factor of natural m
This is a sentence that talks about natural numbers n and m. Therefore, these are the only nonlocal (not introduced by functions or quantifiers) variables that we are allowed to use in the formal expression.
Formalization usually needs a lot of rephrasing steps. The purpose of rephrasing is to bring the informal sentence closer to the formal notation. We do that by making the informal sentence more precise.
In our problem, the first step is to rephrase the sentence so that the logical connectives in it become apparent:
n is not m and n is not 1 and n is a factor of m and n is greater than or equal to any natural
number that has these properties Formalization of most of this sentence is immediate:
n⧧m ∧ n⧧1 ∧ (n is a factor of m) ∧ n ≥ (any natural number that has these properties) We can further simplify as follows:
¬ n: 1,m ∧ (n is a factor of m) ∧ n ≥ (any natural number that has these properties)
We are closer to the formal language. How do we formalize “these properties”? We have to be more specific. The last conjunct can be rephrased as
for any natural number x, if x is neither 1 nor m and x is a factor of m,
then x is less than or equal to n
So the last conjunct is formalized as follows:
∀x: nat· ¬ x: 1,m ∧ (x is a factor of m) ⇒ x≤n
We know that a factor of m cannot be greater than m itself and it cannot be 0. So, the conjunct (x is a factor of m) allows us to restrict the domain of our formalization:
∀x: 1,..m+1· ¬ x: 1,m ∧ (x is a factor of m) ⇒ x≤n
Also, the conjunct ¬ x: 1,m excludes values 1 and m from the domain:
∀x: 2,..m· (x is a factor of m) ⇒ x≤n
Finally, we must formalize the part “is a factor of”. We find this part in two different places in our formalization. Furthermore, in these two places, we talk about different numbers n and x. Finally, the formalization of “is a factor of” is by itself non-trivial. For all these reasons, we will define “is a factor of” as a separate predicate of two variables:
factor = ⟨x, y: nat → x is a factor of y⟩
The formalization of the original sentence is complete if we use that predicate:
¬ n: 1,m ∧ factor n m ∧ ∀x: 2,..m· factor x m ⇒ x≤n The factor predicate is formalized as follows:
x is a factor of y means: there is a natural number z such that y = x×z Formally:
factor = ⟨x, y: nat → ∃z: nat· y=x×z⟩
An alternative to defining factor is to rephrase “x is a factor of y” as “y is a multiple of x”, which can be expressed formally as y: x×nat . So the answer can be stated as
¬ n: 1,m ∧ m: n×nat ∧ ∀x: 2,..m· m: x×nat ⇒ x≤n
1