Consider the following declarative sentence
Not all birds can fly.
This sentence can be paraphrased as
It is not the case that all things which are birds can fly.
Let be the set of all things of interest (i.e., the universe under discussion). We now introduce predicates and , defined by
Finally, using (unary) predicates and , the declarative sentence “Not all birds can fly” can be encoded as follows
where we used negation (), universal quantification (), and material implication (). The (well-formed) formula above should be read as: “it is not the case that for all , if is a bird, then can fly”. Whether the (universally quantified) formula evaluates to or depends on the set we consider. For example, if is the set of all living things on Earth on January 1, 2012, then the formula evaluates to because penguins are birds which cannot fly. However, if we spend the next century eradicating all birds that cannot fly, then on January 1, 2112, the formula might evaluate to .
Let us consider the formula , where is a predicate. If this formula evaluates to , then it is not the case that for all we have that , which is the same as saying that there exists a for which or, in other words, for which . Hence, formula is equivalent (in some sense) to the formula , where is the existential quantifier. We write to denote this equivalence. Hence, we conclude that
Given propositional atoms and , we have that the formula is semantically equivalent  to the formula . We write to denote this equivalence. Thus, we have that
which allows us to conclude that
Using one of De Morgan’s laws, namely, , we conclude that . Eliminating the double negation (we can do that in Classical Logic, but not in Intuitionistic Logic), we obtain . Without further ado, we have that
From all these equivalences, we finally conclude that
What does this equivalence say? It tells us that the declarative sentence “Not all birds can fly” can be paraphrased as follows
There exists a thing which is a bird and which cannot fly.
That “thing” could be, for example, a penguin. For the sake of convenience, let us introduce predicates and , defined by
so that the last equivalence can be written more compactly as
where . This will be useful later on.
Creating our universe
Let us suppose that we do not know that penguins are birds and that they cannot fly. Evaluating the formula using planet Earth’s fauna as the set of all things of interest would require us to consult quite a few Zoology books. However, it is Sunday night and the library is closed for the Winter break. And, to make matters worse, we are somewhat lazy.
Instead of bothering with the actual universe, let us create our own imaginary universe in which there are only three classes of animals: birds, cats, and dogs. Each class contains only three species each.
We construct this imaginary universe in Haskell:
-- create Animal data type
data Animal = Bird String |
Cat String |
Dog String deriving (Show, Eq)
-- create list of animals
animals = [Bird "Dove", Bird "Hawk", Bird "Penguin",
Cat "Burmese", Cat "Persian", Cat "Siamese",
Dog "Dalmatian", Dog "Husky", Dog "Terrier"]
-- define isBird predicate
isBird :: Animal -> Bool
isBird (Bird s) = True
isBird _ = False
-- define canFly predicate
canFly :: Animal -> Bool
canFly (Bird "Dove") = True
canFly (Bird "Hawk") = True
canFly _ = False
-- define phi predicate
phi :: Animal -> Bool
phi x = ((not . isBird) x) || (canFly x)
-- define psi predicate
psi :: Animal -> Bool
psi x = (isBird x) && ((not . canFly) x)
Let us now play with these objects and predicates and evaluate the quantified formulas using the GHCi interpreter:
*Main> -- print list of animals
[Bird "Dove",Bird "Hawk",Bird "Penguin",Cat "Burmese",Cat "Persian",
Cat "Siamese",Dog "Dalmatian",Dog "Husky",Dog "Terrier"]
*Main> -- test isBird predicate
*Main> map isBird animals
*Main> -- test canFly predicate
*Main> map canFly animals
*Main> -- test phi predicate
*Main> map phi animals
*Main> -- test psi predicate
*Main> map psi animals
*Main> -- evaluate universally quantified formula
*Main> not (all phi animals)
*Main> -- evaluate existentially quantified formula
*Main> any psi animals
where we used functions all and any to emulate the universal and existential quantifiers, respectively. Note that both formulas evaluate to , as expected.
Caution: do not confuse the arrow used in the definition of the predicates with the arrow used in material implication. They look the same, but they are different symbols and context should allow one to distinguish the two.
Remark: this post is based on an example in chapter 2 of Huth & Ryan .
 Michael Huth, Mark Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, 2nd ed., Cambridge University Press, June 2004.