[Daniel Contreras]

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.

[Carlos Ivorra]

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.

Claro. La regla de la identidad te permite probar

\( f(x) = f(x) \)

Eso es lo mismo que

\( S_y^{f(x)}(y = f(x)) \)

Ahí puedes introducir el particulador, que te da

\( \exists y(y = f(x)) \)

Y ahí puedes introducir el generalizador y anteponer \( \forall x \).

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)?

No, eso no es un teorema lógico, y no sé qué relación ves con lo anterior. Considera un modelo cuyo universo sea el conjunto de los números naturales y en el que el funtor \( + \) se interpreta como la función que siempre toma el valor 0. En ese modelo la sentencia de la que hablas es falsa. De hecho, te vale cualquier modelo con más de un elemento en el que el funtor \( + \) se interprete como cualquier función constante que quieras fijar.

[Daniel Contreras]

Gracias Carlos por la respuesta.

Claro. La regla de la identidad te permite probar

\( f(x) = f(x) \)

Eso es lo mismo que

\( S_y^{f(x)}(y = f(x)) \)

Ahí puedes introducir el particulador, que te da

\( \exists y(y = f(x)) \)

Y ahí puedes introducir el generalizador y anteponer \( \forall x \).

Comprendo, aunque no llegué a plantearlo de ese modo mientras lo intentaba, sospecho que estoy malinterpretando algo...

Cuando dices

\( f(x) = f(x) \)

Eso es lo mismo que

\( S_y^{f(x)}(y = f(x)) \)

¿cómo se justifica ese paso formalmente? Me explico: En mi deducción coloco \( f(x) = f(x) \) y luego, por lo que creo entender, coloco \( S_y^{f(x)}(y = f(x)) \) que sería una aplicación de la regla de repetición, por... ¿Por definición de sustitución? ¿Quizás teorema 1.12 de tu libro? ¿O es que puedo realizar una sustitución a una nueva variable en cualquier momento? Son varias preguntas, pero espero que con ellas se entienda qué no entiendo. Tal vez lo abordas en tu libro y no le he prestado la debida atención.

No, eso no es un teorema lógico, y no sé qué relación ves con lo anterior. Considera un modelo cuyo universo sea el conjunto de los números naturales y en el que el funtor \( + \) se interpreta como la función que siempre toma el valor 0. En ese modelo la sentencia de la que hablas es falsa. De hecho, te vale cualquier modelo con más de un elemento en el que el funtor \( + \) se interprete como cualquier función constante que quieras fijar.

Pues tienes mucha razón y la verdad es que fue un error mío, lo lamento mucho (parece que no es buena idea escribir en \(  \LaTeX{} \) justo después de hacer ejercicio físico, en mi cabeza siempre estuve escribiendo otra cosa). Es claro que dicha afirmación no es un teorema lógico, y en general cuando un matemático escribe y demuestra tal cosa es en alguna teoría adecuada (como un grupo).

Lo que realmente quería escribir y preguntar era el recíproco:

\( \displaystyle \vdash \forall xyz (x=y \rightarrow x+z=y+z) \).

Respecto a la relación entre una cosa y la otra, pues tienes razón que no es nada clara, quizás solo exista en mis papeles e intentos de demostración, en donde llegué a ambas expresiones en un par de ocasiones.

[Daniel Contreras]

Pues he seguido intentándolo y he llegado a esta demostración. Si resulta que es correcta, pues quizás se respondan de paso varias de mis preguntas, si no lo es pues agradeceré que me corrijas:

[texx]
\displaystyle \begin{array}{lll}
(1) & x+z=x+z & \textrm{I} \\
(2) & \textrm{S}_{y}^{x}(x+z=y+z) & \textrm{R 1} \\
|\,(3) & x=y & \textrm{hipótesis}\\
|\,(4) & x+z=y+z & \textrm{ETI 3 2}\\
(5) & x=y \to x+z=y+z & {} \\
(6) & \forall xyz (x=y \to x+z=y+z) & \textrm{IG}\\
\end{array}
\\
[/texx]

(Pregunto de paso, ¿indicas en algún lugar cómo formateas las demostraciones para colocar, por ejemplo, la línea vertical en ciertas demostraciones?)

[Carlos Ivorra]

Cuando dices

\( f(x) = f(x) \)

