4. The Predicate-Logic Quantifiers¶

4.1.1. More Examples¶

We state some standard exercises with ∀, where the domains and predicates are unimportant:

∀x f(x) |- ∀y f(y)
{
  1. ∀x f(x)    premise
  2. {
       3. a
       4. f(a)  ∀e 1 a
  }
  5. ∀y f(y)    ∀i 2
}

∀z (f(z) ∧ g(z)) |- (∀x f(x)) ∧ (∀y g(y))
{
  1. ∀z (f(z) ∧ g(z))        premise
  2. {
       3. a
       4. f(a) ∧ g(a)        ∀e 1 a
       5. f(a)               ∧e1 4
  }
  6. ∀x f(x)                 ∀i 2
  7. {
       8. b
       9. f(b) ∧ g(b)        ∀e 1 b
       10. g(b)              ∧e2 9
  }
  11. ∀y g(y)                ∀i 7

  12. (∀x f(x)) ∧ (∀y g(y))  ∧i 6 11
}

The earlier example about healthy and happy families illustrates an important structural relationship between ∀ and →:

∀x (f(x) →  g(x)) |- (∀x f(x)) →  (∀x g(x))

can be proved, but the converse cannot.

This last one is reasonable but the proof is a bit tricky because of the nested subproofs:

∀x∀y f(x,y)  |-  ∀y∀x f(x,y)
{
  1. ∀x∀y f(x,y)         premise
  2. {
       3. b
       4. {
            5. a
            6. ∀y f(a,y)  ∀e 1 a
            7. f(a,b)     ∀e 6 b
        }
        8. ∀x f(x,b)      ∀i 4
  }
  9. ∀y∀x f(x,y)          ∀i 2
}

4.1.2. Tactics for the ∀-rules¶

As in the previous chapter, we now give advice as to when to use the ∀i and ∀e rules.

• (***) ∀i-tactic: To prove Premises |- ∀x P(x),

  1. assume a, for a new, anonymous “Mx a”

  2. prove Premises |- P(a)

  3. finish with ∀i.

  The proof structure looks like this:

  1.  Premises         premise
  i. {
       j.  a
            (fill in)
       k.  P(a)
  }
  l. ∀x P(x)           ∀i i
  
  This tactic was applied in Lines 2-9 of the previous (correct) example
  proof.
  

• (*) ∀e-tactic: To prove Premises, ∀x P(x) |- Q, then for an individual, i, that appears in the proof so far, use the ∀e rule to deduce the new fact, P(i):

  1.  Premises        premise
  2.  ∀x P(x)         premise
      . . .
  j.  P(i)            ∀e 2
         (fill in)
  k.  Q
  

  This tactic should be used only when it is clear that the new fact makes a significant step forwards to finishing the proof. Steps 4 and 5 of the previous (correct) example proof used this tactic.

4.1.3. Other Ways of Proving Propositions with The Universal Quantifier¶

How do we prove an assertion of the form, ∀x P(x)? We just saw that ∀i can do this for any domain whatsoever. But there are, in fact, three different approaches, depending on the form of domain we use:

• Approach 1: use conjunctions for a finite domain

  Say that the domain we study is a finite set, D = {e0, e1, ..., ek}. (An example domain is the days of the week, {sun, mon, tues, weds, thurs, fri, sat}.)

  This makes ∀x P(x) just an abbreviation itself of this much-longer assertion:

  P(e0) ∧ P(e1) ∧ ... ∧ P(ek)
  

  For example, when the domain is the days of the week, the assertion, ∀d isBurgerKingDay(d), abbreviates:

  isBurgerKingDay(sun) ∧ isBurgerKingDay(mon) ∧ ... ∧ isBurgerKingDay(sat)
  

  To prove such a ∀x P(x) for a finite domain D, we must prove P(ei), for each and every ei in D.

  We can use this approach when we are analyzing all the elements of a finite-length list. Say that list r has length 4. We can say that the domain of its indexes is {0, 1, 2, 3}. So, if we wish to prove that ∀ 0 <= i < 4, r(i) > 0, we need only prove that r(0) > 0 ∧ r(1) > 0 ∧ r(2) > 0 ∧ r(3) > 0.

• Approach 2: for the domain of nonnegative ints, use mathematical induction

  The domain, Nat = {0, 1, 2, ... } is infinite, so we cannot use the previous technique to prove properties like ∀ n > 0, (n + 1) > n – we would have to write separate proofs that 0 + 1 > 0, 1 + 1 > 1, 2 + 1 > 2, ..., forever. But we can use mathematical induction.

