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.
We need four rules of inference, which correspond to the four tableau rules. The ones corresponding to the two unrestricted tableau rules are mostly unproblematic. One rule says that from a statement of the form \({ [ ∀ V . ( P V ) ] }\) we can deduce one of the form \({ ( P A ) }\) and the other says that from a statement of the form \({ ( P A ) }\) we can deduce one of the from \({ [ ∃ V . ( P V ) ] }\). The first of these is an exact translation of one of our tableau rules and the second can be thought of as the contrapositive of another of our rules.
There is one subtlety of these rules which should be pointed out. Applying those two rules in the order stated takes us from \({ [ ∀ V . ( P V ) ] }\) to \({ ( P A ) }\) to \({ [ ∃ V . ( P V ) ] }\). If we allowed interpretations where the domain is empty then these rules would be unsound. \({ [ ∀ V . ( P V ) ] }\) would always be true, no matter which variable and expression \({ V }\) and \({ P }\) represent because a universal statement is true unless there is some counterexample in the domain and an empty domain can contain no counterexample. On the other hand \({ [ ∃ V . ( P V ) ] }\) is false, again no matter which variable and expression \({ V }\) and \({ P }\) represent, because an existential statement can only be true if there is an example in the domain and there can be no example in an empty domain.
If you want something like first order logic but which is applicable to domains which are not known in advance to be non-empty then you need inclusive logic, which has a different set of rules of inference for quantifiers, rather than first order logic. Inclusive logic is also known as universally free logic or just free logic, although the latter name is dangerous because is is also used for something intermediate between inclusive logic and first order logic.
Besides not assuming the domain is non-empty inclusive logic also allows for parameters which might not refer to any element of the domain. This is more useful than it sounds. You can’t safely apply first order logic to a language which includes phrases like “the current king of France” but it’s hard to build a language which excludes such phrases but includes “the current king of Norway”, who does exist. English certainly makes no attempt to do prevent references to things which don’t exist and therefore essentially all “real world” examples you find in logic textbooks are suspect. Standard mathematical language also allows provides names for non-existent objects, like the quotient of a number by zero, the value of a function at a point not in its domain, the limit of a sequence which doesn’t converge, etc. Mathematicians go ahead and apply first order logic to mathematics anyway, and in fact I’ll do so in the next chapter with elementary arithmetic. That particular application will be harmless because the particular language I’ll use for arithmetic won’t allow references to non-existent objects. It will have, for example, a symbol for multiplication but none for division. It’s hard to do that in any setting more complicated than elementary arithmetic though so there is a real mismatch between modern mathematical language and the first order logic which supposedly forms the basis of mathematical reasoning.
The two rules of inference above are still relatively unproblematic compared to the other two quantifier rules though. The rules in question are variants of the rule of fantasy, but one of them doesn’t introduce any hypothesis! Roughly we would like to say, for example, that if we enter a new scope and manage to derive the statement \({ ( P A ) }\) within it then we can leave that scope and have the statement \({ [ ∀ V . ( P V ) ] }\) in the outer scope. The idea underlying this is that if we can prove \({ P a }\) without making any assumptions on \({ a }\) then \({ P }\) should be true universally. The problem with this is similar to the one we encountered in zeroeth order logic with the rule of substitution and the solution is somewhat similar. We have to restrict our use inside the scope of variables from outside the scope. In this case we need to avoid using statements in which the parameter \({ a }\) appears. Otherwise we’ve not kept to the “without making any assumptions on \({ a }\)” part of the justification for the rule. Or we could allow the use of such statements, but with the requirement that all occurrences of \({ a }\) be replaced by some new parameter.
There is a similar rule of inference corresponding to our remaining tableau rule. If we have a statement in scope of the form \({ [ ∃ V . ( P V ) ] }\) then this rule allows us to introduce a hypothesis \({ ( P A ) }\). When we discharge this hypothesis we can conclude \({ [ ( P A ) ⊃ Q ] }\), provided two restrictions are met. The first is the same as in the previous rule: the variable represented by \({ V }\) should not occur in any of the statements we use from any wider scope. The second restriction is that it should also not occur in \({ Q }\).