Rules with ∀

Just as with our propositional logic operators, there will be two inference rules for each of our predicate logic quanitifiers – an “introduction rule and an “elimination” rule.

In this section, we will see the two inference rules for the universal (∀) quantifier.

For all elimination

For all elimination allows us to take a claim that uses a universal quantifier – a statement about ALL individuals in a domain – and make the same statement about a specific individual in the domain. After all, if the statement is true for ALL individuals, then it follows that it should be true for a particular individual. We can formalize the rule as follows:

     ∀ x P(x)
∀e: ----------- 
       P(v)     where v is a particular individual in the domain

Here is a simple example showing the syntax of the ∀e rule. It shows that given the premises: All humans are mortal and Socrates is a human, that we can prove that Socrates is mortal:

∀ x (isHuman(x) → isMortal(x)),  isHuman(Socrates) ⊢ isMortal(Socrates)
{
    1. ∀ x (isHuman(x) → isMortal(x))               premise
    2. isHuman(Socrates)                            premise
    3. isHuman(Socrates) → isMortal(Socrates)       ∀e 1 Socrates
    4. isMortal(Socrates)                           →e 3 2
}

We can read the justification ∀e 1 Socrates as: “for all elimination of the for-all statement on line 1, plugging in the individual Socrates”.

For all introduction

If we can show that a property of the form P(a) holds for an arbitrary member a of a domain, then we can use for all introduction to conclude that the property must hold for ALL individuals in the domain – i.e., that ∀ x P(x). We can formalize the rule as follows:

     { a              (a is fresh)
       ... P(a) }
∀i: ---------------
      ∀ x P(x) 

Here is a simple example showing the syntax of the ∀i rule: “Everyone is healthy; everyone is happy. Therefore, everyone is both healthy and happy.”:

∀ x isHealthy(x), ∀ y isHappy(y)  |-  ∀ z(isHealthy(z) ∧ isHappy(z))
{

  1. ∀ x isHealthy(x)                   premise
  2. ∀ y isHappy(y)                     premise
  3. {
       4. a
       5. isHealthy(a)                  ∀e 1 a
       6. isHappy(a)                    ∀e 2 a
       7. isHealthy(a) ∧ isHappy(a)     ∧i 5 6
  }
  8. ∀ z (isHealthy(z) ∧ isHappy(z))    ∀i 3
}

If we wish to introduce a for-all statement, the pattern is:

• Open a subproof and introduce an arbitrary/fresh individual in the domain (in the example above, we used a). It MUST be a name that we have not used elsewhere in the proof. The idea is that your individual could have been anyone/anything in the domain.

• When you introduce your individual, you do NOT include a justification on that line

• If you have other for-all statements available within the scope of the subproof, then it is often useful to use ∀e to plug your fresh individual into them. After all, if those statements are true for ALL individuals, then they are also true for your fresh individual.

• If you are trying to prove something of the form ∀ x P(x), then you need to reach P(a) by the end of the subproof. You need to show that your goal for-all statement holds for your fresh individual. In our case, we wished to prove ∀ z (isHealthy(z) ∧ isHappy(z)), so we reached isHealthy(a) ∧ isHappy(a) by the end of the subproof.

• After the subproof, you can use ∀i to introduce a for-all statement for your last claim in the subproof – that since the individual could have been anyone, then the proposition holds for ALL individuals. The ∀i justification needs the line number of the subproof.

• When you use ∀i, it does not matter what variable you introduce into the for-all statement. In the example above, we introduced ∀ z – but that was only to match the goal conclusion in the proof. We could have instead introduced ∀ x, ∀ y, ∀ people, etc. We would use whatever variable we chose in the rest of that proposition – i.e., ∀ z (isHealthy(z) ∧ isHappy(z)), or ∀ people (isHealthy(people) ∧ isHappy(people)), etc.

Examples

In this section, we will look at several proofs involving the universal quantifier.

Example 1

Suppose we wish to prove the following sequent:

∀ x P(x) ⊢ ∀ y P(y)

This will let us show that it doesn’t matter what variable we use with a universal quantifier – both ∀ x P(x) and ∀ y P(y) are saying the same thing: for all individuals, P holds for that individual.

Since the top-level operator of our conclusion is a for-all statement, we see that we will need to use for all introduction. Following the pattern above, we open a subproof and introduce a fresh individual, a. Since we wish to introduce the for-all statement ∀ y P(y), then we know we need to reach P(a) by the end of our subproof:

∀ x P(x) ⊢ ∀ y P(y)
{
    1. ∀ x P(x)         premise
    2. {
        3. a            //our fresh individual

        //need: P(a)
    }
    //want to use ∀i to conclude ∀ y P(y)
}

Since we have an available for-all statement in our subproof (∀ x P(x), from line 1), then we use ∀e to plug a into it:

