Predicado funcional

En lógica formal y ramas relacionadas de las matemáticas, un predicado funcional, o símbolo de función, es un símbolo lógico que se puede aplicar a un término objeto para producir otro objeto término. Los predicados funcionales también se denominan a veces asignaciones, pero ese término tiene significados adicionales en matemáticas. En un modelo, un símbolo de función será modelado por una función.

Específicamente, el símbolo F en un lenguaje formal es un símbolo funcional si, dado cualquier símbolo X que represente un objeto en el lenguaje, F(X) es nuevamente un símbolo que representa un objeto en ese idioma. En lógica escrita, F es un símbolo funcional con dominio tipo T y codominio tipo U si, dado cualquier símbolo X que representa un objeto de tipo T, F(X) es un símbolo representando un objeto de tipo U. De manera similar, se pueden definir símbolos de función de más de una variable, de forma análoga a funciones de más de una variable; un símbolo de función en cero variables es simplemente un símbolo constante.

Ahora considere un modelo del lenguaje formal, con los tipos T y U modelados por conjuntos [T] y [ U] y cada símbolo X de tipo T modelado por un elemento [X] en [T]. Entonces F puede ser modelado por el conjunto

[F]:={}()[X],[F()X)]):[X]▪ ▪ [T]},{displaystyle [F]:={big{}([X],[F(X)]:[X]in [mathbf {T}{big}}}}

que es simplemente una función con dominio [T] y codominio [U]. Es un requisito de un modelo consistente que [F(X)] = [F(Y)] siempre que [X] = [Y].

Introducción de nuevos símbolos de funciones

En un tratamiento de la lógica de predicados que permite introducir nuevos símbolos de predicados, uno también querrá poder introducir nuevos símbolos de funciones. Dados los símbolos de función F y G, se puede introducir un nuevo símbolo de función F ∘ G, el composición de F y G, que satisface (F ∘ G)(X ) = F(G(X)), para todos los X. Por supuesto, el lado derecho de esta ecuación no tiene sentido en la lógica tipada a menos que el tipo de dominio de F coincida con el tipo de codominio de G, por lo que esto es obligatorio para que se defina la composición.

Uno también obtiene ciertos símbolos de función automáticamente. En la lógica sin tipo, existe un id de predicado de identidad que satisface id(X) = X para todos los X. En lógica tipada, dado cualquier tipo T, hay un predicado de identidad id_T con dominio y codominio tipo T; satisface id_T(X) = X para todos los X de tipo T. De manera similar, si T es un subtipo de U, entonces hay un predicado de inclusión de tipo de dominio T y tipo de codominio U que satisface la misma ecuación; hay símbolos de función adicionales asociados con otras formas de construir nuevos tipos a partir de los antiguos.

Además, uno puede definir predicados funcionales después de probar un teorema apropiado. (Si está trabajando en un sistema formal que no le permite introducir nuevos símbolos después de probar los teoremas, tendrá que usar símbolos de relación para sortear esto, como en la siguiente sección). Específicamente, si puede probar que para cada X (o cada X de cierto tipo), existe un único Y que satisface alguna condición P, entonces puede introducir un símbolo de función F para indicar esto. Tenga en cuenta que P será en sí mismo un predicado relacional que involucra tanto a X como a Y. Entonces, si existe tal predicado P y un teorema:

Para todos X tipo T, para algunos únicos Y tipo U, P()X,Y),

entonces puedes introducir un símbolo de función F de tipo de dominio T y tipo de codominio U que satisfaga:

Para todos X tipo T, para todos Y tipo U, P()X,YSi y sólo si Y = F()X).

Prescindir de predicados funcionales

Muchos tratamientos de lógica de predicados no permiten predicados funcionales, solo predicados relacionales. Esto es útil, por ejemplo, en el contexto de probar teoremas metalógicos (como los teoremas de incompletud de Gödel), donde no se quiere permitir la introducción de nuevos símbolos funcionales (ni ningún otro símbolo nuevo, por ejemplo). ese asunto). Pero existe un método para reemplazar los símbolos funcionales con símbolos relacionales dondequiera que aparezcan los primeros; además, esto es algorítmico y, por lo tanto, adecuado para aplicar la mayoría de los teoremas metalógicos al resultado.