Eso es lo mismo que

\( S_y^{f(x)}(y = f(x)) \)

¿cómo se justifica ese paso formalmente? Me explico: En mi deducción coloco \( f(x) = f(x) \) y luego, por lo que creo entender, coloco \( S_y^{f(x)}(y = f(x)) \) que sería una aplicación de la regla de repetición, por... ¿Por definición de sustitución? ¿Quizás teorema 1.12 de tu libro? ¿O es que puedo realizar una sustitución a una nueva variable en cualquier momento? Son varias preguntas, pero espero que con ellas se entienda qué no entiendo. Tal vez lo abordas en tu libro y no le he prestado la debida atención.

Se cumple que \( f(x) = f(x) \) es la misma fórmula que (no una fórmula equivalente a, sino la misma fórmula que)  \( S_y^{f(x)}(y = f(x)) \). Eso es por la definición de sustitución (definición 1.11, primero se aplica la cláusula c, luego la cláusula a en el miembro izquierdo y la d y luego la a en el derecho). El teorema 1.12 no tiene sentido aplicarlo aquí, porque es un teorema sobre modelos, y de lo que se trata es de probar que dos fórmulas son en realidad la misma fórmula, nada que tenga que ver con sus posibles significados.

Como son la misma fórmula, no hay ninguna deducción formal que hacer. Cuando pasas de una a la otra, simplemente estás escribiendo otra vez la misma fórmula, aunque haciendo referencia a ella con otro nombre. Ese paso sólo es conveniente por claridad, pero si omites la repetición, la deducción sigue siendo correcta, pues \( f(x)=f(x) \) es \( S_y^{f(x)}(y = f(x)) \) tanto si lo pones explícitamente como si no, y a partir de \( f(x)=f(x) \) puedes introducir el particularizador, si quieres.

Pues he seguido intentándolo y he llegado a esta demostración. Si resulta que es correcta, pues quizás se respondan de paso varias de mis preguntas, si no lo es pues agradeceré que me corrijas:

[texx]
\displaystyle \begin{array}{lll}
(1) & x+z=x+z & \textrm{I} \\
(2) & \textrm{S}_{y}^{x}(x+z=y+z) & \textrm{R 1} \\
|\,(3) & x=y & \textrm{hipótesis}\\
|\,(4) & x+z=y+z & \textrm{ETI 3 2}\\
(5) & x=y \to x+z=y+z & {} \\
(6) & \forall xyz (x=y \to x+z=y+z) & \textrm{IG}\\
\end{array}
\\
[/texx]

Está bien.

(Pregunto de paso, ¿indicas en algún lugar cómo formateas las demostraciones para colocar, por ejemplo, la línea vertical en ciertas demostraciones?)

Por algún motivo, la forma en que lo hago, que no usa sino instrucciones completamente estándar sobre formateado de tablas, no funciona en el foro, por lo que siempre he incluido las demostraciones como imágenes. Por ejemplo, esto me funciona en cualquier compilador LaTeX, pero no en el foro:

Código: [Seleccionar]

\begin{array}{llp{8cm}}
(1)&\lnot\forall x\alpha&Premisa\\
\multicolumn{1}{|l}{(2)}&\lnot\exists x\lnot\alpha&Hip\'otesis (reducci\'on al absurdo)\\
\multicolumn{1}{|l}{(3)}&\lnot\lnot\forall x\lnot\lnot\alpha&R 2\\
\multicolumn{1}{|l}{(4)}&\forall x\lnot\lnot\alpha&DN 3\\
\multicolumn{1}{|l}{(5)}&\lnot\lnot\alpha&EG 4\\
\multicolumn{1}{|l}{(6)}&\alpha&DN 5\\
\multicolumn{1}{|l}{(7)}&\forall x\alpha&IG 6 (contradicci\'on con 1)\\
(8)&\exists x\lnot\alpha
\end{array}

[Daniel Contreras]

Perfecto Carlos. Todo muy claro. Te lo agradezco mucho.

Respecto a la tabulación, por lo que veo es un problema con MathJax, la librería JavaScript que usa el foro para renderizar LaTeX. He probado con la misma versión que usa el foro y la actual (una nueva versión menor) y ninguna de ellas soporta \multicolumn, una lástima. Quizás la nueva versión 3 que viene en camino.