Por ejemplo en Lógica Proposicional la contradicción es evidente porque Estudia (Belén) ^¬ Estudia (Belén).
Pero en Cálculo de Predicados es diferente porque si tengo:
Estudia(x) ^ ¬Estudia (y). No hay contradicción [Belén/ x, Alberto/y] Estudia (Belén) ^¬ Estudia (Belén).
P(a) y P(x) no son comparables, para que lo sean, se debe encontrar una substitución para x que haga ambas fórmulas idénticas. Este proceso de encontrar una sustitución para hacer fórmulas idénticas se conoce como unificación. Lo que se puede sustituir en una fbf para permitir el paramiento de dos fórmulas son las variables por términos.
Variable (Símbolos de constantes, Símbolos de variables, expresiones funcionales)
Sustitución
- La sustitución de variables por términos generales se remite a variables libres. En las ocurrencias ligadas sólo podemos hacer un cambio de variables por variables y no sucede nada
- La sustitución se debe hacer para todas las ocurrencias libres o para ninguna
- Hay que cuidar que una variable libre no se convierta en ligada por la sustitución.
No hay comentarios:
Publicar un comentario