[franma]

Buenas a todos,

Mis apuntes dicen que se puede definir en \( \mathsf{ZF} \) un predicado \( F \vdash f \) que expresa que una fórmula \( f \in Form_0 \) es derivable (en LK) a partir de un conjunto de formulas \( F \subseteq Form_0 \).

¿Alguien tendría idea de como hacer esto? No preciso nada demasiado detallado, con una idea general me bastaría. Ya que hasta el momento he dado este hecho como cierto pero al momento de sentarme a escribir tal predicado no he podido. Me imagino que debemos "simular" lo que se hace normalmente para definir las derivaciones en NK por ejemplo, ¿no? Aunque de nuevo, no me sale

Saludos,
Franco.

[Carlos Ivorra]

Para responder a eso ayudaría saber cómo te han definido concretamente LK.

[franma]

Hola Carlos ,

El sistema LK esta definido en las siguientes diapositivas. Aquí también esta definido lo que son las derivaciones (a partir de la página 9). Perdón que no las copie pero es un poco extenso y no se como escribir arboles de derivaciones en \( \LaTeX \)

Saludos,
Franco.

[Carlos Ivorra]

¡Uf! Cálculo secuencial. Es muy interesante y útil, pero para formalizarlo es bastante más molesto que un cálculo deductivo a la Hilbert.

Si tienes un lenguaje formal \( \mathcal L \), puedes definir un secuente como un par ordenado \( (\Gamma, \Delta) \) de conjuntos finitos de fórmulas de \( \mathcal L \) (o, si quieres ser más fiel con tus apuntes, de sucesiones finitas de fórmulas de \( \mathcal L \), aunque eso no hace más que complicar las cosas). En la práctica, puedes escribir \( \Gamma\vdash \Delta \) en lugar de \( (\Gamma, \Delta) \).

Si sólo vas a considerar reglas de inferencia con a lo sumo dos premisas (como sucede en LK), puedes definir un árbol como un conjunto finito \( A \) de sucesiones finitas en \( 2 = \{0, 1\} \) tal que si \( s\in A \) y \( n \) es menor que la longitud de \( s \), entonces la restricción \( s|_n\in A \).

Y un árbol de secuentes es una aplicación \( S \) cuyo dominio es un árbol \( A \) y que a cada \( s\in A \) le asigna un secuente \( S_s \).

Y una deducción a partir de un conjunto de secuentes \( P \) (premisas) es un árbol de secuentes \( S \) de dominio \( A \) que cumpla la definición de deducción, es decir, que

1) si \( s\in A \) es maximal (no tiene ninguna extensión en \( A \), entonces \( S_s \) es un axioma, es decir, un secuente de la forma \( ((\phi), (\phi)) \) o bien un secuente de \( P \) (una premisa)

2) En otro caso, o bien \( s \) tiene una única extensión inmediata \( s'\in A \) (es decir que \( s\subset s' \) y la longitud de \( s' \) es una unidad más que la de \( s \)) o bien tiene dos extensiones \( s', s''\in A \), y se cumple que \( S_s \) es consecuencia de \( S_{s'} \) (o de \( S_{s'} \) y \( S_{s''} \)) por una de las reglas de inferencia de LK.

Una derivación en ZF a partir de un conjunto de premisas \( F \) es el caso particular en el que \( \mathcal L \) es el lenguaje de la teoría de conjuntos y \( P \) es el conjunto de secuentes de la forma \( \vdash \alpha \), donde \( \alpha \) es un axioma de ZF o bien una fórmula de \( F \).

Y entonces \( F\vdash f \) se define como que existe una derivación \( S \) en ZF con premisas \( F \) cuyo secuente final es \( S_{\emptyset} = (\vdash f) \).

[franma]

Hola Carlos ,

¡Uf! Cálculo secuencial. Es muy interesante y útil, pero para formalizarlo es bastante más molesto que un cálculo deductivo a la Hilbert.

