Blocks of quantified variables

You may have as many quantified variables as you like, for example: 
∀x[∀y[P(x,y) => Q(x)]
When the quantifiers appear one-after-the-other, and when both are of the same type, they are commutative. In other words, ∀x[∀y[...]] is equivalent to ∀y[∀x[...]] and, simliarly, ∃x[∃y[...]] is equivalent to ∃y[∃x[...]]. However, (important!) when the quantifiers are different, they do not commute! So when we have multiple variables introduced with the same quantifier, we tend to use a single quantifier, and follow it with a list of variables, like this: 
∀x,y[P(x,y) => Q(x)]   ← short for ∀x[∀y[P(x,y) => Q(x)]]
... which, due to commutativity, is equivalent to: 
∀y,x[P(x,y) => Q(x)]   ← short for ∀y[∀x[P(x,y) => Q(x)]]

Let's look at a simple example of how quantifiers don't commute when the quantifier types are mixed. 

Domain of Discourse: People
Predicates: loves(·,·) - note: loves(a,b) means "a loves b" ... sadly, that doesn't always mean "b loves a" too

Consider two formulas ...    version1: ∀x[∃y[loves(y,x)]]       version2: ∃y[∀x[loves(y,x)]]
These two formulas differ only by changing the order of the two quantifiers. Question: can you give a concise English-language description of what these formulas mean? BTW: just reading them out like "for all x there exists a y such that ..." does not count. That's not normal English! 
version1: ∀x[∃y[loves(y,x)]] means "everybody is loved by somebody" - but who loves you may be different than who loves me
version2: ∃y[∀x[loves(y,x)]] means "somebody loves everybody" - there is one person out there who loves everyone
So we see that the formulas mean very different things when you switch quantifiers!

A review of basic first-order proofs with "spcialization" (did not do in class)

So let's extend the speaker-session world from the previous class. Let's say that some speakers form adviser/advisee combinations and, when they do, the advisee can never speak in session 2, and if the advisee is in session 1 then the adviser must be in session 2. We'll introduce predicate adviserOf(x,y) 
∀p[in1(p) => ¬in2(p)] ← original from last class, you can't speak in both sessions
∀p,q[adviserOf(p,q) => ¬in2(q) ∧ (in1(q) => in2(p))] ← new
Assume the above rules about speakers and advisers. Given that George is the adviser of Chris, and given that Chris is in session 1, prove that George is not in session 1. 
1: ∀p[in1(p) => ¬in2(p)]                                                [Given]
2: ∀p,q[adviserOf(p,q) => ¬in2(q) ∧ (in1(q) => in2(p))]                 [Given]
3: adviserOf(george,chris)                                              [Given]
4: ∀q[adviserOf(george,q) => ¬in2(q) ∧ (in1(q) => in2(george))]         [Specializing p to george in 2]
5: adviserOf(george,chris) => ¬in2(chris) ∧ (in1(chris) => in2(george)) [Specializing q to chris in 4]
6: ¬in2(chris) ∧ (in1(chris) => in2(george))                            [Modus Ponens on 5 and 3]
7: in1(chris) => in2(george)                                            [And-elimination on 6]
8: in1(chris)                                                           [Given]
9: in2(george)                                                          [Modus Ponens on 7 and 8]
10: in1(george) => ¬in2(george)                                         [Specializing p to george in 1]
11: ¬¬in2(george) => ¬in1(george)                                       [Contrapositive on 10]
12: in2(george) => ¬in1(george)                                         [Double-negation]
13: ¬in1(george)                                                        [Modus Ponens 12 and 9]
Okay, so that was a lot of steps! However, it was mostly just regular old propositional style proof steps. Only the "specialization" steps were new.

First order logic: the final piece - functions

So far we have seen that first order logic extends propositional logic by replacing boolean variables with predicate expressions, and allowing for quantifiers. We are allowed one more tool with first order logic: functions!

Functions: Predicates map objects in the domain of discourse to true/false values. A function in first order logic has input(s) from the domain of discourse and produces outputs from the domain of discourse as well.

Suppose we want to reason about family relationships. 
Domain of discourse: people
Predicates         : AreSiblings(.,.), Equal(.,.), IsChildOf(.,.), loves(.,.) 
Functions          : mother(.)

This gives us the vocabulary to express some things:

∀x[IsChildOf(x,mother(x))] ... "everyone is a child of their mother"

∀x,y[AreSiblings(x,y) => Equal(mother(x),mother(y))] ... "siblings have the same mother"

With functions, we have seen all of the parts of propositional formulas. So we will put them all together in one place:

A first-order formula consists of the syntactical pieces described below. Underlying them is the idea of a domain of discourse, which is the collection of what we call objects. The pieces are: Warning: We should also define syntax, i.e. how these pieces are allowed to be combined to produce a formula, but for this class we will not do that. I believe it is best for this class to leave that to our in-class discussions and experiences with examples.

Express yourself!

First order logic gives us a language to express certain things, and that language is powerful enough to capture a lot of what we want to say. 
Example 1:
The square of a number is greater than or equal to zero.
∀x[ GreaterThanOrEqualTo(Times(x,x),zero) ]
 |  \__________________/ \___/      \__/
 |         predicate    function   constant
 variable

Example 2:
Everyone loves their mother
∀p[loves(p,motherOf(p))] ← Is "loves" a predicate or a function?  How about "motherOf"?

Example 3:
Siblings don't fight with one another
∀x,y[areSiblings(x,y) => ¬fightsWith(x,y)]
Of course, just because we express it doesn't mean it's true ...

Truth - interpretations, evaluating a formula under an interpretation, model

In propositional logic, we had the notion of interpretation, which assigned a value (true or false) to each variable. Of course, in propositional logic the only thing we had other than the operators were the variables. For first order logic, we have constants, predicates, functions, and a domain of discourse. An interpretation in first order logic gives each of these things a value. Once you have done that, you may ask whether the formula is true. For example: 
F := ∀x [¬P(f(x),c)]
Interpretation 1
domain of discourse: { 1,2,3 }
P(a,b): a = b,
f(a):  a f(a)
       1  1
       2  3
       3  1
c: 2
Verify that F is true under this interpretation! It is important to note that you will do this via proof by exhaustion: for each possible value of x, check that ¬P(f(x),c) evaluates to true. 
Interpretation 2
domain of discourse: { dog, cat }
P(a,b): a = b
f(a):  a   f(a)
      dog  cat
      cat  dog
c : dog
Verify that F is not true under this interpretation! It is important to note that to do this you only need to find one possible of x for which ¬P(f(x),c) evaluates to false. This is called proof by counter example. In many circumstances the domain of discourse is infinite, which is a big change from what we dealt with in propositional logic. For example, here is one more interpretation for F: 
Interpretation 3	
domain of discourse: the integers
P(a,b): a < b
f(a): a*a
c: 0
Under this interpretation, F is equivalent to "for all integers x, x^2 is not less than 0" ... which of course we know to be true.

In propositional logic, and interpretation under which a formula evauates to true is called a model, and we keep that same terminology for first-order formulas.

An interpretation $I$ under which formula $F$ evalutates to true is called a model for $F$.

So interpretations 1 and 3 are models for $F$, but interpretation 2 is not.

Christopher W Brown