1
$\begingroup$

As far as I know, there are only 2 restrictions for the universal introduction rule of inference which are the following:

P[a/x] can become forall x.P if:
1. x is not mentioned in P
2. a is not mentioned in a premise

But these don't prevent the problem mentioned here:
Does existential elimination affect whether you can do a universal introduction?

So is the list of restrictions incomplete or is there something I'm missing here?

  • 0
    Never mind, I realized that I'm mixing different versions of the rules of inference. The need for extra restrictions only arises when using the rules of inference in the linked post and not the ones I mentioned here.2011-06-07

1 Answers 1