∀ x P(x) ⊢ ∀ y P(y)
{
    1. ∀ x P(x)         premise
    2. {
        3. a            //our fresh individual
        4. P(a)         ∀e 1 a
        //need: P(a)
    }
    //want to use ∀i to conclude ∀ y P(y)
}

At that point, we see that we have exactly the proposition we wanted to end our subproof – P(a). All that remains is to use ∀i to state that since a could have been anyone, that the proposition we reached at the end of subproof 2 must hold for all individuals. Here is the completed proof:

∀ x P(x) ⊢ ∀ y P(y)
{
    1. ∀ x P(x)         premise
    2. {
        3. a            //our fresh individual
        4. P(a)         ∀e 1 a
        //need: P(a)
    }
    //want to use ∀i to conclude ∀ y P(y)
    5. ∀ y P(y)         ∀i 2
}

Example 2

Suppose we wish to prove that, given the following premises in the domain of people:

• All students have a phone and/or a laptop
• Everyone is a student

Then we can conclude:

• Everyone has a phone and/or a laptop

First, we identify the following predicates:

• isStudent(x) - whether person x is a student
• hasPhone(x) - whether person x has a phone
• hasLaptop(x) = whether person x has a laptop

Then, we can translate our premises and goal conclusion to predicate logic:

• All students have a phone and/or a laptop translates to: ∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x))
• Everyone is a student translates to: ∀ x isStudent(x)
• Everyone has a phone and/or a laptop translates to: ∀ x (hasPhone(x) ∨ hasLaptop(x))

We need to prove the following sequent:

∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)), ∀ x isStudent(x) ⊢ ∀ x (hasPhone(x) ∨ hasLaptop(x))

As with our previous example, we see that we are trying to prove a for-all statement (∀ x (hasPhone(x) ∨ hasLaptop(x))). This means we will need to open a subproof and introduce a fresh individual – perhaps bob. By the end of the subproof, we must show that our goal for-all statement holds for that individual – that hasPhone(bob) ∨ hasLaptop(bob). We start the proof as follows:

∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)), ∀ x isStudent(x) ⊢ ∀ x (hasPhone(x) ∨ hasLaptop(x))
{
    1. ∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x))          premise
    2. ∀ x isStudent(x)                                         premise
    3. {
        4. bob
        
        //goal: hasPhone(bob) ∨ hasLaptop(bob)
    }
    //use ∀i to conclude ∀ x (hasPhone(x) ∨ hasLaptop(x))
}

We have two available for-all statements within the subproof – x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)) and ∀ x isStudent(x). Since those propositions hold for all individuals, they also hold for bob. We use ∀e to plug in bob to those two propositions:

∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)), ∀ x isStudent(x) ⊢ ∀ x (hasPhone(x) ∨ hasLaptop(x))
{
    1. ∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x))          premise
    2. ∀ x isStudent(x)                                         premise
    3. {
        4. bob
        5. isStudent(bob) → hasPhone(bob) ∨ hasLaptop(bob)      ∀e 1 bob
        6. isStudent(bob)                                       ∀e 2 bob 
        //goal: hasPhone(bob) ∨ hasLaptop(bob)
    }
    //use ∀i to conclude ∀ x (hasPhone(x) ∨ hasLaptop(x))
}

Line 5 is an implies statement the form p → q, and line 6 is a statement of the form p. Thus we can use →e to conclude hasPhone(bob) ∨ hasLaptop(bob) (the “q” in that statement) – which is exactly what we needed to end the subproof. All that remains is to apply our ∀i rule after the subproof. Here is the completed proof:

∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x)), ∀ x isStudent(x) ⊢ ∀ x (hasPhone(x) ∨ hasLaptop(x))
{
    1. ∀ x (isStudent(x) → hasPhone(x) ∨ hasLaptop(x))          premise
    2. ∀ x isStudent(x)                                         premise
    3. {
        4. bob
        5. isStudent(bob) → hasPhone(bob) ∨ hasLaptop(bob)      ∀e 1 bob
        6. isStudent(bob)                                       ∀e 2 bob   
        7. hasPhone(bob) ∨ hasLaptop(bob)                       →e 5 6
        //goal: hasPhone(bob) ∨ hasLaptop(bob)
    }
    //use ∀i to conclude ∀ x (hasPhone(x) ∨ hasLaptop(x))
    8. ∀ x (hasPhone(x) ∨ hasLaptop(x))                         ∀i 3
}

Example 3

Next, suppose we wish to prove the following sequent:

∀ x (S(x) → Pz(x)), ∀ x (Pz(x) → D(x)), ∀ x ¬D(x) ⊢ ∀ x ¬S(x)

We again see that the top-level operator of what we are trying to prove is a universal quantifier. We use our strategy to open a subproof, introduce a fresh individual (maybe a), and plug that individual into any available for-all statements. Since we wish to prove ∀ x ¬S(x), then we will want to reach ¬S(a) by the end of the subproof. Here is a sketch:

