Instanciação existencial

Na lógica de predicados, instanciação existencial (também chamada como eliminação existencial)^[1][2][3] é uma regra de inferência válida, onde dada um fórmula da forma ${\displaystyle (\exists x)\phi (x)}$,  pode-se inferir ${\displaystyle \phi (c)}$ como um novo símbolo de constante ou variável denotada por c. A regra tem a restrição de que a constante ou variável c que forem introduzidas pela regra, devem ser um novo termo que não ocorreu no início da prova.

A regra denotada em notação formal:

${\displaystyle (\exists x){\mathcal {F}}x::{\mathcal {F}}a,}$

onde 'a' é um termo arbitrário que não tem sido parte da prova até agora.

• Falácia existencial

Referências