Autor Tema: Igualdad entre descriptores

0 Usuarios y 1 Visitante están viendo este tema.

21 Septiembre, 2021, 06:49 pm
Leído 242 veces

Eparoh

  • $$\Large \color{#5e8d56}\pi\,\pi\,\pi$$
  • Mensajes: 347
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Hola a todos, estoy intentado demostrar que en un lenguaje formal \( \mathcal{L} \) con descriptor, si \( \alpha \) es una fórmula cualquiera y \( w \) es una variable que no está en \( \alpha \) entonces

\( \vdash z|\alpha = w|S_z^w \alpha \)

Estoy siguiendo la notación y resultados del libro de Lógica matemática de Carlos Ivorra, y se que lo anterior es realmente un teorema lógico pues no es complicado ver que es una fórmula lógicamente valida. Sin embargo, me gustaría poder demostrarlo formalmente, en \( K_\mathcal{L} \) sin necesidad de apelar al teorema de completitud semántica.

¿Alguna idea de como podría conseguirse?

Un saludo y muchas gracias por sus respuestas.

21 Septiembre, 2021, 10:35 pm
Respuesta #1

Carlos Ivorra

  • Administrador
  • Mensajes: 9,908
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
    • Página web personal
Hay que distinguir dos casos, o bien \( \exists ! z\,\alpha \) o bien \( \lnot \exists! z\,\alpha \). Vamos a considerar el primer caso.

No recuerdo cómo vas con la equivalencia de variables ligadas. Si supongo \( \exists ! z\,\alpha \), ¿puedo poner a continuación \( \exists u\forall z(\alpha\leftrightarrow u=z) \) donde \( u \) es cualquier variable que me convenga o tengo que tomar la de menor índice? Voy a suponer que me dejas elegir la variable \( u \). Si no, habría que afinar un poco más. Un esbozo de prueba es así:

1)\( \exists ! z\,\alpha \) Hipótesis
2) \( S_z^{z|\alpha}\alpha \) por DP 1
3) \( \exists u \forall z(\alpha\leftrightarrow u = z) \) (equivalente a 1)
4) \( \forall z(\alpha \leftrightarrow u = z) \) por EP 3
5) \( S_z^{z|\alpha}\alpha\leftrightarrow u = z|\alpha \) por EG 4
6) \( u = z|\alpha \) (se sigue de 5 y 2 eliminando el bicondicionador y usando MP)
7) \( S_z^w\alpha\leftrightarrow u = w \) por EG 4
8) \( \forall w(S_z^w\alpha\leftrightarrow u= w) \) por IG 7
9) \( \exists u\forall w(S_z^w\alpha\leftrightarrow u= w) \) por IP 8
10) \( \exists! w\, S_z^w\alpha \)  (equivalente a 9)
11) \( S_w^{w|S_z^w\alpha}S_z^w\alpha \) por DP 10
12) \( S_w^{w|S_z^w\alpha}S_z^w\alpha\leftrightarrow u = w|S_z^w\alpha \)  por EG 8
13) \( u = w\mid S_z^w\alpha \) (se sigue de 11 y 12, eliminando el bicondicionador y aplicando MP)
14) \( z\mid\alpha = w\mid S_z^w\alpha \) (se sigue de 6 y 13 por las reglas del igualador).

La única cuestión técnica que veo es que he usado la misma variable \( u \) al pasar de 1 a 3 que al pasar de 9 a 10 y, según las definiciones, no tendría por qué ser exactamente la misma. Si ya tienes probado que la cambiar la variable da lugar a una fórmula equivalente, listo. Y si no, no lo he pensado mucho, pero, en el caso en que el paso de 9 a 10 requiriera otra variable \( v \), ¿no bastaría cambiar \( u \) por \( v \) al eliminar el particularizador en 4? Si la \( v \) está disponible, ya está. En el peor de los casos, habría que probar antes que el cambio de variable da lugar a una fórmula equivalente.

El caso en que \( \lnot \exists ! z\alpha \) debería ser más sencillo, llegando a que tanto \( z\mid\alpha \) como \( w\mid S_z^w\alpha \) coinciden con \( x\mid x = x \).

22 Septiembre, 2021, 09:31 am
Respuesta #2

Eparoh

  • $$\Large \color{#5e8d56}\pi\,\pi\,\pi$$
  • Mensajes: 347
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Hola Carlos, gracias por la respuesta.

La cuestión técnica que comentas de utilizar la misma variable al pasar de 1 a 3 y de 9 a 10, creo que es correcto. En el Teorema 2.9 c), la equivalencia es cierta siempre que las variables \( y_1, \cdots, y_n \) no estén en \( \alpha \) y sean distintas de \( x_1, \cdots, x_n \), luego tomando el \( u \) de forma que no esté en ninguna de las fórmulas que nos interesan podemos tomar perfectamente la misma variable, ¿no?

Ahora bien, lo que no veo es de donde sale la equivalencia en 12).

Como dices, el otro caso cuando \( \lnot \exists! z\,\alpha \) creo que me ha salido facilmente. De todas formas, cuando consiga saber de donde sale 12) posteo una prueba completa a ver si esta todo correcto :)

Un saludo y muchas gracias.

22 Septiembre, 2021, 09:39 am
Respuesta #3

Carlos Ivorra

  • Administrador
  • Mensajes: 9,908
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
    • Página web personal
La cuestión técnica que comentas de utilizar la misma variable al pasar de 1 a 3 y de 9 a 10, creo que es correcto. En el Teorema 2.9 c), la equivalencia es cierta siempre que las variables \( y_1, \cdots, y_n \) no estén en \( \alpha \) y sean distintas de \( x_1, \cdots, x_n \), luego tomando el \( u \) de forma que no esté en ninguna de las fórmulas que nos interesan podemos tomar perfectamente la misma variable, ¿no?

Sí, claro, correcto es sin duda. Lo que no sabía era en qué punto estabas y si ya habías visto la prueba de ese hecho (no me puse a mirar mi libro para ver en qué momento te podía haber surgido este problema). En efecto, el teorema 2.9 c) es todo lo que se necesita.

Ahora bien, lo que no veo es de donde sale la equivalencia en 12).

Vaya, se me olvidó poner la indicación en ese paso. Ya la he añadido. Es simplemente una eliminación del generalizador en 8, cambiando w por la descripción.

22 Septiembre, 2021, 08:19 pm
Respuesta #4

Eparoh

  • $$\Large \color{#5e8d56}\pi\,\pi\,\pi$$
  • Mensajes: 347
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Hola Carlos, con el mensaje anterior esta ya todo claro  :laugh:

Muchas gracias y un saludo.