∀ x (S(x) → Pz(x)), ∀ x (Pz(x) → D(x)), ∀ x ¬D(x) ⊢ ∀ x ¬S(x)
{
    1. ∀ x (S(x) → Pz(x))               premise
    2. ∀ x (Pz(x) → D(x))               premise
    3. ∀ x ¬D(x)                        premise
    4. {
        5. a
        6. S(a) → Pz(a)                 ∀e 1 a
        7. Pz(a) → D(a)                 ∀e 2 a
        8. ¬D(a)                        ∀e 3 a

        //goal: ¬S(a)
    }
    //use ∀i to conclude ∀ x ¬S(x)
}

Now, we see that our goal is to reach ¬S(a) by the end of the subproof – so we need to prove something whose top-level operator is a NOT. We recall that we have a strategy to prove NOT(something) from propositional logic – we open a subproof, assuming something (S(a), in our case), try to get a contradiction, and use NOT introduction after the subproof to conclude NOT (something) (¬S(a) for us). Here is the strategy:

∀ x (S(x) → Pz(x)), ∀ x (Pz(x) → D(x)), ∀ x ¬D(x) ⊢ ∀ x ¬S(x)
{
    1. ∀ x (S(x) → Pz(x))               premise
    2. ∀ x (Pz(x) → D(x))               premise
    3. ∀ x ¬D(x)                        premise
    4. {
        5. a
        6. S(a) → Pz(a)                 ∀e 1 a
        7. Pz(a) → D(a)                 ∀e 2 a
        8. ¬D(a)                        ∀e 3 a
        9. {
            10. S(a)                    assume

            //goal: contradiction
        }
        //use ¬i to conclude ¬S(a)

        //goal: ¬S(a)
    }
    //use ∀i to conclude ∀ x ¬S(x)
}

We can complete the proof as follows:

∀ x (S(x) → Pz(x)), ∀ x (Pz(x) → D(x)), ∀ x ¬D(x) ⊢ ∀ x ¬S(x)
{
    1. ∀ x (S(x) → Pz(x))               premise
    2. ∀ x (Pz(x) → D(x))               premise
    3. ∀ x ¬D(x)                        premise
    4. {
        5. a
        6. S(a) → Pz(a)                 ∀e 1 a
        7. Pz(a) → D(a)                 ∀e 2 a
        8. ¬D(a)                        ∀e 3 a
        9. {
            10. S(a)                    assume
            11. Pz(a)                   →e 6 10
            12. D(a)                    →e 7 11
            13. ⊥                       ¬e 12 8
            //goal: contradiction
        }
        //use ¬i to conclude ¬S(a)
        14. ¬S(a)                       ¬i 9

        //goal: ¬S(a)
    }
    //use ∀i to conclude ∀ x ¬S(x)
    15. ∀ x ¬S(x)                       ∀i 4
}

Rules with ∃

In this section, we will see the two inference rules for the existential (∃) quantifier.

Exists introduction

We can use the exists introduction rule, ∃i, when we have a proposition of the form P(a) for an arbitrary member a of a domain. Since we found one individual where a proposition held, then we can also say that there exists an individual for which the proposition is true. We can formalize the rule as follows:

       P(d)         where  d  is an individual
∃i: -----------
      ∃ x P(x)

Here is a simple example showing the syntax of the ∃i rule:

isHuman(Socrates) ⊢  ∃ x isHuman(x)
{
    1. isHuman(Socrates)            premise
    2. ∃ x isHuman(x)               ∃i 1 Socrates
}

When we use the ∃i rule to justify a claim like ∃ x P(x), we include the line number of where the proposition held for a particular individual, as well as the name of the individual. In the proof above, we claim ∃ x isHuman(x) with justification ∃i 1 Socrates – line 1 corresponds to isHuman(Socrates), where our ∃ x isHuman(x) proposition held for a particular individual. The Socrates part of the justification is the name of the individual.

Note that we can use the ∃i rule to introduce any variable, not just x. You can choose which variable to introduce based on the variables used in the conclusion. For example, the following proof is also valid:

isHuman(Socrates) ⊢  ∃ z isHuman(z)
{
    1. isHuman(Socrates)            premise
    2. ∃ z isHuman(z)               ∃i 1 Socrates
}

Exists elimination

Since the ∃i-rule constructs propositions that begin with ∃, the ∃e-rule (exists elimination) disassembles propositions that begin with ∃.

Here is a quick example (where our domain is living things):

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

We don’t know the name of the human, but it does not matter. Since ALL humans are mortal and SOMEONE is human, then our anonymous human must be mortal. The steps will go like this:

• Since “someone is human” and since we do not know his/her name, we will just make up our own name for them – “Jane”. So, we assume that “Jane is human”.

• We use the logic rules we already know to prove that “Jane is mortal”.

• Therefore, SOMEONE is mortal and their name does not matter.

This approach is coded into the last logic law, ∃e (exists elimination).

Suppose we have a premise of the form ∃ x P(x). Since we do not know the name of the individual “hidden” behind the ∃ x, we make up a name for it, say a, and discuss what must follow from the assumption that P(a) holds true. Here is the formalization of the ∃e rule:

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

