MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

## Syntactically speaking, when can you introduce a universal such that no logical inconsistencies are introduced? [closed]

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:
http://math.stackexchange.com/questions/43936/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?

-
 I suspect you're mixing together rules (and restrictions) from more than one source. The restrictions you need for universal introduction depend on how the other rules and/or axioms are formulated. In any case, this is not a research-level question, so I'm voting to close. – Andreas Blass Jun 7 2011 at 19:32 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. – unknown (google) Jun 7 2011 at 21:37