It’s possible to extend the natural deduction system we built for zeroeth order logic to first order logic by introducing new rules of inference, to include quantifiers. Writing down sound rules is more difficult than you might expect. At least one textbook, which I will not name, went through multiple editions, each with a different unsound set of rules, before finally finding a correct set.
The rules for equality are relatively straightforward, reflecting the familiar properties of reflexivity, symmetry and transitivity of the \({ = }\) sign.
For any parameter \({ A }\) we can derive a statement of the form \({ ( A = A ) }\).
From any statement of the form \({ ( A = B ) }\), where \({ A }\) and \({ B }\) are parameters, we can derive \({ ( B = A ) }\).
From any statements of the form \({ ( A = B ) }\) and \({ ( B = C ) }\), where \({ A }\), \({ B }\) and \({ C }\) are parameters, we can derive \({ ( A = C ) }\).
From any statement of the form \({ ( A = B ) }\), where \({ A }\) and \({ B }\) are parameters, and \({ P }\), where \({ P }\) is an expression, we can deduce \({ Q }\), where \({ Q }\) is the result of replacing one or more occurrences of \({ A }\) in \({ P }\) with \({ B }\) or one or more occurrences of \({ B }\) with \({ A }\).
In the last rule, note that we aren’t required to replace all occurrences, unlike in some of our substitution rules.
It’s the rules for quantifiers which tend to cause trouble.
The expressions \({ [ ¬ ( ∃ V . P ) ] }\) and \({ [ ∀ V . ( ¬ P ) ] }\) are freely interchangeable, where \({ V }\) is a variable and \({ P }\) is an expression.
The expressions \({ [ ¬ ( ∀ V . P ) ] }\) and \({ [ ∃ V . ( ¬ P ) ] }\) are freely interchangeable, where \({ V }\) is a variable and \({ P }\) is an expression.
From a statement of the form \({ ( ∀ V . P ) }\) we can deduce \({ \{ [ ∃ V . ( V = A ) ] ⊃ Q \} }\), where \({ V }\) is a variable, \({ P }\) is an expression, \({ A }\) is a parameter, and \({ Q }\) is the result of replacing all free occurrences of \({ V }\) in \({ P }\) by \({ A }\).
From a statement of the form \({ \{ [ ∃ V . ( V = A ) ] ∧ Q \} }\) we can deduce \({ ( ∃ V . P ) }\), where \({ V }\) is a variable, \({ P }\) is an expression, \({ A }\) is a parameter, and \({ Q }\) is the result of replacing all free occurrences of \({ V }\) in \({ P }\) by \({ A }\).
The expressions \({ ( ∃ V . P ) }\) and \({ \{ [ ∃ V . ( V = B ) ] ∧ R \} }\) are freely interchangeable, where \({ V }\) is a variable, \({ P }\) is an expression, \({ B }\) is a parameter not appearing in any statement available in the current scope, and \({ R }\) is the result of replacing all free occurrences of \({ V }\) in \({ P }\) by \({ B }\).
The expressions \({ ( ∀ V . P ) }\) and \({ \{ [ ∃ V . ( V = B ) ] ⊃ R \} }\) are freely interchangeable, where \({ V }\) is a variable, \({ P }\) is an expression, \({ B }\) is a parameter not appearing in any statement available in the current scope, and \({ R }\) is the result of replacing all free occurrences of \({ V }\) in \({ P }\) by \({ B }\).
Besides adding these three rules for equality and six rules for quantifiers we can remove one of our rules of inference from zeroeth order logic, the rule of substitution. It deals with the substitution of expressions for Boolean variables, but we have no Boolean variables in our language for first order logic so we would never be able to apply it. This is the only one of our original rules of inference which referred to Boolean variables so no other rule of inference is similarly affected.
We don’t need a replacement for the rule of substitution, but there are two useful rules we can add. Anything which could be proved with them could also be proved without them, but they are sound rules of inference and make some proofs considerably shorter.
In any expression we can replace all occurrences of any variable with no free occurrences in that expression with any variable not appearing in that expression.
In any available statement we may substitute any variable for any variable which does not appear in any hypothesis which was active in that statement’s scope, provided the substitution doesn’t convert free occurrences to bound ones.
If \({ S }\) is a tautology of zeroeth order logic then we can derive any statement in which replace each Boolean variable in \({ S }\) by an expression in first order logic, provided each occurrence of a Boolean variable is replaced by the same expression.
These mimic some uses of the rule of substitution from zeroeth order logic, to rename variables and to avoid repeating proofs for different substitution instances of the same tautology.
The limitation in the second rule to variables not appearing in active hypotheses is familiar from zeroeth order logic, and is needed for the same reason as there. The requirement that no free instances become bound is new, since we didn’t have free and bound occurrences in zeroth order logic. It’s there to ensure that we can, for example, deduce \[ ( ∀ v . \{ ∀ w . [ ∃ x . ( f v w x ) ] \} ) \] from \[ ( ∀ x . \{ ∀ y . [ ∃ z . ( f x y z ) ] \} ) \] but can’t deduce \[ ( ∀ z . \{ ∀ y . [ ∃ z . ( f z y z ) ] \} ) \] from it. To see why that would be a problem, consider the interpretation of first order logic where the domain is the natural numbers and \({ f }\) is sum relation, if \({ f x y z }\) means \({ x + y = z }\). In this case \[ ( ∀ x . \{ ∀ y . [ ∃ z . ( f x y z ) ] \} ) \] means \[ ( ∀ x . \{ ∀ y . [ ∃ z . ( x + y = z ) ] \} ) , \] which simply expresses the fact that the sum of any two natural numbers is a natural number. This is a true statement on this interpretation. On the other hand \[ ( ∀ z . \{ ∀ y . [ ∃ z . ( f z y z ) ] \} ) \] would mean \[ ( ∀ z . \{ ∀ y . [ ∃ z . ( z + y = z ) ] \} ) . \] The inner expression \({ z + y = z }\) means that adding \({ y }\) to \({ z }\) leaves \({ z }\) unchanged, which is true for \({ y = 0 }\) but not for any other \({ y }\). The larger expression \({ [ ∃ z . ( z + y = z ) ] }\) is therefore also true for \({ y = 0 }\). Since it’s not true for all \({ y }\) the larger expression \({ \{ ∀ y . [ ∃ z . ( z + y = z ) ] \} }\) is false. It’s false no matter what natural number is substituted for all free occurrences of \({ z }\) since there are no free occurrences of \({ z }\) in \({ \{ ∀ y . [ ∃ z . ( z + y = z ) ] \} }\). The full statement is therefore false. So the rule without this restriction would be unsound, since it would allow us to deduce a false statement from a true one in at least one intended interpretation. The phenomenon we’re ruling out is called “variable capture”, since it causes a free variable to become bound.
Although we haven’t formalised this yet, and can’t until we have a proper definition of computability, one of our requirements for a formal system is that questions of whether a statement follows from previous statements by a rule of inference must always be decidable. The second rule above satisfies this requirement because we’ve already introduced a procedure to check whether a statement in zeroeth order logic is a tautology.