¿Existe un argumento más rápido desde las condiciones de derivabilidad de HBL hasta la equivalencia de puntos fijos de $\neg\Box$ a $\mathsf{Con}$ ?

Question

Estoy a punto de enviar el último PDF corregido de la segunda edición de mi libro de Gödel, y se me ocurre la siguiente pregunta (¿¡neurótica?!?).

En la discusión sobre el Segundo Teorema de Incompletitud, utilizo (por supuesto) las tres condiciones de derivabilidad de HBL que rigen el predicado de demostrabilidad de $T$

C1. Si $T \vdash \varphi$ entonces $T \vdash \Box\varphi$ ,

C2. $T \vdash \Box\mathsf{(\varphi \to \psi)} \to (\Box\varphi \to \Box\psi)$ ,

C3. $T \vdash \Box\varphi \to \Box\Box\varphi$ ,

Doy el siguiente argumento para el teorema de que si $\gamma$ es punto fijo para $\neg\Box$ en $T$ es demostrablemente equivalente a $\neg\Box\bot$ . [Si se utiliza "sentencia de Gödel", como hacen algunos, para referirse a un punto fijo de $\neg\Box$ entonces esto demuestra que, al menos en relación con una elección de predicado de demostrabilidad, las sentencias de Gödel son demostrablemente equivalentes].

1. $T \vdash \gamma \equiv \neg\Box\gamma$
2. $T \vdash \gamma \to (\Box\gamma \to \bot)\quad\quad\text{From 1, by logic}$
3. $T \vdash \Box(\gamma \to (\Box\gamma \to \bot))\quad\quad\text{From 2 by C1}$
4. $T \vdash \Box\gamma \to \Box(\Box\gamma \to \bot))\quad\quad\text{From 3, by C2}$
5. $T \vdash \Box\gamma \to (\Box\Box\gamma \to \Box\bot)\quad\quad \text{From 4, by C2}$
6. $T \vdash \Box\gamma \to \Box\Box\gamma\quad\quad \text{From C3}$
7. $T \vdash \Box\gamma \to \Box\bot\quad\quad \text{From 5 and 6}$
8. $T \vdash \bot \to \gamma\quad\quad\text{Logic}$
9. $T \vdash \Box(\bot \to \gamma)\quad\quad \text{From 8, by C1}$
10. $T \vdash \Box\bot \to \Box\gamma \quad\quad \text{From 9, by C2}$
11. $T \vdash \Box\gamma \equiv \Box\bot \quad\quad \text{From 7 and 10}$
12. $T \vdash \gamma \equiv \neg\Box\bot \quad\quad \text{From 1 and 11}$

Pregunta/problema: Esta es la prueba que estaba en la primera edición, y nadie se quejó -- pero ¿es esta la prueba más corta? ¿O he recorrido las casas de forma poco elegante?

Answer 1

Es bastante elegante desde mi punto de vista informático:

Visto a través de la correspondencia Curry-Howard, las condiciones HBL corresponden a la tipificación básica metaprogramación donde $\Box \tau$ es el tipo de fragmentos cerrados de texto de programa de tipo $\tau$ . Si para facilitar la lectura escribimos $\Box \tau$ como $[\tau]$ y la flecha se asocia a la derecha, las condiciones son

C1. Si $M$ es un término cerrado de tipo $\tau$ entonces $\ulcorner M\urcorner$ es un término de tipo $[\tau]$ .

C2. Para cada $\alpha$ y $\beta$ hay un término $\mathtt{App}_{\alpha,\beta}$ de tipo $[\alpha\to\beta]\to[\alpha]\to[\beta]$ .

C3. Para cada $\alpha$ hay un término $\mathtt{Lift}_{[\alpha]}$ de tipo $[\alpha]\to\bigl[[\alpha]\bigr]$ .

Las condiciones C1 y C2 nos permiten formar cuasiquotaciones : $$ \ulcorner \cdots \llcorner M \lrcorner \cdots \urcorner \qquad\text{means}\qquad \mathtt{App}\;\ulcorner \lambda x. \cdots x \cdots \urcorner\; \ulcorner M \urcorner$$

En su prueba dada $\gamma \equiv \Box\gamma\to\bot$ estás asumiendo un término $\mathtt{p}: \gamma\to[\gamma]\to\bot$ . También tienes, desde la lógica, $\mathtt{Explode}:\bot\to\alpha$ para todos $\alpha$ .

Su prueba ahora corresponde a construir, (con algunos $\beta\eta$ -recesos de la traducción de la cuasiquote ya reducida):

$$\lambda x.\ulcorner \mathtt p\;\llcorner x\lrcorner\;\llcorner \mathtt{Lift}\;x\lrcorner\urcorner ~:~ [\gamma]\to[\bot] $$ $$ \lambda x:\ulcorner \mathtt{Explode}\;\llcorner x \lrcorner\urcorner ~:~ [\bot]\to[\gamma] $$

Es difícil ver cómo podría hacerse más corto. Esencialmente, todo lo que haces parece ser la configuración necesaria para poder utilizar $\mathtt{p}$ para cualquier cosa dado que $\mathtt{Lift}$ sólo funciona cuando ya tienes uno $\Box$ .

Jugué un poco con empezar desde $\delta\equiv\Box\neg\delta$ en su lugar, pero eso parece no llevar a ninguna parte.

---

Por cierto, no me resisto a señalar que la habitualmente bastante impenetrable demostración modal estándar del teorema de Löb se vuelve muy sencilla y bella gracias a esta correspondencia. La premisa del teorema es que conocemos un término $\mathtt{eval}$ de tipo $[\tau]\to\tau$ (donde el nombre "eval" es sugerente pero no del todo fiable porque todo lo que realmente sabemos es que $\mathtt{eval}$ producirá algunos valor del tipo $\tau$ no necesariamente relacionado con la entrada a $\mathtt{eval}$ ).

El teorema de Löb (y la prueba estándar) observa simplemente que el tipo $\tau$ está habitado por un programa que va:

1. Producir una copia de mi propio código fuente, por la propiedad fixpoint.
2. Solicitar $\mathtt{eval}$ a ese código fuente y mostrar su resultado.