That is, if we can deduce Q from P(a), and we do not mention a within Q, then it means Q can be deduced no matter what name the hidden individual has. So, Q follows from ∃ P(x).

We can work the previous example, with ∃e:

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

We make up the name, jane, for the human whose name we do not know:

∀ 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. jane isHuman(jane)               assume
        5. isHuman(jane) → isMortal(jane)   ∀e 1 jane
        6. isMortal(jane)                   →e 5 4
        7. ∃y isMortal(y)                   ∃i 6 jane
    }
    8. ∃y isMortal(y)                       ∃e 2 3
}

Line 4 proposes the name jane and the assumption that isHuman(jane). The subproof leads to Line 7, which says that someone is mortal. (We never learned the individual’s name!) Since Line 7 does not explicitly mention the made-up name, jane, we use Line 8 to repeat Line 7 – without knowing the name of the individual “hiding” inside Line 2, we made a subproof that proves the result, anyway. This is how ∃e works.

Note that when we use the ∃e rule as a justification we include first the line number of the there-exists statement that we processed (by naming the hidden individual) in the previous subproof, and then the line number of that subproof. In the example above, we say ∃e 2 3 because line 2 includes the there-exists statement we processed (∃ x isHuman(x)) in the previous subproof and line 3 is the subproof.

When using ∃e, the previous subproof must begin with introducing a name for a hidden individual in a there-exists statement and then immediately substituting that name into the there-exists statement. The justification on the first line is always assume. The last line in the subproof should contain NO mention of the chosen name. Whatever we claim on the last line in the subproof, we must claim EXACTLY the same thing immediately afterwards when we use the ∃e rule.

You are welcome to use any name for the hidden individual – not just jane or a. The only restriction is that you cannot have used the name anywhere else in the proof.

Examples

In this section, we will look at several proofs involving the existential quantifier.

Example 1

Suppose we wish to prove the following sequent:

∃ x (Human(x)) ⊢ ∃ y (Human(y))

Following the same approach in the ∃e example above, we know that there is SOME human. Let’s introduce the alias bob for that human:

∃ x (Human(x)) ⊢ ∃ y (Human(y))
{
    1. ∃ x (Human(x))               premise
    2. {
        3. bob Human(bob)           assume

        //goal: get to our conclusion, ∃ y (Human(y))
    }
    //use ∃e to restate our conclusion, since we know SOME such human exists
}

Since we have Human(bob) in our subproof, we can use ∃i in our subproof to instead say that there exists some human. We will introduce the y variable, since that’s what we want in our conclusion:

∃ x (Human(x)) ⊢ ∃ y (Human(y))
{
    1. ∃ x (Human(x))               premise
    2. {
        3. bob Human(bob)           assume
        4. ∃ y (Human(y))           ∃i 3 bob

        //goal: get to our conclusion, ∃ y (Human(y))
    }
    //use ∃e to restate our conclusion, since we know SOME such human exists
}

All that remains is to use ∃e to restate our conclusion after the subproof. Since we knew someone was a human, and since we reached a claim that didn’t use our alias, then we can restate the result outside the scope of the subproof:

∃ x (Human(x)) ⊢ ∃ y (Human(y))
{
    1. ∃ x (Human(x))               premise
    2. {
        3. bob Human(bob)           assume
        4. ∃ y (Human(y))           ∃i 3 bob

        //goal: get to our conclusion, ∃ y (Human(y))
    }
    //use ∃e to restate our conclusion, since we know SOME such human exists
    5. ∃ y (Human(y))               ∃e 1 2
}

Example 2

Suppose we wish to prove the following sequent:

∃ x (Adult(x) ∨ Kid(x)) ⊢ (∃ x Adult(x)) ∨ (∃ x Kid(x))

We will begin as we did previously: by introducing an alias for our person that is either an adult or a kid (say, alice):

∃ x (Adult(x) ∨ Kid(x)) ⊢ (∃ x Adult(x)) ∨ (∃ x Kid(x))
{
    1. ∃ x (Adult(x) ∨ Kid(x))              premise
    2. {
        3. alice Adult(alice) ∨ Kid(alice)  assume

        //goal: get to our conclusion, (∃ x Adult(x)) ∨ (∃ x Kid(x))
    }
    //use ∃e to restate our conclusion, since we know SOME such person is either an adult or kid
}

To finish our proof, we can use OR elimination on Adult(alice) ∨ Kid(alice), and then ∃e afterwards to restate our conclusion. Here is the completed proof:

