En la lógica de predicados , la instanciación existencial (también llamada eliminación existencial ) [1] [2] [3] es una regla de inferencia que dice que, dada una fórmula de la forma, uno puede inferir para un nuevo símbolo constante c . La regla tiene las restricciones de que la constante c introducida por la regla debe ser un término nuevo que no haya ocurrido antes en la prueba, y tampoco debe ocurrir en la conclusión de la prueba. También es necesario que cada instancia de que está obligado a debe ser reemplazado uniformemente por c . Esto está implícito en la notación, pero su declaración explícita a menudo se deja fuera de las explicaciones.
En una notación formal, la regla se puede denotar por
donde a es un nuevo símbolo constante que no ha aparecido en la prueba.