Subsection 5.1.18 Checking Predicate Logic Proofs
StepWise (the proof checking tool that we used for Boolean logic) also works for predicate logic proofs.
We’ll soon see how to design nontrivial proofs using all of the rules at our disposal. But, before we do that, let’s practice using the instantiation and generalization rules that we’ve just learned.
Exercises Exercises
1.
Assume the following premises:
[1] ∀x (Dragon(x) → SpewsFire(x)) All dragons spew fire.
[2] ∃x (Dragon(x)) Dragons exist.
Prove:
∃x (SpewsFire(x)) Fire spewing creatures exist.
questionId: Dragon1
problemType: gradeLogicProof
questionTitle: Instantiation and Generalization Practice
questionDisplayText: Prove that fire-spewing dragons exist.
hints: Give a name to the dragon that we know must exist. What can you say about him/her/it?
[1] x (Dragon(x) SpewsFire(x)) Premise
[2] x (Dragon(x)) Premise
[3] Dragon(c*) Existential Instantiation [2]
[4] Dragon(c*) SpewsFire(c*) Universal Instantiation [1]
[5] SpewsFire(c*) Modus Ponens [3], [4]
[6] x (SpewsFire(x)) Existential Generalization [5]
2.
Assume the following premises:
[1] ¬∃x (Dragon(x) ∧ PetOwner(x)) No dragons own pets.
[2] ∀x (¬PetOwner(x) → Grumpy(x)) Anyone without a pet is grumpy.
Prove:
∀x (Dragon(x) → Grumpy(x)) All dragons are grumpy.
questionId: Dragon2
problemType: gradeLogicProof
questionTitle: Instantiation and Generalization Practice
questionDisplayText: Prove that all dragons are grumpy.
hints: 1. It is easier to work with quantified statements if they are not negated. 2. You need to derive an implication. Try using Conditional Disjunction to derive one from an or.
[1] x (Dragon(x) PetOwner(x)) Premise.
[2] x (PetOwner(x) Grumpy(x)) Premise.
[3] x ((Dragon(x) PetOwner(x))) Quantifier Exchange [1]
[4] x (Dragon(x) PetOwner(x)) De Morgan [3]
[5] x (Dragon(x) PetOwner (x)) Conditional Disjunction [4]
[6] Dragon(c) PetOwner (c) Universal Instantiation [5]
[7] PetOwner(c) Grumpy(c) Universal Instantiation [2]
[8] Dragon(c) Grumpy(c) Hypothetical Syllogism [6], [7]
[9] x (Dragon(x) Grumpy(x)) Universal Generalization [8]
3.
Let the universe over which ∀x quantifies be the set of dragons. Assume the following premise:
∀x (∃y (Tail(y) ∧ HasPart(x, y))) Every dragon has a tail.
Here’s a proposed proof that all dragons share the same tail:
[1] ∀x (y (Tail(y) ∧ HasPart(x, y))) Premise
[2] ∃y (Tail(y) ∧ HasPart(d, y)) Universal Instantiation [1]
[3] Tail(t*) ∧ HasPart(d, t*) Existential Instantiation [2]
[4] ∀x (Tail(t*) ∧ HasPart(x, t*)) Universal Generalization [3]
[5] ∃t (∀x (Tail(t) ∧ HasPart(x, t))) Existential Generalization [4]
Clearly it does not follow from our premise that all dragons share the same tail. So there’s at least one thing wrong with this proof. In which line did we make our first mistake? You should be able to explain exactly what we did wrong.
Line [2]
Line [3]
Line [4]
Line [5]
Explanation: The existentially quantified statement that we are instantiating occurs inside the scope of the universal quantifier. So we can’t assert that there’s some individual tail t*. We must assert that there’s some tail whose identity depends on the particular dragon we’re talking about. So, instead of instantiating to a value, t*, we must instantiate to something that is a function of d. Thus line [3] should have been:
[3] Tail(f(d)) HasPart(d, f(d)) Existential Instantiation [2]
(We didn’t need to name our function f. It could have been anything.) Now try to continue with the proof from here. You’ll see that we can’t reach the absurd conclusion about the one-tailed world of dragons.