5.8: Sustitución
- Page ID
- 103712
Definición\(\PageIndex{1}\): Substitution in a term
Definimos\(\Subst{s}{t}{x}\), el resultado de sustituir\(t\) por cada ocurrencia de\(x\) in\(s\), recursivamente:
-
\(\indcase{s}{c}\)\(\Subst{s}{t}{x}\)es justo\(s\).
-
\(\indcase{s}{y}\)\(\Subst{s}{t}{x}\)también es justo\(s\), siempre\(y\) que sea una variable y\(y \not\ident x\).
-
\(\indcase{s}{x}\)\(\Subst{s}{t}{x}\)es\(t\).
-
\(\indcase{s}{\Atom{f}{t_1, \dots, t_n}}\)\(\Subst{s}{t}{x}\)es\(\Atom{f}{\Subst{t_1}{t}{x}, \dots, \Subst{t_n}{t}{x}}\).
Definición\(\PageIndex{2}\)
Un término\(t\) es libre para\(x\) in\(A\) si ninguna de las ocurrencias libres de\(x\) in\(A\) ocurre en el alcance de un cuantificador que une una variable in\(t\).
Ejemplo\(\PageIndex{1}\)
-
\(\Obj v_8\)es gratis para\(\Obj v_1\) en\(\lexists{\Obj v_3}{}\Atom{\Obj A^2_4}{\Obj v_3,\Obj v_1}\)
-
\(\Obj f^2_1(\Obj v_1, \Obj v_2)\)no es gratis para\(\Obj v_0\) en\(\lforall{\Obj v_2}{}\Atom{\Obj A^2_4}{\Obj v_0,\Obj v_2}\)
Definición\(\PageIndex{3}\): Substitution in a formula
Si\(A\) es una fórmula,\(x\) es una variable, y\(t\) es un término libre para\(x\) in\(A\), entonces\(\Subst{A}{t}{x}\) es el resultado de sustituir\(t\) por todas las ocurrencias libres de \(x\)en\(A\).
-
\(\indcase{A}{\lfalse}\)\(\Subst{\indfrm}{t}{x}\)es\(\lfalse\).
-
\(\indcase{A}{\Atom{P}{t_1,\dots, t_n}}\)\(\Subst{\indfrm}{t}{x}\)es\(\Atom{P}{\Subst{t_1}{t}{x}, \dots, \Subst{t_n}{t}{x}}\).
-
\(\indcase{A}{\eq[t_1][t_2]}\)\(\Subst{\indfrmp}{t}{x}\)es\(\Subst{t_1}{t}{x} = \Subst{t_2}{t}{x}\).
-
\(\indcase{A}{\lnot B}\)\(\Subst{\indfrmp}{t}{x}\)es\(\lnot \Subst{B}{t}{x}\).
-
\(\indcase{A}{(B \land C)}\)\(\Subst{\indfrmp}{t}{x}\)es\((\Subst{B}{t}{x} \land \Subst{C}{t}{x})\).
-
\(\indcase{A}{(B \lor C)}\)\(\Subst{\indfrmp}{t}{x}\)es\((\Subst{B}{t}{x} \lor \Subst{C}{t}{x})\).
-
\(\indcase{A}{(B \lif C)}\)\(\Subst{\indfrmp}{t}{x}\)es\((\Subst{B}{t}{x} \lif \Subst{C}{t}{x})\).
-
\(\indcase{A}{\lforall{y}{B}}\)\(\Subst{\indfrmp}{t}{x}\)es\(\lforall{y}{\Subst{B}{t}{x}}\), siempre que\(y\) sea una variable distinta a\(x\); de lo contrario\(\Subst{\indfrmp}{t}{x}\) es justo\(\indfrm\).
-
\(\indcase{A}{\lexists{y}{B}}\)\(\Subst{\indfrmp}{t}{x}\)es\(\lexists{y}{\Subst{B}{t}{x}}\), siempre que\(y\) sea una variable distinta a\(x\); de lo contrario\(\Subst{\indfrmp}{t}{x}\) es justo\(\indfrm\).
Tenga en cuenta que la sustitución puede ser vacuosa: Si\(x\) no ocurre en\(A\) absoluto, entonces\(\Subst{A}{t}{x}\) es justo\(A\).
La restricción que\(t\) debe ser gratuita para\(x\) in\(A\) es necesaria para excluir casos como los siguientes. Si\(A \ident \lexists{y}{x < y}\) y\(t \ident y\), entonces\(\Subst{A}{t}{x}\) lo sería\(\lexists{y}{y < y}\). En este caso la variable libre\(y\) es “capturada” por el cuantificador en el\(\lexists{y}{}\) momento de la sustitución, y eso es indeseable. Por ejemplo, nos gustaría que fuera el caso que cada vez que se\(\lforall{x}{B}\) sostiene, también lo hace\(\Subst{B}{t}{x}\). Pero considere\(\lforall{x}{\lexists{y}{x < y}}\) (aquí\(B\) está\(\lexists{y}{x < y}\)). Es la oración la que es cierta sobre, por ejemplo, los números naturales: por cada número\(x\) hay un número\(y\) mayor que éste. Si permitiéramos\(y\) como posible sustitución de\(x\), terminaríamos con\(\Subst{B}{y}{x} \ident \lexists{y}{y < y}\), lo cual es falso. Esto lo evitamos al exigir que ninguna de las variables libres en\(t\) terminara siendo ligada por un cuantificador in\(A\).
A menudo usamos la siguiente convención para evitar la notación cumbersume: Si\(A\) es una fórmula con una variable libre\(x\), escribimos\(A(x)\) para indicar esto. Cuando está claro cuál\(A\) y\(x\) tenemos en mente, y\(t\) es un término (se supone que es libre para\(x\) adentro\(A(x)\)), entonces escribimos\(A(t)\) como abreviatura de\(\Subst{A(x)}{t}{x}\).