First-order logic theory that doesn't need the generalization rule of inference

144 Views Asked by At

I'm trying to understand the generalization rule of inference better. Suppose we have a language $L$ consisting of some predicate symbols with the sizes corresponding to them. Now, we construct some theory $T$ in the following way. If $f$ is a valid closed formula over $L$ (i.e. $f$ is true for all interpretations of $L$), then $f\in T$. $T$ may also include some other closed formulas over $L$ (by closed I mean of course not containing free variables). Now, the system of inference rules usually includes the modus ponens (MP) and the generalization rule (GEN). Can we state that we don't need GEN for $T$, i.e. every theorem of $T$ that can be proved with MP+GEN can be also proved only with MP?