Símbolo de función

En los sistemas formales, particularmente en la lógica matemática , un símbolo de función es un símbolo no lógico que representa una función o mapeo en el dominio del discurso , aunque, formalmente, no necesita representar nada en absoluto. Los símbolos de función son un componente básico en los lenguajes formales para formar términos . Específicamente, si el símbolo${\displaystyle F}$es un símbolo de función, entonces dado cualquier símbolo constante${\displaystyle X}$representar un objeto en el lenguaje,${\displaystyle F(X)}$también representa un objeto en el lenguaje. De manera similar, si${\displaystyle T}$es algún término en el idioma,${\displaystyle F(T)}$También es un término. Por lo tanto, la interpretación de un símbolo de función debe definirse en todo el ámbito del discurso. Los símbolos de función son una noción primitiva y, por consiguiente, no se definen en términos de otros conceptos más básicos.

En lógica tipada , F es un símbolo funcional con dominio T y 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, análogas a las funciones de más de una variable; un símbolo de función sin variables es simplemente un símbolo constante.

Ahora consideremos 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

${\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 ].

En un tratamiento de la lógica de predicados que permite introducir nuevos símbolos de predicado, también se querrá 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 satisface ( 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 tipada 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 la composición esté definida.

También se obtienen automáticamente ciertos símbolos de función. En lógica sin tipos, existe un predicado de identidad id que satisface id( X ) = X para todo X. En lógica con tipos, dado cualquier tipo T , existe un predicado de identidad id _T con dominio y codominio de tipo T ; satisface id _T ( X ) = X para todo X de tipo T. De manera similar, si T es un subtipo de U , entonces existe un predicado de inclusión de dominio de tipo T y codominio de tipo U que satisface la misma ecuación; existen 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 demostrar un teorema apropiado . (Si trabaja en un sistema formal que no permite introducir nuevos símbolos después de demostrar teoremas, deberá usar símbolos de relación para sortear esta limitación, como se explica en la siguiente sección). Específicamente, si puede demostrar que para cada X (o cada X de un tipo determinado), existe un Y único que satisface alguna condición P , entonces puede introducir un símbolo de función F para indicarlo. Esto se denomina extensión por definición . Nótese que P será en sí mismo un predicado relacional que involucra tanto a X como a Y. Por lo tanto, si existe tal predicado P y un teorema:

Para todo X de tipo T , para algún Y único de 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 todo X de tipo T , para todo Y de tipo U , P ( X , Y ) si y solo si Y = F ( X ).

Muchos tratamientos de la lógica de predicados no admiten predicados funcionales, solo relacionales . Esto resulta ú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 introducir nuevos símbolos funcionales (ni ningún otro símbolo nuevo). Sin embargo, existe un método para reemplazar los símbolos funcionales por símbolos relacionales dondequiera que aparezcan los primeros; además, este método 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 un dominio de tipo T y un codominio de tipo U , entonces puede reemplazarse con un predicado P de tipo ( T , U ). Intuitivamente, P ( X , Y ) significa F ( X ) = Y. Entonces, siempre que F ( X ) aparezca en una proposición, puede reemplazarse con un nuevo símbolo Y de tipo U e incluir otra proposición P ( X , Y ). Para poder hacer las mismas deducciones, se necesita una proposición adicional:

Para todo X de tipo T , para algún Y único de tipo U , P ( X , Y ).

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

Dado que la eliminación de predicados funcionales es conveniente para algunos propósitos y posible, muchos tratamientos de lógica formal no abordan explícitamente los símbolos de función, sino que utilizan únicamente símbolos de relación; otra forma de pensarlo 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 se desea especificar un esquema de proposición que se aplique solo a predicados funcionales F ; ¿cómo saber de antemano si satisface esa condición? Para obtener una formulación equivalente del esquema, primero reemplace cualquier expresión 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 haya cuantificado, o al comienzo de la proposición si X es libre), y proteja la cuantificación con P ( X , Y ). Finalmente, haga que toda la proposición 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:

${\displaystyle \forall A,\exists B,\forall C,C\in A\rightarrow F(C)\in B.}$

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

${\displaystyle \forall A,\exists B,\forall C,C\in A\rightarrow D\in B.}$

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

${\displaystyle \forall A,\exists B,\forall C,\forall D,C\in A\rightarrow D\in B.}$

Aún debemos introducir P para proteger esta cuantificación:

${\displaystyle \forall A,\exists B,\forall C,\forall D,P(C,D)\rightarrow (C\in A\rightarrow D\in B).}$

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

${\displaystyle (\forall X,\exists !Y,P(X,Y))\rightarrow (\forall A,\exists B,\forall C,\forall D,P(C,D)\rightarrow (C\in A\rightarrow D\in B)).}$

Esta versión del esquema axiomático de reemplazo ahora es 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 afirmación original como una afirmación en dicho lenguaje formal; simplemente era una abreviatura de la afirmación resultante.

Una función no interpretada ^{[ 1 ]} es aquella que no tiene otra propiedad que su nombre y su forma n-aria . La teoría de funciones no interpretadas también se denomina a veces teoría libre, porque se genera libremente y, por lo tanto, es un objeto libre , o teoría vacía, al ser la teoría que tiene un conjunto vacío de sentencias (en analogía con un álgebra inicial ). Las teorías con un conjunto no vacío de ecuaciones se conocen como teorías ecuacionales . El problema de satisfacibilidad para teorías libres se resuelve mediante la unificación sintáctica ; los algoritmos para esta última son utilizados por intérpretes de varios lenguajes de programación, como Prolog . La unificación sintáctica también se utiliza en algoritmos para el problema de satisfacibilidad de ciertas otras teorías ecuacionales, véase Unificación (ciencia de la computación) .

(declarar-fun f (Int) Int) (afirmar (= (f 10) 1)) 

(declarar-fun f (Int) Int) (afirmar (= (f 10) 1)) (afirmar (= (f 10) 42)) 

• Tipo de datos algebraicos
• Álgebra inicial
• Conector lógico
• Constante lógica
• Álgebra de términos
• Teoría de la igualdad pura