Funciones ordinarias vs. funciones de lenguaje de primer orden

Question

Varios libros introducen funciones como símbolos no lógicos de lenguajes de lógica de primer orden. Luego introducen nuevamente funciones como pares ordenados, donde para cada $x$ hay un par único $\langle x, f(x)\rangle$.

Me pregunto si las dos son nociones diferentes que casualmente tienen el mismo nombre y notación, o si la segunda es una instancia de la primera, es decir, en $\langle x, f(x)\rangle$, $f(x)$ se puede pensar como un caso especial, donde las variables están fijadas (elementos).
Finalmente, ¿cuál es una buena manera de abordar los dos tipos de funciones para evitar ambigüedades?

ACTUALIZACIÓN

Según la solicitud de Rob Arthan, doy dos referencias de libros.

Este es Kunen, K. (2013). Teoría de conjuntos. Elsevier.

Es necesario distinguir entre los símbolos lógicos y los símbolos no lógicos. Los símbolos lógicos son fijos, [...] Los símbolos no lógicos varían con el contexto. Cada aplicación de lógica especificará un conjunto $\mathcal{L}$ de símbolos no lógicos. [...] Cada símbolo en $\mathcal{L}$ tiene una aridad especificada, que es un número natural, y un tipo especificado, que es o ''símbolo de predicado" o "símbolo de función". Si estamos discutiendo ZFC, entonces $\mathcal{L} = \left\{ \in\right\}$, donde $\in$ es un símbolo de predicado.

Definición 1.6.3 $\;$ $R$ es una función si y solo si $R$ es una relación y para cada $x$, hay a lo sumo un $y$ tal que $(x,y) \in R$. Si $\exists y [xRy]$, entonces $R(x)$ denota ese $y$ único.

Y ahora Enderton, H. B. (2001). Introducción matemática a la lógica. Elsevier.

Una función es una relación $F$ con la propiedad de ser únivaluada. Para cada $x$ en dom $F$ solo hay un $y$ tal que $x, y \in F$.

Suponemos en lo sucesivo que se nos han dado infinitamente muchos objetos distintos (que llamamos símbolos), dispuestos de la siguiente manera:
A. Símbolos lógicos $\;$ 0. Paréntesis: $($ , $)$. $\;$ 1. Símbolos de conectores proposicionales: $\rightarrow$, $\neg$. $\;$ 2. Variables (una para cada entero positivo n): $\; v_1 , v_2 , \ldots$ $\;$ 3. Símbolo de igualdad (opcional): =.
B. Parámetros $\;$ 0. Símbolo cuantificador: $\forall$. $\;$ 1. Símbolos de predicado: Para cada entero positivo $n$, algún conjunto (posiblemente vacío) de símbolos, llamados símbolos de predicado de $n$ plazas. $\;$ 2. Símbolos constantes: Algunos símbolos (posiblemente vacíos). $\;$ 3. Símbolos de función: Para cada entero positivo $n$, algún conjunto (posiblemente vacío) de símbolos, llamados símbolos de función de $n$ plazas.

Answer 1

Estas son dos nociones distintas pero relacionadas.

En la lógica de primer orden de un solo tipo, definimos un "vocabulario" como un conjunto de símbolos de predicado y un conjunto de símbolos de función (cada uno con una aridad dada). Por ejemplo, si estamos describiendo un campo ordenado, podríamos tener símbolos de función $+$ y $\cdot$ y el símbolo de predicado $\leq$. Abusamos de la notación escribiendo $x + y$ en lugar de $+(x, y)$ (y lo mismo con $\cdot$ y $\leq$).

Una vez que tenemos un vocabulario, podemos considerar afirmaciones lógicas construidas a partir del vocabulario. Por ejemplo, podríamos considerar la oración $\forall x \forall y \forall z, x \leq y \to x + z \leq y + z$.

Es importante tener en cuenta aquí que los símbolos de función y los símbolos de predicado son solo símbolos. No tienen ningún "significado" per se, excepto en cómo pueden ser utilizados sintácticamente para construir afirmaciones y oraciones.

Luego podemos introducir un conjunto de reglas formales de deducción que describen cómo podemos probar oraciones a partir de otras oraciones previamente conocidas. Esto nos da una noción de prueba formal. Hay varias formas de hacer esto, pero todas son equivalentes.

Ahora cambiemos de tema a teoría de conjuntos. En la teoría de conjuntos, podemos definir la noción de un "subconjunto". También podemos decir qué significa formalmente la afirmación $f : A \to B$.

Dentro de la teoría de conjuntos, podemos tomar afirmaciones formales en lógica de primer orden e interpretar estas afirmaciones como referentes a un conjunto específico.

Para ser precisos, sea $P$ un conjunto de símbolos de predicado y $F$ un conjunto de símbolos de función, cada uno con una aridad. Una estructura en el vocabulario $(P, R)$ es un conjunto $M$, junto con, para cada símbolo de predicado $n$-ario $Q \in P$, un conjunto $Q_M \subseteq M^n$, y también junto con, para cada símbolo de función $m$-ario $f \in F$, una función $f_M : M^m \to M$.

Para cada afirmación formal $\phi$, entonces podemos interpretar lo que significaría que $\phi$ sea verdadera en la estructura $M$. Es decir, podemos determinar qué significaría que $M$ modele $\phi$ (escrito como $M \models \phi$). Por ejemplo, digamos que estamos tratando con el vocabulario $+, \cdot, \leq$, y interpretamos este vocabulario en la estructura $(\mathbb{Z}, +, \cdot, \leq)$. Nota que el símbolo de función $+$ y la función $+$ son dos cosas totalmente diferentes; solo los estamos denotando con el mismo carácter. Esto se conoce como "abuso de notación" - es algo que no es técnicamente correcto, pero a menudo puede llevar a una mayor comprensión.

La afirmación $\mathbb{Z} \models \forall x \forall y \forall z . x \leq y \to x + z \leq y + z$ se interpreta entonces como que para todos los enteros $x, y,$ y $z$, si $x \leq y$ entonces $x + z \leq y + z$.

La situación se complica aún más por el hecho de que la teoría de conjuntos es en sí misma una teoría formal en lógica de primer orden. Entonces estamos usando la teoría de conjuntos, que se expresa formalmente como una teoría específica en lógica de primer orden, para interpretar teorías en lógica de primer orden dentro de estructuras en la teoría de conjuntos.