¿Qué enuncia?
Cuando una fórmula está cuantificada existencialmente, la variable cuantificada puede ser sustituida por una constante nueva y el cuantificador se puede eliminar:
Para que la aplicación de la regla sea correcta, es necesario garantizar que la constante utilizada es nueva, es decir, que no haya aparecido nunca antes.
Puede entenderse de la forma siguiente: si se sabe que hay un elemento del dominio que cumple una determinada propiedad (A), nos podemos referir al mismo con una constante (a), siempre y cuando la misma constante no se utilice también para referirse a cualquier otro elemento del dominio.