• Approach 3: for any domain, finite or infinite whatsoever, use the ∀i-law

  Finally, we might be using a large domain that is not as organized as the nonnegatives, 0,1,2,.... Maybe the domain is the domain of all humans or all the citizens of Peru or the members of the Republican party or all the objects on Planet Earth. How can we prove ∀ x P(x) for such huge collections?

  To prove a claim of form, ∀x P(x), for an arbitrary domain, we undertake a kind of case analysis: we prove property P(a) for an arbitrary member, a, of domain D. (Call the element, “Mx a” — Mx arbitrary — Mx anybody — Mx anonymous). Since Mx a is a complete unknown, it stands for “everyone” in doman D. We know that we can substitute whichever domain element, d from domain D, we want into the proof and we get a proof of P(d). In this way, we have proofs of P for all elements of domain D.

  This is the idea behind the ∀i-rule.

4.2.1. The Existential-Introduction Rule¶

Often ∃ is used to “hide” secret information. Consider these Pat Sajack musings from a typical game of Wheel of Fortune:

• Pat thinks: “There is an ‘E’ covered over on Square 14 of the game board”. In predicate logic, this can be written:

  isCovered(Square14) ∧ holds(Square14,'E').
  

• Pat thinks: “Wait – I can’t say that on TV! Perhaps I can say, There is a vowel covered on Square 14 of the game board”. In predicate logic, this is written:

  isCovered(Square14) ∧ (∃c isVowel(c) ∧ holds(Square14,c)).
  

  In this way, Pat does not reveal the letter to the game players and TV viewers.

• Because it isn’t fair to tell the players which squares hold vowels, Pat announces on the air, “There is a vowel that is still covered on the game board”:

  ∃s (isSquare(s) ∧ isCovered(s) ∧ (∃c isVowel(c) ∧ holds(s,c)))
  

  This statement hides the specific square and letter that Pat is thinking about.

Pat’s announcement was deduced from its predecessors by means of the ∃i-rule, which we see in a moment.

What can a game player do with Pat’s uttered statement? A player might deduce these useful facts:

• There is a square still covered: ∃s isSquare(s) ∧ isCovered(s)

• There is a vowel: ∃c isVowel(c)

• There is a covered letter, A, E, I, O, U (assuming the vowels are exactly A, E, I, O, U):

  ∃s isSquare(s) ∧ isCovered(s) ∧
    (holds(s,'A') ∨ holds(s,'E') ∨ holds(s,'I') ∨ holds(s,'O') ∨ holds(s,'U'))
  

Although the game player does not know the letter and square that Pat Sajak “hid” with his statement, the player can still make useful deductions. We will use the ∃e rule to deduce these style of propositions.

       P(d)         where  d  is an individual in the domain D
∃i: -----------
      ∃x P(x)

isHuman(Socrates), isMortal(Socrates) |- ∃h (isHuman(h) ∧ isMortal(h))
{
  1. isHuman(Socrates)                        premise
  2. isMortal(Socrates)                       premise
  3. isHuman(Socrates) ∧ isMortal(Socrates)   ∧i 1 2
  4. ∃h (isHuman(h) ∧ isMortal(h))            ∃i 3 Socrates
}

isVowel(e), holds(Square14,e) |- ∃c(isVowel(c) ∧ ∃s holds(s,c))
{
  1. isVowel(e)                       premise
  2. holds(Square14,e)                premise
  3. ∃s holds(s,e)                    ∃i 2 Square14
  4. isVowel(e) ∧ ∃s holds(s,e)       ∧i 1 3
  5. ∃c(isVowel(c) ∧ ∃s holds(s,c))   ∃i 4 e
}

isVowel(e), holds(Square14,e) |- ∃c∃s(isVowel(c) ∧ holds(s,c))
{
  1. isVowel(e)                       premise
  2. holds(Square14,e)                premise
  3. isVowel(e) ∧ holds(Square14,e)   ∧i 1 2
  4. ∃s(isVowel(e) ∧ holds(s,e))      ∃i 3 Square14
  5. ∃c∃s(isVowel(c) ∧ holds(s,c))    ∃i 4 e
}

All humans are mortal
Someone is human
Therefore, someone is mortal

                  {a  P(a)   assume       // where  a  is a new, fresh name
      ∃x P(x)      ...  Q           }     // a  MUST NOT appear in  Q
∃e: -----------------------------------
                     Q

All humans are mortal
Someone is human
Therefore, someone is mortal

∀h(isHuman(h) →  isMortal(h)), ∃x isHuman(x) |- ∃y isMortal(y)
{
  1. ∀h(isHuman(h) →  isMortal(h))   premise
  2. ∃x isHuman(x)                   premise
  3. {
       4. a   isHuman(a)             assume
       5. isHuman(a) →  isMortal(a)  ∀e 1 a
       6. isMortal(a)                → e 5 4
       7. ∃y isMortal(y)             ∃i 6 a
  }
  8. ∃y isMortal(y)                  ∃e 2 3
}