Todo esto lo vimos en su momento en mi curso de lógica pero nunca entramos en detalle en el tema de formalizar cosas como \( \vdash_{\mathsf{LK}} \) más allá de dar las reglas y hablar por arriba de "los árboles". Así que esto también me sirve para aprender como se hace.

Si tienes un lenguaje formal \( \mathcal L \), puedes definir un secuente como un par ordenado \( (\Gamma, \Delta) \) de conjuntos finitos de fórmulas de \( \mathcal L \) (o, si quieres ser más fiel con tus apuntes, de sucesiones finitas de fórmulas de \( \mathcal L \), aunque eso no hace más que complicar las cosas). En la práctica, puedes escribir \( \Gamma\vdash \Delta \) en lugar de \( (\Gamma, \Delta) \).

De acuerdo.

Si sólo vas a considerar reglas de inferencia con a lo sumo dos premisas (como sucede en LK), puedes definir un árbol como un conjunto finito \( A \) de sucesiones finitas en \( 2 = \{0, 1\} \) tal que si \( s\in A \) y \( n \) es menor que la longitud de \( s \), entonces la restricción \( s|_n\in A \).

¿Aquí la intuición es que cada elemento \( s\in A \) representa un posible camino en el árbol "binario" \( A \)? Por ejemplo \( s = \{((0,0),(1,0),(2,1)\} \) sería como hacer derecha-derecha-izquierda. ¿O la interpretación es otra?

Y un árbol de secuentes es una aplicación \( S \) cuyo dominio es un árbol \( A \) y que a cada \( s\in A \) le asigna un secuente \( S_s \).

De acuerdo.

Y una deducción a partir de un conjunto de secuentes \( P \) (premisas) es un árbol de secuentes \( S \) de dominio \( A \) que cumpla la definición de deducción, es decir, que

1) si \( s\in A \) es maximal (no tiene ninguna extensión en \( A \), entonces \( S_s \) es un axioma, es decir, un secuente de la forma \( ((\phi), (\phi)) \) o bien un secuente de \( P \) (una premisa)

2) En otro caso, o bien \( s \) tiene una única extensión inmediata \( s'\in A \) (es decir que \( s\subset s' \) y la longitud de \( s' \) es una unidad más que la de \( s \)) o bien tiene dos extensiones \( s', s''\in A \), y se cumple que \( S_s \) es consecuencia de \( S_{s'} \) (o de \( S_{s'} \) y \( S_{s''} \)) por una de las reglas de inferencia de LK.

Perfecto, creo que lo entiendo.

Una derivación en ZF a partir de un conjunto de premisas \( F \) es el caso particular en el que \( \mathcal L \) es el lenguaje de la teoría de conjuntos y \( P \) es el conjunto de secuentes de la forma \( \vdash \alpha \), donde \( \alpha \) es un axioma de ZF o bien una fórmula de \( F \).

Y entonces \( F\vdash f \) se define como que existe una derivación \( S \) en ZF con premisas \( F \) cuyo secuente final es \( S_{\emptyset} = (\vdash f) \).

Excelente, comprendo la idea. Aunque hay que pedir siempre que \( \emptyset \in A \), ¿o no?


No se si sea apropiado (si no lo es puedo abrir un nuevo hilo) pero una vez tenemos esta definición, en mis notas se define:

\( \text{Cons}(F) :\equiv (\exists f\in \text{Form}_0)\ F\not \vdash f \)

Y se enuncia la siguiente proposición:

Proposición

Todo conjunto de fórmulas que tiene un modelo es consistente:

\( (\forall F\subseteq \text{Form}_0)[\exists M\exists E\ (M,E)\models F)\Rightarrow \text{Cons}(F)] \)

[cerrar]

Donde \( (M,E)\models F \) esta definido como:

\( (M,E)\models F :\equiv M\neq \emptyset \land E\subseteq M^2 \land (\forall f\in F)\ (M,E)\models f \)