Específicamente, si F tiene el tipo de dominio T y el tipo de codominio U, entonces se puede reemplazar con un predicado P de tipo (T,U). Intuitivamente, P(X,Y) significa F(X) = Y. Luego, siempre que aparezca F(X) en una declaración, puede reemplazarlo con un nuevo símbolo Y de tipo U e incluya otra instrucción P(X,Y). Para poder hacer las mismas deducciones, necesita una proposición adicional:

Para todos X tipo T, para algunos únicos Y tipo U, P()X,Y).

(Por supuesto, esta es la misma proposición que tuvo que probarse como teorema antes de introducir un nuevo símbolo de función en la sección anterior).

Debido a que la eliminación de predicados funcionales es conveniente para algunos propósitos y posible, muchos tratamientos de la lógica formal no se ocupan explícitamente de los símbolos de función, sino que usan solo símbolos de relación; otra forma de pensar en esto es que un predicado funcional es un tipo especial de predicado, específicamente uno que satisface la proposición anterior. Esto puede parecer un problema si desea especificar un esquema de proposición que se aplique solo a los predicados funcionales F; ¿Cómo sabe de antemano si cumple esa condición? Para obtener una formulación equivalente del esquema, primero reemplace cualquier cosa de la forma F(X) con una nueva variable Y. Luego cuantifique universalmente sobre cada Y inmediatamente después de que se introduzca el X correspondiente (es decir, después de que se cuantifique X sobre, o al comienzo de la si X está libre), y guarde la cuantificación con P(X,Y). Finalmente, haga que la declaración completa sea una consecuencia material de la condición de unicidad para un predicado funcional anterior.

Tomemos como ejemplo el esquema axiomático de reemplazo en la teoría de conjuntos de Zermelo-Fraenkel. (Este ejemplo utiliza símbolos matemáticos). Este esquema establece (en una forma), para cualquier predicado funcional F en una variable:

О О A,∃ ∃ B,О О C,C▪ ▪ A→ → F()C)▪ ▪ B.{displaystyle forall A,exists B,forall C,Cin Arightarrow F(C)in B.}

Primero, debemos reemplazar F(C) con alguna otra variable D:

О О A,∃ ∃ B,О О C,C▪ ▪ A→ → D▪ ▪ B.{displaystyle forall A,exists B,forall C,Cin Arightarrow Din B.}

Por supuesto, esta declaración no es correcta; D debe cuantificarse justo después de C:

О О A,∃ ∃ B,О О C,О О D,C▪ ▪ A→ → D▪ ▪ B.{displaystyle forall A,exists B,forall C,forall D,Cin Arightarrow Din B.}

Aún debemos presentarnos. P para guardar esta cuantificación:

О О A,∃ ∃ B,О О C,О О D,P()C,D)→ → ()C▪ ▪ A→ → D▪ ▪ B).{displaystyle forall A,exists B,forall C,forall D,P(C,D)rightarrow (Cin Arightarrow Din B).}

Esto es casi correcto, pero se aplica a demasiados predicados; lo que realmente queremos es:

()О О X,∃ ∃ !Y,P()X,Y))→ → ()О О A,∃ ∃ B,О О C,О О D,P()C,D)→ → ()C▪ ▪ A→ → D▪ ▪ B)).{displaystyle (forall X,exists !Y,P(X,Y))rightarrow (forall A,exists B,forall C,forall D,P(C,D)rightarrow (Cin Arightarrow Din B)). }

Esta versión del esquema axiom de reemplazo es ahora adecuada para su uso en un lenguaje formal que no permite la introducción de nuevos símbolos de función. Alternativamente, se puede interpretar la declaración original como una declaración en un lenguaje formal; fue simplemente una abreviatura para la declaración producida al final.