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).
0

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?

flag
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

closed as no longer relevant by Andreas Blass, Mariano Suárez-Alvarez, Todd Trimble, François G. Dorais♦ Jun 7 2011 at 20:29

Browse other questions tagged or ask your own question.