Question on Universal/Existential Generalization/Instantiation in Proof Sequences

Question

I have a simple question. Are there any restrictions when using Universal/Existential Generalization/Instantiation in Proof Sequences? My specific question is, if I apply universal instantiation during a proof sequence step, later down the line, is it possible for me to apply the existential generalization? And also the opposite. If I apply existential instantiation at one point, is it illegal to then later convert that piece with universal generalization? Logically to me, it seems like these sort of moves would be illogical and breaking some sort of "law" in this subject, but I don't know. I would assume that if I applied a universal instantiation to one item, I would have to apply universal generalization to it later down the road, and the same for existential. Any help in cleaning this up would be greatly appreciated.

Answer 1

Different systems define these rules a bit differently in terms of notation. For example, some systems simply drop quantifiers for the elimination rules, leaving what seems to be free variables in the formula, while others replace those variables with constant symbols. Either way, however, restrictions do indeed need to be in place that prevent you from making invalid inferences, as you already suspected.

Here is an example. Say you have $\forall x P(x)$. Then obviously I can infer $P(a)$ for any constant symbol $a$. No restirctions there, really, although notice that we do make an assumption there that the domain of discourse is not empty (otherwise the $a$ could not refer to anything). Almost all logic systems make that assumption though, which is also why you can infer $\exists x P(x)$ from $\forall x P(x)$: once you have $P(a)$, you can infer $\exists x P(x)$ from that. Again, no restrictions there. So, basically, Universal Elimination and Existential Introduction have no restrictions.

On the other hand, Universal Introduction and Existential Elimination do have restrictions. For Universal Introduction, we usually do something that is the equivalent of 'Let $d$ be some arbitrary object of our domain ... [inferencing] ... and therefore $d$ has property $P$. Therefore, all objects have property $P$'. So, for example, some systems will use a constant symbol $a$ that will be used to denote that arbitrary object $d$, and if you can show that $P(a)$, you can conclude $\forall x P(x)$. This, however, is only going to work if $a$ is not already used to denote some specific object, because if that specific object would have property $P$, then with this method we would be concluding that all objects have property $P$ on the basis of this one object having property $P$, which is clearly not right. So, typically formalizations of the rule will say that $a$ needs to be a 'fresh' or 'new' constant: a constant that is not used elsewhere for a different purpose.

For Existential Elimination something similar happens. The conceptual thinking here is: 'I know there is something with property $P$. I don't know what specific object it is, but let me call that object $d$, so $d$ has property $P$ ... [further inferencing can take place]'. To formalize this, some systems will once again use a constant symbol $a$ to denote the object $d$, and so will infer $P(a)$ from $\exists x P(x)$. But again, care must be taken that this $a$ is a new constant, so it can take the role of 'that object that has property P, even if I don't know what exactly that object is'. Again, if we were already using $a$ for something else in the proof, then we can't say $P(a)$, because that object may not have property $P$ at all. In other words, once again you have to introduce a new constant.