Muy buenas a todos. He estado estudiando lógica de primer orden, apoyándome principalmente en el libro de lógica de Carlos Ivorra y los distintos artículos y discusiones de este foro. Resulta que me surgió una duda, y aunque tal vez es un poco tonta, no logro darme una respuesta adecuada, así que preferí preguntar acá directamente (¡mi primer mensaje!). En realidad son dos dudas que expreso en este mismo hilo porque posiblemente están relacionadas.
Consideremos un lenguaje formal de primer orden con un funtor monádico \( f \), de modo que si \( x \) es un término también lo es \( f(x) \). Cuando leo esa frase entiendo que
pretende decir (considerando un modelo) que si tomo un objeto \( a \), existirá otro objeto (no necesariamente distinto) que puedo denotar como \( f(a) \). Estoy consciente que dicha explicación cae fuera de la definición de lenguaje formal, sin embargo, la fórmula
\( \forall x \exists y(y=f(x)) \)
está bien formada y "veo" (informalmente) que
pretende decir lo mismo que mi interpretación (otra vez informal) de lo que significa tener un funtor. Mi duda es la siguiente:
¿Es posible deducir dicha fórmula a partir de los axiomas y reglas de inferencia de \( K_{\mathcal L} \), o tal cosa es un disparate?Con esto me refiero a si existe una deducción para esa fórmula en cualquier lenguaje que incluya un funtor monádico.
La duda me surgió mientras practicaba haciendo algunas demostraciones por mi cuenta y quise demostrar lo que habitualmente un matemático escribiría como "si \( x+z=y+z \), entonces \( x=y \)". Entiendo que dicha expresión es deducible solo a partir de principios lógicos sin necesitar axiomas propios. Considero entonces un lenguaje formal de primer orden con igualador que incluye un funtor diádico \( + \), de modo que se tenga
\( \vdash \forall xyz (x+z=y+z\rightarrow x=y) \).
¿Es esto realmente un teorema lógico? Es decir, ¿es realmente deducible solo sin premisas adicionales (axiomas propios de alguna teoría)?
Espero haber sido claro en mis dudas y el contexto. Gracias de antemano.