Generalización universal

En lógica predicada, generalización (también universalización, introducción universal, GEN, UG) es una regla de inferencia válida. Dice que si ${displaystyle vdash !P(x)}$ ha sido derivado, entonces ${displaystyle vdash !forall x,P(x)}$ puede ser derivado.

Generalización con hipótesis

La regla de generalización completa permite hipótesis a la izquierda del torntil, pero con restricciones. Assume ${displaystyle "Gamma"$ es un conjunto de fórmulas, ${displaystyle varphi }$ una fórmula, y ${displaystyle Gamma vdash varphi (y)}$ ha sido derivado. La norma de generalización establece que ${displaystyle Gamma vdash forall x,varphi (x)}$ puede derivarse si ${displaystyle y}$ no se menciona en ${displaystyle "Gamma"$ y ${displaystyle x}$ no ocurre en ${displaystyle varphi }$.

Estas restricciones son necesarias para la solidez. Sin la primera restricción, uno podría concluir ${displaystyle forall xP(x)}$ de la hipótesis ${displaystyle P(y)}$. Sin la segunda restricción, se podría hacer la siguiente deducción:

1. ${displaystyle exists z,exists w,(znot =w)}$ (Hypothesis)
2. ${displaystyle exists w,(ynot =w)}$ (Existential instantiation)
3. ${displaystyle ynot =x}$ (Existential instantiation)
4. ${displaystyle forall x,(xnot =x)}$ (Faulty universalization)

Esto pretende mostrar que ${displaystyle exists z,exists w,(znot =w)vdash forall x,(xnot =x),}$ que es una deducción insondable. Note que ${displaystyle Gamma vdash forall y,varphi (y)}$ es admisible si ${displaystyle y}$ no se menciona en ${displaystyle "Gamma"$ (la segunda restricción no debe aplicarse, como la estructura semántica ${displaystyle varphi (y)}$ no está siendo cambiado por la sustitución de ninguna variable).

Ejemplo de prueba

Probar: ${displaystyle forall x,(P(x)rightarrow Q(x))rightarrow (forall x,P(x)rightarrow forall x,Q(x)}$ es derivable de ${displaystyle forall x,(P(x)rightarrow Q(x)}$ y ${displaystyle forall x,P(x)}$.

Prueba:

Paso	Formula	Justificación
1	${displaystyle forall x,(P(x)rightarrow Q(x)}$	Hipótesis
2	${displaystyle forall x,P(x)}$	Hipótesis
3	${displaystyle (forall x,(P(x)rightarrow Q(x)))rightarrow (P(y)rightarrow Q(y)}$	Instantiación universal
4	${displaystyle P(y)rightarrow Q(y)}$	De (1) y (3) por Modus ponens
5	${displaystyle (forall x,P(x))rightarrow P(y)}$	Instantiación universal
6	${displaystyle P(y)}$	De (2) y (5) por Modus ponens
7	${displaystyle Q(y)}$	De (6) y (4) por Modus ponente
8	${displaystyle forall x,Q(x)}$	De (7) por generalización
9	${displaystyle forall x,(P(x)rightarrow Q(x)),forall x,P(x)vdash forall x,Q(x)}$	Resumen de (1) a (8)
10	${displaystyle forall x,(P(x)rightarrow Q(x))vdash forall x,P(x)rightarrow forall x,Q(x)}$	De (9) por Teorema de Deducción
11	${displaystyle vdash forall x,(P(x)rightarrow Q(x))rightarrow (forall x,P(x)rightarrow forall x,Q(x)}$	De (10) por Teorema de Deducción

En esta prueba, se utilizó la generalización universal en el paso 8. El teorema de deducción fue aplicable en los pasos 10 y 11 porque las fórmulas que se están moviendo no tienen variables libres.