Instanciación existencial

En 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 , se 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á vinculada a debe ser reemplazada uniformemente por c . Esto está implícito en la notación , pero su declaración explícita a menudo se omite en las explicaciones. ${\displaystyle (\exists x)\phi (x)}$${\displaystyle \phi (c)}$${\displaystyle x}$${\displaystyle \exists x}$${\displaystyle P\left({a}\right)}$

En una notación formal, la regla puede denotarse por

${\displaystyle \exists xP\left({x}\right)\implies P\left({a}\right)}$

donde a es un nuevo símbolo constante que no ha aparecido en la prueba.

• Falacia existencial
• Instanciación universal
• Lista de reglas de inferencia