Welcome back. In our previous lesson, we developed the crucial skill of translating natural language arguments into the precise syntax of first-order logic. We now have a formal language capable of expressing claims about objects, their properties, and relationships, using quantifiers like "for all" () and "there exists" (). However, translation is only half the battle. The ultimate goal is to rigorously determine the validity of these arguments.
This lesson equips you with the tools to do just that. We will extend the natural deduction system you're familiar with from propositional logic by adding four new inference rules—one introduction rule and one elimination rule for each of our two quantifiers. You will learn how to construct formal proofs for arguments in predicate logic, a process that is systematic and, given your background, should feel akin to building a mathematical proof or designing an algorithm. Two of these rules are straightforward extensions of our existing logic, while the other two require careful handling of assumptions and are the key to unlocking the full power of predicate proofs.
1. Extending Natural Deduction for Quantifiers
All the propositional logic rules you've learned (Modus Ponens, Conjunction Introduction, Reductio ad Absurdum, etc.) are still valid and will be the workhorses of our new proofs. We simply need to add rules to handle the quantifiers themselves. Our overall strategy will be to use these new rules to "strip away" the quantifiers, revealing a propositional core that we can work on with our existing tools, and then re-introduce quantifiers as needed to reach our conclusion.
Let's begin by watching an overview of the four new rules.
Natural Deduction for Quantifiers | Attic Philosophy
This video, "Natural Deduction for Quantifiers," provides a concise introduction to the four rules we will be covering.
Watch the introductory segment from the beginning. It sets the stage by explaining that we are simply adding four new rules to the propositional system we already know.
As the video suggests, we can group these rules into two pairs: the "straightforward" ones and the "tricky" ones. Let's start with the straightforward pair.
2. The Simple Rules: and
Universal Elimination ()
This rule is perhaps the most intuitive of all. It states that if a property holds for everything in a domain, then it must hold for any specific individual in that domain.
- Formal Rule: From a premise , you can infer , where is any constant or closed term.
- In English: From "All humans are mortal," you can infer "Socrates is mortal."
This rule is also known as Universal Instantiation. It allows us to move from a general, universal claim to a specific instance.
Natural Deduction for Quantifiers | Attic Philosophy
The same video provides a clear explanation of Universal Elimination.
Please watch the segment from Universal Elimination.
Existential Introduction ()
This rule works in the opposite direction. If you have established that a specific individual has a certain property, you can then validly conclude that something has that property.
- Formal Rule: From a premise , where is a constant or closed term, you can infer .
- In English: From "Socrates is a philosopher," you can infer "There exists a philosopher."
This rule is also known as Existential Generalization.
Natural Deduction for Quantifiers | Attic Philosophy
Now, let's look at the corresponding simple rule for the existential quantifier.
Please watch the explanation of Existential Introduction. Note the subtlety that you can choose to replace some or all occurrences of the constant with the new variable.
These two rules allow us to instantiate universal claims and create existential ones. They are the primary tools for moving from the quantified level to the level of specific instances and back.
3. The Complex Rules: and
The other two rules are more complex because they involve restrictions on how we reason with constants. They introduce the powerful concept of an eigenvariable (or "arbitrary name"), a placeholder constant that must be handled with care to ensure our reasoning remains valid. Given your mathematical training, you can think of the conditions on these rules as being analogous to the constraints required when proving a general theorem by considering an arbitrary element from a set.
For a formal definition of these rules and the crucial eigenvariable condition, the Open Logic Project text is an excellent resource.
This text from the Open Logic Project provides the rigorous, formal definitions of the quantifier rules.
Please read the section on "Quantifier Rules". Pay close attention to the definition of the eigenvariable condition. This is the formal heart of what makes the next two rules "tricky."
Universal Introduction ()
How can we prove a statement of the form ? We cannot check every single object. Instead, we must show that holds for an arbitrary constant . A constant is arbitrary if it has no special properties—it cannot have appeared in any premise or undischarged assumption of our proof. If we can prove a property for such a generic individual, we can generalize to all individuals.
- Formal Rule: If you have derived , you can infer , provided that the constant (the eigenvariable) does not appear in any undischarged assumption on which depends.
- Strategy: To prove , pick a fresh constant symbol that hasn't been used, and prove . Then, apply .
Natural Deduction for Quantifiers | Attic Philosophy
This video provides an excellent conceptual explanation for why this rule must be restrictive.
Watch the segment on Universal Introduction. The contrast between the valid and invalid examples of generalization is key to understanding the role of the "arbitrary name."
Existential Elimination ()
This is often considered the most complex rule. If we know , we know something has property , but we don't know what. We can't just infer for some known constant . The solution is to use a sub-proof.
- Formal Rule: If you have a premise , and you can derive a conclusion from the assumption , you can then assert outside that sub-proof. This is valid provided that the constant (the eigenvariable) does not appear in , in , or in any other undischarged assumption.
- Strategy: To use the premise , start a sub-proof. Assume for a fresh constant . Derive some conclusion that does not contain . You can then end the sub-proof and state as your new line.
Natural Deduction for Quantifiers | Attic Philosophy
Finally, let's examine the rule for using an existential statement.
Watch the detailed explanation of Existential Elimination. Focus on the sub-proof structure and the critical restriction that your conclusion cannot depend on the arbitrary individual you introduced.
4. A Complete Proof Deconstructed
With all four rules in hand, let's analyze a complete proof that uses them. The following proof shows that from the premise , we can validly conclude .
Let's walk through this proof step-by-step:
- Line 1: We assume the antecedent of the implication we want to prove. This is a standard strategy using the rule, which will be the final step.
- Line 2: We apply to line 1. Since the statement is true for all , it must be true for some arbitrary constant, which we'll call .
- Line 3: Now we have . To use this, we must start a sub-proof for . We assume an instance, using a new, fresh constant . So we assume .
- Line 4: Inside the sub-proof, we use a simple propositional rule, , to get .
- Line 5: The sub-proof (lines 3-4) has successfully derived . Crucially, the constant does not appear in . Therefore, we can export out of the sub-proof, completing our use of .
- Line 6: We have derived . The constant was introduced by a rule and does not appear in the original premise from which it was derived. It is therefore "arbitrary." We can apply to generalize from to .
- Lines 7-10: This is another, independent use of . The structure is identical to lines 3-5, but this time we derive .
- Line 7: Assume an instance for a new constant .
- Line 8: Use to get .
- Line 9: Use . Since we know , we know something is .
- Line 10: The sub-proof (7-9) derived . The constant is not in this conclusion. We can export it.
- Line 11: We have (line 6) and (line 10). We combine them with .
- Line 12: We apply , discharging our initial assumption from line 1. This completes the proof.
5. Strategy and Further Examples
Constructing these proofs requires not just knowing the rules, but knowing how to deploy them strategically. The process of removing quantifiers to reason propositionally and then re-adding them is central.
Chapter 5: Predicate Logic Proofs - UT Austin Computer Science
This guide from UT Austin's CS department provides an excellent high-level view of proof strategy.
First, read the section "Our Approach" to solidify the overall mental model for these proofs. Then, read the "Summary of the New Rules", which gives a crucial piece of strategic advice: perform Existential Instantiations (\exists E) before Universal Instantiations (\forall E) whenever possible. This is because \exists E requires a new name, while \forall E can use any name. By applying \exists E first, you create a constant that you can then specifically target with a later \forall E.
To see these rules and strategies in action with more examples, the following videos are highly recommended.
Natural Deduction for Quantifiers - Worked Examples | Attic Philosophy
This video provides two complete worked examples, focusing on the two "tricky" rules.
First, watch the walkthrough of a proof using Universal Introduction. Then, watch the walkthrough for a proof using Existential Elimination. Try to pause the video and complete the proofs yourself before watching the solution.
Conclusion
In this lesson, you have added the final four rules needed to complete our system of natural deduction for first-order logic. You now possess a complete toolkit for formally proving the validity of a vast range of arguments.
Key Takeaways:
- Natural deduction for predicate logic adds four rules to the propositional system:
- Universal Elimination (): From , infer for any term .
- Existential Introduction (): From , infer .
- Universal Introduction (): To prove , prove for a fresh, arbitrary constant .
- Existential Elimination (): To use , start a sub-proof assuming for a fresh constant , and derive a conclusion that doesn't mention .
- The rules and are governed by the eigenvariable condition, which ensures that the constants used for generalization or instantiation are truly arbitrary and do not carry illicit information.
- A common proof strategy is to apply elimination rules to break down premises, reason with propositional rules, and then apply introduction rules to build up the conclusion. It's often best to apply before .
Preview of the Next Lesson:
Now that we have the complete machinery for predicate logic proofs, we will apply it to a classic and historically significant class of arguments: syllogisms. We will see how arguments first analyzed by Aristotle, like "All men are mortal; Socrates is a man; therefore, Socrates is mortal," can be translated into predicate logic and formally proven valid using the rules you've just learned. This will demonstrate the power and elegance of our formal system.