∃c (isVowel(c) ∧ ∃s holds(s,c)) |-  ∃d isVowel(d)
{
  1. ∃c (isVowel(c) ∧ ∃s holds(s,c))     premise
  2. {
     3. a   isVowel(a) ∧ ∃s holds(s,a)   assume
     4. isVowel(a)                       ∧e1 3
     5. ∃d isVowel(d)                    ∃i 4 a
  }
  6. ∃d isVowel(d)                       ∃e 1 2
}

∃x p(x) |- ∃y p(y)
{
  1. ∃x p(x)          premise
  2. {
       3. a    p(a)   assume
       4. ∃y p(y)     ∃i 3 a
  }
  5. ∃y p(y)          ∃e 1 2
}

∃x(f(x) ∧ g(x)) |- (∃y f(y)) ∧ (∃z g(z))
{
  1. ∃x(f(x) ∧ g(x))             premise
  2. {
       3. a    f(a) ∧ g(a)        assume
       4. f(a)                    ∧e1 3
       5. ∃y f(y)                 ∃i 4 a
       6. g(a)                    ∧e2 3
       7. ∃z g(z)                 ∃i 6 a
       8. (∃y f(y)) ∧ (∃z g(z))   ∧i 5 7
  }
  9.  (∃y f(y)) ∧ (∃z g(z))       ∃e 1 2
}

(∃y f(y)) ∧ (∃z g(z)) |- ∃x(f(x) ∧ g(x)).

∃x (p(x) V q(x))  |-  (∃x p(x)) V (∃x q(x))
{
  1. ∃x (p(x) V q(x))                   premise
  2. {
       3. a   p(a) V q(a)               assume
       4. {
            5. p(a)                     assume
            6. ∃x p(x)                  ∃i 5 a
            7. (∃x p(x)) V (∃x q(x))    Vi1 6
       }
       8. {
            9. q(a)                     assume
            10. ∃x q(x)                 ∃i 9 a
            11. (∃x p(x)) V (∃x q(x))   Vi2 10
       }
       12.    (∃x p(x)) V (∃x q(x))     Ve 3 4 8
  }
  13. (∃x p(x)) V (∃x q(x))             ∃e 1 2
}

(∃x p(x)) V (∃x q(x)) |- ∃x (p(x) V q(x)).

∃x ∀y isBossOf(x,y)        // isBossOf(boss, subordinate)

∃x∀y isBossOf(x,y) |- ∀u∃v isBossOf(v,u)
{
  1. ∃x∀y isBossOf(x,y)           premise
  2. {
       3. b   ∀y isBossOf(b,y)    assume
       4. {
            5. a
            6. isBossOf(b,a)      ∀e 3 a
            7. ∃v isBossOf(v,a)   ∃i 6 b
       }
       8. ∀u∃v isBossOf(v,u)      ∀i 4
  }
  9. ∀u∃v isBossOf(v,u)           ∃e 1 2
}

∃x∀y isBossOf(x,y) |- ∀u∃v isBossOf(v,u)
{
  1. ∃x∀y isBossOf(x,y)                 premise
  2. {
       3. a
       4. {
            5. b     ∀y isBossOf(b,y)   assume
            6. isBossOf(b,a)            ∀e 5 a
            7. ∃v isBossOf(v,a)         ∃i 6 b
       }
       8. ∃v isBossOf(v,a)              ∃e 1 4
  }
  9. ∀u∃v isBossOf(v,u)                 ∀i 2
}

∀u∃v isBossOf(v,u) |- ∃x∀y isBossOf(x,y) ???