∃ x (Adult(x) ∨ Kid(x)) ⊢ (∃ x Adult(x)) ∨ (∃ x Kid(x))
{
    1. ∃ x (Adult(x) ∨ Kid(x))                  premise
    2. {
        3. alice Adult(alice) ∨ Kid(alice)      assume
        4. {
            5. Adult(alice)                     assume
            6. ∃ x Adult(x)                     ∃i 5 alice
            7. (∃ x Adult(x)) ∨ (∃ x Kid(x))    ∨i1 6
        }
        8. {
            9. Kid(alice)                       assume
            10. ∃ x Kid(x)                      ∃i  9 alice
            11. (∃ x Adult(x)) ∨ (∃ x Kid(x))   ∨i2 10
        }
        12. (∃ x Adult(x)) ∨ (∃ x Kid(x))       ∨e 3 4 8

        //goal: get to our conclusion, (∃ x Adult(x)) ∨ (∃ x Kid(x))
    }
    //use ∃e to restate our conclusion, since we know SOME such person is either an adult or kid

    13. (∃ x Adult(x)) ∨ (∃ x Kid(x))           ∃e 1 2
}

Example 3

Suppose we wish to prove the following (in the domain of living things):

• All bunnies are fluffy
• There is a fast bunny
• Therefore, there is a creature that is fast and fluffy

We can translate our premises and desired conclusion to predicate logic, and write the following sequent:

∀ x (Bunny(x) → Fluffy(x)), ∃ x (Fast(x) ∧ Bunny(x)) ⊢ ∃ x (Fast(x) ∧ Fluffy(x))

Since we are trying to prove a claim about some individual, it makes sense that we would start the process of an ∃e subproof where we introduce an alias (thumper) for the fast bunny. We will try to reach the conclusion by the end of that subproof. Here is the setup:

∀ x (Bunny(x) → Fluffy(x)), ∃ x (Fast(x) ∧ Bunny(x)) ⊢ ∃ x (Fast(x) ∧ Fluffy(x))
{
    1. ∀ x (Bunny(x) → Fluffy(x))                   premise
    2. ∃ x (Fast(x) ∧ Bunny(x))                     premise
    3. {
        4. thumper Fast(thumper) ∧ Bunny(thumper)   assume
        5. Fast(thumper)                            ∧e1 4
        6. Bunny(thumper)                           ∧e2 4

        //goal: ∃ x (Fast(x) ∧ Fluffy(x))
    }

    //use ∃e to restate ∃ x (Fast(x) ∧ Fluffy(x)), since we know there is SOME fast bunny
}

To finish our subproof, we see that we have a proposition about all creatures (∀ x (Bunny(x) → Fluffy(x))) and that we are working with an individual creature (thumper). We can use ∀e to prove Bunny(thumper) → Fluffy(thumper). After that, we have a few more manipulations using propositional logic rules, our ∃i rule to transition our claim from being about our alias thumper to being about an unnamed individual, and then our ∃e rule to pull our final claim out of the subproof. Here is the completed proof:

∀ x (Bunny(x) → Fluffy(x)), ∃ x (Fast(x) ∧ Bunny(x)) ⊢ ∃ x (Fast(x) ∧ Fluffy(x))
{
    1. ∀ x (Bunny(x) → Fluffy(x))                   premise
    2. ∃ x (Fast(x) ∧ Bunny(x))                     premise
    3. {
        4. thumper Fast(thumper) ∧ Bunny(thumper)   assume
        5. Fast(thumper)                            ∧e1 4
        6. Bunny(thumper)                           ∧e2 4
        7. Bunny(thumper) → Fluffy(thumper)         ∀e 1 thumper
        8. Fluffy(thumper)                          →e 7 6
        9. Fast(thumper) ∧ Fluffy(thumper)          ∧i 5 8
        10. ∃ x (Fast(x) ∧ Fluffy(x))               ∃i 9 thumper

        //goal: ∃ x (Fast(x) ∧ Fluffy(x))
    }
    //use ∃e to restate ∃ x (Fast(x) ∧ Fluffy(x)), since we know there is SOME fast bunny

    11. ∃ x (Fast(x) ∧ Fluffy(x))                   ∃e 2 3
}

Nested Quantifiers

Our examples so far have included propositions with single quantifiers. This section will discuss how to prove sequents that use nested quantifers. We will see that the approach is the same as before, but that we must take caution to process the quantifiers in the correct order. Recall that quantifier precedence is from right to left (i.e., from the outside in), so that ∀ x ∀ y P(x, y) is equivalent to ∀ x (∀ y P(x, y)).

Example 1

Suppose we wish to prove the following sequent:

∀ x ∀ y P(x, y) ⊢ ∀ y ∀ x P(y, x)

Since we wish to prove a for-all statement of the form ∀ y (SOMETHING), then we know we must start with our for all introduction template:

∀ x ∀ y P(x, y) ⊢ ∀ y ∀ x P(y, x)
{
    1. ∀ x ∀ y P(x, y)              premise
    2. {
        3. a 
        
        //need: ∀ x P(a, x)
    }
    //want to use ∀i to conclude ∀ y ∀ x P(y, x)
}

But now we see that we want to prove ANOTHER for-all statement, ∀ x P(a, x). So we again use our for all introduction strategy in a nested subproof:

