First-order natural deduction extends the truth-functional logic (TFL) system by adding 8 new rules while retaining all previous TFL rules. This creates a complete system for proving and analyzing first-order logic arguments.
1. Universal Quantifier Rules
A. Universal Elimination (∀E)
The simplest of the new rules
Purpose: From a universal statement, derive specific instances
Example: From "Everything is red" → "This specific thing is red"
Key points:
Can replace universal variable with ANY name
Must replace EVERY instance of the variable with the same name
No restrictions on which name to use
Works because if something is true for everything, it's true for any specific thing
B. Universal Introduction (∀I)
More complex rule involving arbitrary names
Purpose: To prove something is true for everything
Key concept: Arbitrary names
Functions as a placeholder
Doesn't refer to any specific thing
Like saying "Let's call it Steve" without caring who Steve is
Requirements:
The name used must not appear in any undischarged assumptions
Must not appear in opening assumptions or sub-proof assumptions
Must replace every instance of the name
The variable can't already be in the sentence
Logic: If we can prove something for an arbitrary case, it must work for all cases