Primero lógica de primer orden - ¿por qué necesitamos símbolos de función?

Question

Usar símbolos de función en lógica de primer orden nos obliga a definir "términos" de manera inductiva, lo que hace que muchas pruebas sean más largas y mucho más tediosas. Por supuesto, los símbolos de función simplifican las cosas cuando se intenta usar la lógica de primer orden para describir cosas, pero en apariencia parece que podrían ser reemplazados completamente por relaciones: En lugar de $f$ utilizar una relación $R_f$ de manera que en lugar de escribir $\varphi(f(x))$ se escriba ($\forall x\exists! y(R(x,y))\wedge R(x,y)\wedge\varphi(y)$. Ahora utiliza $f(x)$ como una notación abreviada, para que puedas usarlo en "la vida real" pero evitarlo en las pruebas.

Supongo que me estoy perdiendo alguna necesidad profunda aquí, ¿pero cuál?

(Lo mismo ocurre con los símbolos constantes, pero no complican las cosas tanto como lo hacen los símbolos de función).

Answer 1

Siempre puedes tomar una teoría de primer orden con constantes y símbolos de función y reemplazarla con una teoría utilizando solo símbolos de relación. Esto se hace a expensas de complicar la teoría, ya que, por ejemplo, si $R$ es el símbolo relacional que representa al símbolo funcional binario $f$, necesitamos un axioma de la forma $$( \forall x ) ( \forall y ) ( \exists z ) ( \forall u ) ( R(x,y,u) \leftrightarrow u = z ).$$ Pero como $R$ y $f$ son definibles uno a partir del otro, habría una traducción natural de los teoremas de una teoría a la otra.

Otro gasto está en la afirmación de ciertos teoremas de teoría de modelos. Por ejemplo, una teoría $T$ se dice que admite eliminación de cuantificadores si para cada fórmula $\phi (x_1 , \ldots, x_n )$ hay una fórmula libre de cuantificadores $\psi (x_1 , \ldots, x_n )$ tal que $$T \vdash (\forall x_1 ) \cdots ( \forall x_n ) ( \phi \leftrightarrow \psi ).$$ El ejemplo básico de una teoría que admite eliminación de cuantificadores es la teoría de cuerpos reales cerrados. Observa que si el lenguaje subyacente no tiene símbolos constantes, entonces no hay oraciones libres de cuantificadores, y por lo tanto ninguna teoría sin símbolos constantes puede admitir eliminación de cuantificadores. Se tendría que modificar la definición para referirse solo a aquellas fórmulas $\phi$ con al menos una variable libre. Se puede demostrar que esto sería fiel, pero también es una definición algo menos natural.

Answer 2

Formalmente, tienes toda la razón: los símbolos de función podrían ser "definidos" mediante el uso de relaciones. Pero la noción de términos hace que muchas cosas sean mucho más naturales.

Entre las características que nos gustaría tener en nuestra lógica de primer orden está que la estructura de una demostración de una afirmación matemática en alguna teoría de FOL (por ejemplo, la teoría de grupos) refleje estructuralmente la demostración en matemáticas en lenguaje natural. En matemáticas en lenguaje natural, sin embargo, usamos funciones (y operaciones) todo el tiempo, y a menudo es muy poco natural considerarlas como relaciones. Esto sigue siendo un poco ambiguo, sin embargo. Un buen ejemplo de cómo esto aparece en lógica es cuando trabajamos de manera elemental con embeddings de modelos. Trabajar con términos en ese contexto te permite aprovechar de manera muy natural la perspectiva de que los objetos en un modelo surgen -- son "creados" si se quiere -- cerrándose bajo funciones y operaciones. Sin términos en el lenguaje, se vuelve muy difícil emplear ese tipo de razonamiento para mediar entre cuestiones semánticas y sintácticas.