Y me estaba preguntando como probarla Se me ocurre que si logramos probar (tal vez por inducción interna en \( \text{Form} \), aunque todavía no se me ocurre bien como) que:

\( (\forall f\in \text{Form}_0)(F\vdash f \Rightarrow (M,E)\models f) \)

Entonces si suponemos por absurdo \( \neg\text{Cons}(F) \) tenemos en particular que \( F\vdash (\dot{\forall}{\tt{x}})({\tt{x}}\not\doteq {\tt{x}}) \) luego por el "lema" tendríamos que \( (M,E)\models (\dot{\forall}{\tt{x}})({\tt{x}}\not\doteq {\tt{x}}) \) luego \( (\forall x\in M)x\not = x \) pero como \( M \neq \emptyset \) llegamos a un absurdo.

¿Sería algo así?

Saludos,
Franco.

[Carlos Ivorra]

¿Aquí la intuición es que cada elemento \( s\in A \) representa un posible camino en el árbol "binario" \( A \)? Por ejemplo \( s = \{((0,0),(1,0),(2,1)\} \) sería como hacer derecha-derecha-izquierda. ¿O la interpretación es otra?

Sí. \( A \) es el conjunto de los nodos del árbol, y luego, a cada nodo, le asignas un secuente.

Excelente, comprendo la idea. Aunque hay que pedir siempre que \( \emptyset \in A \), ¿o no?

Sí, o simplemente exigir que \( A\neq \emptyset \), pues si existe un \( s\in A \), entonces \( \emptyset = s|_0\in A \), por definición de árbol.

No se si sea apropiado (si no lo es puedo abrir un nuevo hilo) pero una vez tenemos esta definición, en mis notas se define:

\( \text{Cons}(F) :\equiv (\exists f\in \text{Form}_0)\ F\not \vdash f \)

Y se enuncia la siguiente proposición:

Proposición

Todo conjunto de fórmulas que tiene un modelo es consistente:

\( (\forall F\subseteq \text{Form}_0)[\exists M\exists E\ (M,E)\models F)\Rightarrow \text{Cons}(F)] \)

[cerrar]

Donde \( (M,E)\models F \) esta definido como:

\( (M,E)\models F :\equiv M\neq \emptyset \land E\subseteq M^2 \land (\forall f\in F)\ (M,E)\models f \)

Y me estaba preguntando como probarla Se me ocurre que si logramos probar (tal vez por inducción interna en \( \text{Form} \), aunque todavía no se me ocurre bien como) que:

\( (\forall f\in \text{Form}_0)(F\vdash f \Rightarrow (M,E)\models f) \)

Entonces si suponemos por absurdo \( \neg\text{Cons}(F) \) tenemos en particular que \( F\vdash (\dot{\forall}{\tt{x}})({\tt{x}}\not\doteq {\tt{x}}) \) luego por el "lema" tendríamos que \( (M,E)\models (\dot{\forall}{\tt{x}})({\tt{x}}\not\doteq {\tt{x}}) \) luego \( (\forall x\in M)x\not = x \) pero como \( M \neq \emptyset \) llegamos a un absurdo.

¿Sería algo así?

No. Es mucho más sencillo. Si \( F \) tiene un modelo, pero fuera contradictorio, toda fórmula cumpliría \( F\vdash f \). En particular, \( F\vdash \exists x\, x\neq x \), y entonces, \( (M, E)\vDash \exists x\,x\neq x \), pero esto es falso, luego tenemos una contradicción que prueba que \( F \) es consistente.

[franma]

Hola Carlos

Sí. \( A \) es el conjunto de los nodos del árbol, y luego, a cada nodo, le asignas un secuente.

Perfecto.

Sí, o simplemente exigir que \( A\neq \emptyset \), pues si existe un \( s\in A \), entonces \( \emptyset = s|_0\in A \), por definición de árbol.

