Universal Elimination (UE) allows us to reason from the general to the particular. It states that, whenever we believe a universally quantified sentence, we can infer a version of the target of that sentence in which the universally quantified variable is replaced by an appropriate term.
where τ is substitutable for ν in φ
For example, consider the sentence ∀y.hates(jane,y). From this premise, we can infer that Jane hates Jill, i.e. hates(jane,jill). We also can infer that Jane hates her mother, i.e. hates(jane,mother(jane)). We can even infer than Jane hates herself, i.e. hates(jane,jane).
In addition, we can use Universal Elimination to create conclusions with free variables. For example, from ∀x.hates(jane,x), we can infer hates(jane,x) or, equivalently, hates(jane,y).
In using Universal Elimination, we have to be careful to avoid conflicts with other variables and quantifiers in the quantified sentence. This is the reason for the constraint on the replacement term. As an example of what can go wrong without this constraint, consider the sentence ∀x.∃y.hates(x,y), i.e. everybody hates somebody. From this sentence, it makes sense to infer ∃y.hates(jane,y), i.e. Jane hates somebody. However, we do not want to infer ∃y.hates(y,y); i.e., there is someone who hates herself.
We can avoid this problem by obeying the restriction on the Universal Elimination rule. We say that a term τ is free for a variable ν in a sentence φ if and only if no free occurrence of ν occurs within the scope of a quantifier of some variable in τ. For example, the term x is free for y in ∃z.hates(y,z). However, the term z is not free for y, since y is being replaced by z and y occurs within the scope of a quantifier of z. Thus, we cannot substitute z for y in this sentence, and we avoid the problem we have just described.
Universal Introduction (UI) allows us to reason from arbitrary sentences to universally quantified versions of those sentences.
where ν does not occur free in both φ and an active assumption
Typically, UI is used on sentences with free variables to make their quantification explicit. For example, if we have the sentence hates(jane,y), then, we can infer ∀y.hates(jane,y).
Note that we can also apply the rule to sentences that do not contain the variable that is quantified in the conclusion. For example, from the sentence hates(jane,jill), we can infer ∀x.hates(jane,jill). And, from the sentence hates(jane,y), we can infer ∀x.hates(jane,y). These are not particularly sensible conclusions. However, the results are correct, and the deduction of such results is necessary to ensure that our proof system is complete.
There is one important restriction on the use of Universal Introduction. If the variable being quantified appears in the sentence being quantified, it must not appear free in any active assumption, i.e. an assumption in the current subproof or any superproof of that subproof. For example, if there is a subproof with assumption p(x) and from that we have managed to derive q(x), then we cannot just write ∀x.q(x).
If we want to quantify a sentence in this situation, we must first use Implication Introduction to discharge the assumption and then we can apply Universal Introduction. For example, in the case just described, we can first apply Implication Introduction to derive the result (p(x) ⇒ q(x)) in the parent of the subproof containing our assumption, and we can then apply Universal Introduction to derive ∀x.(p(x) ⇒ q(x)).