Una regla de inferencia que permite derivar una instancia de una fórmula a partir de una afirmación cuantificada universalmente: de ∀x P(x) se puede inferir P(t) para cualquier término t apropiado para sustituir a x.

Principio

Una afirmación cuantificada universalmente sobre todos los elementos de un dominio autoriza la sustitución de un término arbitrario pero adecuado por la variable ligada, produciendo una instancia concreta y preservando la verdad si la sustitución evita la captura de variables.

Demostración

Dado el axioma ∀n ∈ N, n + 0 = n, podemos instanciar para obtener 5 + 0 = 5 sustituyendo el numeral 5 por la variable ligada n.

Aplicación incorrecta

Instanciar con un término que no pertenece al dominio, o sustituir un término que introduce captura de variable (por ejemplo reemplazar una variable ligada por una expresión que contiene una variable cuantificada) invalida la inferencia.

Consecuencia

Permite derivar consecuencias concretas a partir de leyes generales, facilitando el paso de premisas generales a conclusiones particulares en demostraciones y cálculos.

Inversión

La inversión es la generalización universal, que intenta inferir ∀x P(x) a partir de instancias; a diferencia de la instanciación, la generalización exige cuidado para asegurar que la instancia era arbitraria y no se hicieron suposiciones adicionales.

Límite

Se aplica en lógicas de primer orden y lógicas afines donde dominios y sustituciones están bien definidos; no autoriza instanciaciones entre diferentes tipos ni en contextos que cambien la estructura de enlace, y requiere que el término sustitutorio sea libre para la variable.

Tensión semántica

Hay tensión con las reglas existenciales: la instanciación universal produce instancias particulares pero no genera afirmaciones de existencia; confundir instanciación con introducción existencial es un error semántico común.

Síntesis

Instanciación Universal: una regla básica y segura en lógicas de predicados estándar que produce instancias específicas a partir de enunciados universales, siempre que las sustituciones respeten dominio, tipos y la ausencia de captura de variables.