∀ x ∀ y P(x, y) ⊢ ∀ y ∀ x P(y, x)
{
    1. ∀ x ∀ y P(x, y)              premise
    2. {
        3. a 
        4. {
            5. b

            //need: P(a, b)
        }
        //want to use ∀i to conclude ∀ x P(a, x)

        //need: ∀ x P(a, x)
    }
    //want to use ∀i to conclude ∀ y ∀ x P(y, x)
}

Now, in subproof 4, we see that we must use ∀e on our premise (∀ x ∀ y P(x, y)) to work towards our goal of P(a, b). We have two available individuals – a and b. When we use ∀e, we must eliminate the OUTER (top-level) quantifier and its variable. In the case of ∀ x ∀ y P(x, y), we see that we must eliminate the ∀ x. Since the x is the first parameter in P(x, y), and since we are hoping to reach P(a, b) by the end of subproof 4, we can see that we need to plug in the a for the x so that it will be in the desired position:

∀ x ∀ y P(x, y) ⊢ ∀ y ∀ x P(y, x)
{
    1. ∀ x ∀ y P(x, y)              premise
    2. {
        3. a 
        4. {
            5. b
            6. ∀ y P(a, y)          ∀e 1 a

            //need: P(a, b)
        }
        //want to use ∀i to conclude ∀ x P(a, x)

        //need: ∀ x P(a, x)
    }
    //want to use ∀i to conclude ∀ y ∀ x P(y, x)
}

Note that on line 6, we could NOT have used ∀e to eliminate the ∀ y in ∀ x ∀ y P(x, y), as it was not the top-level operator.

Next, we apply ∀e again to ∀ y P(a, y) to leave us with P(a, b). All that remains at that point is to use ∀i twice as planned to wrap up the two subproofs. Here is the completed proof:

∀ x ∀ y P(x, y) ⊢ ∀ y ∀ x P(y, x)
{
    1. ∀ x ∀ y P(x, y)              premise
    2. {
        3. a 
        4. {
            5. b
            6. ∀ y P(a, y)          ∀e 1 a
            7. P(a, b)              ∀e 6 b

            //need: P(a, b)
        }
        //want to use ∀i to conclude ∀ x P(a, x)

        8. ∀ x P(a, x)              ∀i 4

        //need: ∀ x P(a, x)
    }
    //want to use ∀i to conclude ∀ y ∀ x P(y, x)

    9. ∀ y ∀ x P(y, x)              ∀i 2
}

Example 2

Suppose we have the predicate IsBossOf(x, y) in the domain of people, which describes whether person x is the boss of person y. We wish to prove the following sequent:

∃ x ∀ y IsBossOf(x, y) ⊢ ∀ y ∃ x IsBossOf(x, y)

You can read the premise as “There is a person that is everyone’s boss”. From this statement, we are trying to prove the conclusion: “All people have a boss”. Here is the completed proof:

∃ x ∀ y IsBossOf(x, y) ⊢ ∀ y ∃ x IsBossOf(x, y)
{
  1. ∃ x ∀ y IsBossOf(x, y)             premise
  2. {
       3. a ∀ y IsBossOf(a, y)          assume
       4. {
            5. b
            6. IsBossOf(a, b)           ∀e 3 b
            7. ∃ x IsBossOf(x, b)       ∃i 6 a
       }
       8. ∀ y ∃ x IsBossOf(x, y)        ∀i 4
  }
  9. ∀ y ∃ x IsBossOf(x, y)             ∃e 1 2
}

In the above proof, we let a be our made-up name for the boss-of-everyone. So, we have the assumption that ∀ y IsBossOf(a, y). Next, we let b be “anybody at all” who we might examine in the domain of people. The proof exposes that the boss of “anybody at all” in the domain must always be a. ∀i and then ∃e finish the proof.

Here is the proof worked again, with the subproofs swapped:

∃ x ∀ y IsBossOf(x, y) ⊢ ∀ y ∃ x IsBossOf(x, y)
{
  1. ∃ x ∀ y IsBossOf(x, y)             premise
  2. {
       3. b
       4. {
            5. a ∀ y IsBossOf(a, y)     assume
            6. IsBossOf(a, b)           ∀e 5 b
            7. ∃ x IsBossOf(x, b)       ∃i 6 a
       }
       8. ∃ x IsBossOf(x, b)            ∃e 1 4
  }
  9. ∀ y ∃ x IsBossOf(x, y)             ∀i 2
}

Can we prove the converse? That is, if everyone has a boss, then there is one boss who is the boss of everyone?

∀ y ∃ x IsBossOf(x, y) ⊢ ∃ x ∀ y IsBossOf(x, y)

NO. We can try, but we get stuck:

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

    ...can't finish
}

We see that the “block structure” of the proofs warns us when we are making invalid deductions.

Equivalence

In Chapter 5, we saw DeMorgan’s laws for quantifiers – that if we have some domain, and if P(x) is a predicate for individuals in that domain, then the following statements are equivalent:

