Universal Generalization (UG) is also called Universal Introduction (UI). I'll claim that this rule has an analogy in propositional logic. Such rules as
universal elimination (removing or instantiation), and
existential introduction (or generalization) are easy to convert from predicate logic to propositional:
∀xAx → Ay
Ay → ∃xAx
Another story with two other ones rules, which are being used in proof sequences to help to get some important theorems. I guess we can trace similar rule in propositional logic. This time I want to view UG (or UI), and the next time to present EI (or EE) here.
This is, by the way, how the universal generalization looks like:
Ay → ∀xAx, where x isn't free in Ay, and y is arbitrary
First of all, when we do UG we derive or assume an arbitrary variable with a predicate (or in more general cases, a series of arbitrary variables with a predicate), and then generalize it. It is important that such a generalization is available only if a free variable of our given predicate formula is arbitrary.
That arbitrariness, on one hand, is quiet an unusual, and by look we can't differ one free variable formula from another. In other words, if in the sequence of proof there are two formulas Fx and Gx, we can't say about their variables (except for they are unbound) if they are arbitrary.
The most trusted way to check this is to derive or to assume as many same-predicate formulas as possible. For instance, if from a certain wff formula
S in predicate logic (somewhere in a proof sequence) we can entail
Fa, Fb, Fc, etc without any limits of how many variables we get achieve, we may say that
Fx (
Fx=Fa and
Fx=Fb, etc) has an arbitrary variable. The same is about assumption.
In propositional logic there is a theorem that plays the same role. This is the one:
P1→(P2→(P3...(Pn-1→(Pn→(P1&P2&P3&...&Pn)...)
or in a shorer form:
p→(q→(p&q)) (conjunction introduction)
It's easy to check if this formula is correct. We can do this, for instance, this way:
1. A→A tautology
2. (p&q)→(p&q) A/(p&q), 1
3. p→(q→(p&q) exportation, 2But exactly this prove above can demonstrate the same principle or technique we've been using in predicate logic to generalize our free formula with an arbitrary variable. We also derive or assume as many as possible formulas with similar predicate, but different variables and then add to them the universal quantor. Technically it looks like this:
Aa→(Ab→...(Ay→∀xAx)...)
Then compare it to a form that almost repeat the propositional logic one:
Fa→(Fb→(Fc→...(Fn→(Fa&Fb&Fc&...&Fn)...)
No doubt this is the same one. Only we can offer similar analogue to n-variable predicate formula. Then their form'll be like:
Faaa→(Faab→...(Fnnz→...(Fnnn→(Faaa&Faab&...&Fnnn)...)
And a predicate logic parallel theorem will turn into:
Aaaa→(Aaab→...(Annn→∀xyzAxyz)...)
Must note, and I guess this note is really important: if in propositional logic the formula of conjunction introduction doesn't allow us to conclude from all the antecedent propositions to all the consequent propositions, then we cannot use universal generalization in predicate logic.
In simple words, since the conjunction introduction in propositional logic is a theorem, this fact allows us to use universal generalization in predicate logic.