Tienes razón.

No. Es mucho más sencillo. Si \( F \) tiene un modelo, pero fuera contradictorio, toda fórmula cumpliría \( F\vdash f \).

Toda fórmula interna, ¿no?

En particular, \( F\vdash \exists x\, x\neq x \), y entonces, \( (M, E)\vDash \exists x\,x\neq x \)

Formalmente habría que escribir \( \dot{\exists} {\tt{x}}\, {\tt{x}}\not\doteq {\tt{x}} \), ¿no? ¿Y no estamos usando implícitamente que si \( F\vdash f \) entonces \( (M,E)\models f \)? ¿O eso es obvio y no lo veo?

Saludos,
Franco.

[Carlos Ivorra]

No. Es mucho más sencillo. Si \( F \) tiene un modelo, pero fuera contradictorio, toda fórmula cumpliría \( F\vdash f \).

Toda fórmula interna, ¿no?

Sí.

En particular, \( F\vdash \exists x\, x\neq x \), y entonces, \( (M, E)\vDash \exists x\,x\neq x \)

Formalmente habría que escribir \( \dot{\exists} {\tt{x}}\, {\tt{x}}\not\doteq {\tt{x}} \), ¿no?

Sí.

¿Y no estamos usando implícitamente que si \( F\vdash f \) entonces \( (M,E)\models f \)?

Sí, por eso se cumple lo que digo.

[franma]

¿Y no estamos usando implícitamente que si \( F\vdash f \) entonces \( (M,E)\models f \)?

Sí, por eso se cumple lo que digo.

¿Y eso se prueba por inducción interna en \( \text{Form} \)?

[Carlos Ivorra]

¿Y eso se prueba por inducción interna en \( \text{Form} \)?

Ah, disculpa, que en los últimos mensajes no nos estábamos entendiendo, porque había pensado que esto:

\( (\forall f\in \text{Form}_0)(F\vdash f \Rightarrow (M,E)\models f) \)

era tu definición de \( (M, E)\vDash F \), cuando en realidad era algo que preguntabas si era cierto. Por eso lo había dado por hecho y no entendía por qué insistías en ello.

Aquí el hecho de que definas las deducciones en términos del cálculo secuencial complica un poco las cosas.  Eso se prueba por inducción sobre la altura del árbol de una derivación de \( f \).

Más precisamente, hay que probar que todo secuente \( \Gamma\vdash \Delta \) derivable con premisas en \( F \) es verdadero en \( (M, E) \), lo que significa que \( (M, E)\vDash \lnot\gamma_1\lor \cdots \lor \lnot\gamma_m\lor \delta_1\lor \cdots \lor \delta_n \), donde \( \Gamma = (\gamma_1,\ldots, \gamma_m) \) y \( \Delta = (\delta_1,\ldots, \delta_n) \). En particular, si \( F\vdash f \), tenemos que el secuente \( \vdash f \) es derivable con premisas en \( F \), y por lo tanto \( (M, E)\vDash f \).

A su vez, para probar eso se razona por inducción sobre la altura del árbol de una derivación de \( \Gamma\vdash \Delta \).

Si un secuente es derivable mediante un árbol de altura 0, es que se trata de un axioma o de un secuente \( \vdash f \), con \( f\in F \). En el segundo caso es verdadero en \( (M, E) \) por hipótesis, y en el primero es de la forma \( g\vdash g \), y es claramente verdadero, pues esto equivale a que \( (M, E)\vDash \lnot g\lor g \).

Luego, si es cierto para secuentes derivables mediante árboles de altura menor que \( n \) y tenemos un secuente derivable mediante un árbol de altura \( n \), hay que considerar todas las reglas de inferencia que pueden llevar hasta él. Por hipótesis de inducción, su o sus secuentes superiores son verdaderos en \( (M, E) \) y basta probar que todas las reglas de inferencia pasan de secuentes verdaderos a secuentes verdaderos.