• ¬(∃ x P(x)) is equivalent to ∀ x ¬P(x)
• ¬(∀ x P(x)) is equivalent to ∃ x ¬P(x)

The process of proving that two predicate logic statements are equivalent is the same as it was in propositional logic – we must prove the second proposition using the first as a premise, and we must prove the first given the second as a premise.

Example - how to prove equivalence

For example, to prove that ¬(∃ x P(x)) is equivalent to ∀ x ¬P(x), we must prove the sequents:

¬(∃ x P(x)) ⊢ ∀ x ¬P(x)

and

∀ x ¬P(x) ⊢ ¬(∃ x P(x))

We prove both directions below:

¬(∃ x P(x)) ⊢ ∀ x ¬P(x)
{
    1. ¬(∃ x P(x))              premise
    2. {
        3. a
        4. {
            5. P(a)             assume
            6. ∃ x P(x)         ∃i 5 a
            7. ⊥                ¬e 6 1
        }
        8. ¬P(a)                ¬i 4
    }
    9. ∀ x ¬P(x)                ∀i 2
}

and

∀ x ¬P(x) ⊢ ¬(∃ x P(x))
{
    1. ∀ x ¬P(x)                premise
    2. {
        3. ∃ x P(x)             assume
        4. {
            5. a P(a)           assume
            6. ¬P(a)            ∀i 1 a
            7. ⊥                ¬e 5 6
        }
        8. ⊥                    ∃e 3 4
    }
    9. ¬(∃ x P(x))              ¬i 2
}

More extensive list of equivalences

Here is a more extensive list of equivalences in predicate logic. The remaining proofs are left as exercises for the reader:

• ¬(∃ x P(x)) is equivalent to ∀ x ¬P(x)
• ¬(∀ x P(x)) is equivalent to ∃ x ¬P(x)
• ∀ x (P(x) → ¬Q(x)) is equivalent to ¬(∃ x P(x) ∧ Q(x))
• ∀ x ∀ y P(x, y) is equivalent to ∀ y ∀ x P(x, y)
• ∃ x ∃ y P(x, y) is equivalent to ∃ y ∃ x P(x, y)
• Q ∧ (∀ x P(x)) is equivalent to ∀ x (Q ∧ P(x)) (where x does not appear in Q)
• Q v (∀ x P(x)) is equivalent to ∀ x (Q V P(x)) (where x does not appear in Q)
• Q ∧ (∃ x P(x)) is equivalent to ∃ x (Q ∧ P(x)) (where x does not appear in Q)
• Q V (∃ x P(x)) is equivalent to ∃ x (Q V P(x)) (where x does not appear in Q)

Summary and Strategies

In this section, we summarize all available rules in propositional logic, and discuss strategies for approaching proofs.

Rules with universal quantifier (∀)

Rule summaries:

     ∀ x P(x)
∀e: ----------- 
       P(v)     where v is a particular individual in the domain

     { a              (a is fresh)
       ... P(a) }
∀i: ---------------
      ∀ x P(x) 

Rule syntax summaries:

{ 
    ...
    r. ∀ x P(x) 	        (...)
    s. P(v)                 ∀e r v
    ...
}

{ 
    ...
    r. {
        s. a
        ...
        t. P(a)             (...)
    }
    u. ∀ x P(x)             ∀i r
}

Rules with existential quantifier (∃)

Rule summaries:

       P(d)         where  d  is an individual
∃i: -----------
      ∃ x P(x)

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

Rule syntax summaries:

{
    ...
    r. P(d)                 (...)
    s. ∃ x P(x)             ∃i r d
    ...
}

{
    ...
    b. ∃ x P(x)             (...)
    c. {
        d. a P(a)           assume
        ...
        e. Q                (...)
    }
    f. Q                    ∃e b c
}

Reminder: propositional logic rules are still available

When doing proofs in predicate logic, remember that all the deduction rules from propositional logic are still available. You will often want to use the same strategies we saw there – not introduction to prove a NOT, implies introduction to create an implies statement, OR elimination to process an OR statement, etc.

However, keep in mind that propositional logic rules can only be used on claims without quantifiers as their top-level operator. For example, if we have the statement ∀ x (S(x) ∧ Pz(x)), then we cannot use ∧e – the top-level operator is a universal quantifier, and the ∧ statement is “bound up” in that quantifier. We would only be able to use ∧e after we had used ∀ e to eliminate the quantifier.

Strategies

1. Write down all premises first. Can you extract anything from the premises?

   • If you have a for-all statement and an available individual, use ∀e to plug that individual into the for-all statement.
   • If you have p∧q, use ∧e1 to extract p by itself and then ∧e2 to extract q by itself.
   • If you have p→q and p, use →e to get q.
   • If you have p and ¬p, use ¬e to claim a contradiction, ⊥.

