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 de objeto para producir otro término de objeto. 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 .
En concreto, 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 de nuevo un símbolo que representa un objeto en ese lenguaje. En lógica tipificada , F es un símbolo funcional con tipo de dominio T y tipo de codominio U si, dado cualquier símbolo X que represente un objeto de tipo T , F ( X ) es un símbolo que representa un objeto de tipo U . De forma 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 .
Consideremos ahora un modelo del lenguaje formal, con los tipos T y U modelados por los conjuntos [ T ] y [ U ] y cada símbolo X del tipo T modelado por un elemento [ X ] en [ T ]. Entonces F puede ser modelado por el conjunto
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 ].
En un tratamiento de la lógica de predicados que permita introducir nuevos símbolos de predicado, también será necesario poder introducir nuevos símbolos de función. Dados los símbolos de función F y G , se puede introducir un nuevo símbolo de función F ∘ G , la composición de F y G , que satisfaga ( F ∘ G )( X ) = F ( G ( X )), para todo X . Por supuesto, el lado derecho de esta ecuación no tiene sentido en la lógica tipificada a menos que el tipo de dominio de F coincida con el tipo de codominio de G , por lo que esto es necesario para que se defina la composición.
También se obtienen ciertos símbolos de función automáticamente. En la lógica no tipificada, hay un predicado de identidad id que satisface id( X ) = X para todos los X . En la lógica tipificada, dado cualquier tipo T , hay un predicado de identidad id T con dominio y codominio de 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, se pueden definir predicados funcionales después de probar un teorema apropiado . (Si estás trabajando en un sistema formal que no te permite introducir nuevos símbolos después de probar teoremas, entonces tendrás que usar símbolos de relación para evitar esto, como en la siguiente sección). Específicamente, si puedes probar que para cada X (o cada X de un cierto tipo), existe una única Y que satisface alguna condición P , entonces puedes introducir un símbolo de función F para indicar esto. Ten en cuenta que P será en sí mismo un predicado relacional que involucra tanto a X como a Y . Entonces, si existe un predicado P y un teorema:
Luego puedes introducir un símbolo de función F de tipo de dominio T y tipo de codominio U que satisfaga:
Muchos tratamientos de la lógica de predicados no permiten predicados funcionales, sino solo predicados relacionales . Esto es útil, por ejemplo, en el contexto de la demostración de teoremas metalógicos (como los teoremas de incompletitud de Gödel ), donde no se desea permitir la introducción de nuevos símbolos funcionales (ni ningún otro símbolo nuevo, en realidad). Pero existe un método para reemplazar 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.
En concreto, si F tiene dominio de tipo T y codominio de tipo U , entonces puede reemplazarse por un predicado P de tipo ( T , U ). Intuitivamente, P ( X , Y ) significa F ( X ) = Y. Entonces, siempre que F ( X ) aparezca en un enunciado, puede reemplazarlo por un nuevo símbolo Y de tipo U e incluir otro enunciado P ( X , Y ). Para poder hacer las mismas deducciones, necesita una proposición adicional:
(Por supuesto, esta es la misma proposición que tuvo que demostrarse 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 lógica formal no tratan explícitamente con símbolos de función sino que en su lugar 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 predicados funcionales F ; ¿cómo sabe de antemano si satisface 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 la X correspondiente (es decir, después de que X se cuantifique sobre, o al comienzo del enunciado si X es libre), y proteja la cuantificación con P ( X , Y ). Finalmente, haga que todo el enunciado 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:
Primero, debemos reemplazar F ( C ) con alguna otra variable D :
Por supuesto, esta afirmación no es correcta; D debe cuantificarse justo después de C :
Todavía debemos introducir P para proteger esta cuantificación:
Esto es casi correcto, pero se aplica a demasiados predicados; lo que realmente queremos es:
Esta versión del esquema axiomático 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 el enunciado original como un enunciado en un lenguaje formal de ese tipo; era simplemente una abreviatura del enunciado producido al final.
![{\displaystyle [F]:={\big \{}([X],[F(X)]):[X]\in [\mathbf {T} ]{\big \}},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b4330f8ae04afd533c5bf1fbe3fc20c065056d4d)