∀u∃v isBossOf(v,u) |- ∃x∀y isBossOf(x,y)
{
  1. ∀u∃v isBossOf(v,u)             premise
  2. {
       3. a
       4. ∃v isBossOf(v,a)          ∀e 1 a
       5. {
            6. b    isBossOf(b,a)   assume
       }
  6. ∀y isBoss(b,y)                 ∀i 2  NO--THIS PROOF IS TRYING TO FINISH
                                          THE OUTER SUBPROOF WITHOUT FINISHING
                                          THE INNER ONE FIRST.

∃x∀y isBossOf(x,y) |- ∃z isBossOf(z,z)

∃x∀y isBossOf(x,y) |- ∃z isBossOf(z,z)
{
  1. ∃x∀y isBossOf(x,y)           premise
  2. {
       3. b    ∀y isBossOf(b,y)   assume
       4. isBossOf(b,b)           ∀e 3 b
       5. ∃z isBossOf(z,z)        ∃i 4 b
  }
  6. ∃z isBossOf(z,z)             ∃e 1 2
}

. . . < -3 < -2 < -1 < 0 < 1 < 2 < 3 < . . .

4.4.1. Interpretations¶

When we write propositions in a logic, we use predicates and function symbols (e.g., ∀i (i*2)>i). An interpretation gives the meaning of

1. the underlying domain – what set of elements it names;

2. each function symbol – what answers it computes from its arguments from the domain; and

3. each predicate – which combinations of arguments from the domain lead to True answers and False answers.

Here is an example. Say we have the function symbols, +, -, *, /, and predicate symbols, >, =. What do these names and symbols mean? We must interpret them.

• The standard interpretation of arithmetic is that int names the set of all integers; +, -, *, / name integer addition, subtraction, multiplication, and division, and = and > name integer equality comparison and integer less-than comparison. With this interpretation of arithmetic, we can interpret propositions. For example, ∀i (i*2)>i interprets to False, and ∃j (j*j)=j interprets to True. If we use any extra, “constant names”, (e.g., pi), we must give meanings to the constants, also.

• Now, given function names +, -, *, /, and predicates, =, >, we can choose to interpret them in another way. For example, we might interpret the underlying domain as just the nonnegative integers. We can interpret +, *, /, >, = as the usual operations on ints, but we must give a different meaning to -. We might define m - n == 0, whenever n > m.

• Yet another interpretation is to say that the domain is just {0,1}; the functions are the usual arithmetic operations on 0,1, modulo 2; and > is defined 1 > 0 (and that’s it).

These three examples show that the symbols in a logic can be interpreted in multiple different ways. (In the chapter propositional logic, we called an interpretation a “context”. In this chapter, we see that a “context” is quite complex – domain, functions, and predicates.)

Here is a second example. There are no functions, and the predicates are isMortal(_), isLeftHanded(_), isMarriedTo(_,_). An interpretation might make all (living) members of the human race as the domain; make isMortal(h) True for every human, h; make isLeftHanded(j) True for exactly those humans, j, who are left handed; and set isMarriedTo(m,f) True for all pairs of humans m, f, who have their marriage document in hand.

You get the idea….

We can ask whether a proposition is True within one specific interpretation, and we can ask whether a proposition is True within all possible interpretations. This leads to the notions of soundness and completeness for predicate logic:

A sequent, P_1, P_2, ..., P_n |- Q is valid in an interpretation, I, provided that when all of P_1, P_2, ..., P_n are True in interpretation I, so is Q. The sequent is valid exactly when it is valid in all possible interpretations. We have these results for the rules of propositional logic plus ∀i, ∀e, ∃i, ∃e:

1. soundness: When we use the deduction rules to prove that P_1, P_2, ..., P_n |- Q, then the sequent is valid (in all possible interpretations).

2. completeness: When P_1, P_2, ..., P_n |- Q is valid (in all possible interpretations), then we can use the deduction rules to prove the sequent.

Note that, if P_1, P_2, ..., P_n |- Q is valid in just one specific interpretation, we are not guaranteed that our rules will prove it. This is a famous trouble spot: For centuries, mathematicians were searching for a set of deduction rules that could be used to build logic proofs of all the True propositions of arithmetic, that is, the language of int, +, -, *, /, >, =. No appropriate rule set was devised.

In the early 20th century, Kurt Gödel showed that it is impossible to formulate a sound set of rules customized for arithmetic that will prove exactly the True facts of arithmetic. Gödel showed this by formulating True propositions in arithmetic notation that talked about the computational power of the proof rules themselves, making it impossible for the proof rules to reason completely about themselves. The form of proposition he coded in logic+arithmetic stated “I cannot be proved”. If this proposition is False, it means the proposition can be proved. But this would make the rule set unsound, because it proved a False claim. The only possibility is that the proposition is True (and it cannot be proved). Hence, the proof rules remain sound but are incomplete.

Gödel’s construction, called diagonalization, opened the door to the modern theory of computer science, called computability theory, where techniques from logic are used to analyze computer programs. Computability theory tells us what problems computers cannot solve, and why, and so we shouldn’t try. (For example, it is impossible to build a program-termination checker that works on all programs – the checker won’t work on itself!) There is also an offshoot of computability theory, called computational complexity theory, that studies what can be solved and how fast an algorithm can solve it. These subjects can be studied in CIS 570 and CIS 575 respectively.

Given an interpretation of a predicate logic, we can say that the “meaning” of a proposition is exactly the set of interpretations in which the proposition is True. This returns us to the Boolean-algebra model of logic. Or, we can organize the interpretations so that an interpretation grows in its domain and knowledge over time. This takes us to the Kripke models. Or, we can introduce two new programming constructs, the abstract data type and the parametric polymorphic function and extend the Heyting interpretation.

All of these are possible and are studied in a typical second course on logic.