2. Look at the top-level operator of what you are trying to prove.

   • Are you trying to prove something of the form ∀ x P(x)?

     • Use ∀i. Open a subproof, introduce a fresh a, and get to P(a) by the end of the subproof. After the subproof, use ∀i to conclude ∀ x P(x).

   • Are you trying to prove something of the form ∃ x P(x)?

     • You will usually have another there-exists (∃) statement available as a premise or previous claim. Open a subproof, and assume an alias for the individual in your there-exists statement. Get to ∃ x P(x) by the last line of the subproof. After the subproof, use ∃e to restate ∃ x P(x).

   • Are you trying to prove something of the form p→q?

     • Use →i. Open a subproof, assume p, and get to q by the end of the subproof. After the subproof, use →i to conclude p→q.

   • Are you trying to prove something of the form ¬p?

     • Use ¬i. Open a subproof, assume p, and get a contradiction, ⊥, by the end of the subproof. After the subproof, use ¬i to conclude ¬p.

   • Are you trying to prove something of the form p ∧ q?

     • Try to prove p by itself and then q by itself. Afterward, use ∧i to conclude p ∧ q.

   • Are you trying to prove something of the form p ∨ q?

     • See if you have either p or q by itself – if you do, use either ∨i1 or ∨i2 to conclude p ∨ q.

3. You’ll need to nest the approaches from step 2. Once you are in a subproof, think about what you are trying to prove by the end of that subproof. Follow the strategy in step 2 to prove your current goal, nesting subproofs as needed. As you work, stop and scan the claims that you have available. See if you can extract anything from them as you did for the premises in step 1.

4. No match, or still stuck?

   • Do you have a there-exists statement available? Try using ∃e to reach your goal.
   • Do you have an OR statement available? Try using OR elimination to prove your goal conclusion.
   • Do your statements have NOT operators, but don’t fit the form for using ¬i? Try using pbc. If you are trying to prove something of the form p, open a subproof, assume ¬p, and try to reach a contradiction by the end of the subproof. Afterward, use pbc to conclude p.
   • As a last resort, try pasting in the proof for the law of the excluded middle (see section 4.5). Then use OR elimination on p ∨ ¬p.

Think of doing a proof as solving a maze, and of all our deduction rules as possible directions you can turn. If you have claims that match a deduction rule, then you can try applying the rule (i.e, “turning that direction”). As you work, you may apply more and more rules until the proof falls into place (you exit the maze)…or, you might get stuck. If this happens, it doesn’t mean that you have done anything wrong – it just means that you have reached a dead end and need to try something else. You backtrack, and try a different approach instead (try turning in a different direction).

Soundness and Completeness

Soundness and completeness definitions

We now revisit the notions of soundness and completeness. We recall from propositional logic that a proof system is sound if everything that is provable is actually true. A proof system is complete if everything that is true can be proved.

Interpretations

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

• The underlying domain – what set of elements it names

• Each function symbol – what answers it computes from its parameters from the domain

• Each predicate – which combinations of arguments from the domain lead to true answers and false answers

Interpretation example - integers

Here is an example. Say we have the function symbols: +, -, *, and /, and the predicate symbols: > and =. 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

• +, -, *, and / name the integer addition, subtraction, multiplication, and division functions (that take two integers as “parameters” and “return” an integer result)

• = and > name integer equality comparison and integer less-than comparison predicates (that take two integers as “parameters” and “return” the boolean result of the comparison)

With this interpretation of arithmetic, we can interpret statements. For example,∀ i (i * 2) > i interprets to false, as when i is negative, then i * 2 < i. Similarly, ∃ j (j * j) = j interprets to true, as 1 * 1 = 1.

Now, given the function names +, -, *, /, and the 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 and 1 under the modulus of 2. For example, we would define 1 + 1 == 0 because (1 + 1) mod 2 == 0. We would define 1 > 0 as true and any other evaluation of < as false.

These three examples show that the symbols in a logic can be interpreted in multiple different ways.

Interpretation example - predicates

Here is a second example. There are no functions, and the predicates are IsMortal(_), IsLeftHanded(_) and IsMarriedTo(,). An interpretation might make all (living) members of the human race as the domain; make IsMortal(h) defined as true for every human h; make IsLeftHanded(j) defined as true for exactly those humans, j, who are left handed; and set IsMarriedTo(x, y) as true for all pairs of humans (x, y) who have their marriage document in hand.

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.

Valid sequents in 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, then so is Q. The sequent is valid exactly when it is valid in ALL possible interpretations.

Soundness and completeness in predicate logic

We can then define soundness and completeness for predicate logic:

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)

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, then 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, +, -, *, /, >, and =. 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. You can study these topics more in CIS 570 and CIS 575.

Computability theory includes the notion of decidability – a problem that is decidable CAN be solved by a computer, and one that is undecidable cannot. A famous example of an undecidable problem is the Halting problem: given an arbitrary computer program and program input, can we write a checker program that will tell if the input program will necessarily terminate (halt) on its input? The answer is NO - the checker wouldn’t work on itself.