Puntos fijos en computabilidad y lógica.

Esta pregunta también se ha publicado en Math.SE,

/math/1002540/fixed-points-in-computability-nd-logic

Espero que esté bien publicarlo aquí también. Si no es así, o si es demasiado básico para CS.SE, dígame y lo eliminaré.

Me gustaría entender mejor la relación entre los teoremas de punto fijo en la lógica y el cálculo de $\lambda$ .

Antecedentes

1) El papel de los puntos fijos en la incompletitud e indefinibilidad de la verdad

Según tengo entendido, aparte de la idea fundamental de internalizar la lógica, la clave de las pruebas de la indefinibilidad de la verdad de Tarski y del teorema de incompletitud de Goedel es la siguiente teorema lógico de punto fijo , que vive en una metateoría constructiva y finitista (espero que la formulación está bien, corríjame si algo es incorrecto o incorrecto):

Existencia de puntos fijos en la lógica.

Supongamos que ${\mathscr T}$ es una teoría suficientemente expresiva y recursivamente enumerable sobre el lenguaje ${\mathcal L}$ , y que ${\mathbf C}$ sea ​​una codificación de las fórmulas ${\mathcal L}$ en ${\mathscr T}$ , es decir, un algoritmo que convierte las fórmulas arbitrarias bien formadas φ en fórmulas L con una variable libre C ( φ ) ( v ) , de modo que para cualquier fórmula L φ tenemos T ⊢ ∃ ! v : C ( φ ) ( v ) .${\mathcal L}$$\varphi$${\mathcal L}$${\mathbf C}(\varphi)(v)$${\mathcal L}$$\varphi$${\mathscr T}\vdash \exists! v: {\mathbf C}(\varphi)(v)$

Entonces existe un algoritmo ${\mathbf Y}$ convierte las fórmulas bien formadas ${\mathcal L}$en una variable libre en fórmulas bien formadas ${\mathcal L}$cerradas, de modo que para cualquier fórmula ${\mathcal L}$ en una variable libre $\phi$ tenemos

$${\mathscr T}\vdash {\mathbf Y}(\phi)\Leftrightarrow \exists v: {\mathbf C}({\mathbf Y}(\phi))(v)\wedge \phi(v),$$ que, interpretando ${\mathbf C}$ como un símbolo de función definida $\lceil -\rceil$, también podría escribirse de manera más compacta como $${\mathscr T}\vdash {\mathbf Y}(\phi)\Leftrightarrow \phi(\lceil{\mathbf Y}(\phi)\rceil).$$

En otras palabras, ${\mathbf Y}$ es un algoritmo para la construcción de puntos fijos con respecto a la equivalencia ${\mathscr T}$ de las fórmulas de una variable ${\mathcal L}$.

Esto tiene al menos dos aplicaciones:

• Al aplicarlo al predicado $\phi(v)$ expresa " $v$ codifica una oración que, cuando se instancia con su propia codificación, no es demostrable". produce la formalización de "Esta oración no es demostrable", que se encuentra en el corazón del argumento de Goedel.

• Aplicarlo a para una oración arbitraria ϕ produce la indefinibilidad de la verdad de Tarski.$\neg\phi$$\phi$

2) Puntos fijos en λ sin tipo$\lambda$ tipo

En el cálculo tipo, la construcción de puntos fijos es importante en la realización de funciones recursivas.$\lambda$

Existencia de puntos fijos en cálculo :$\lambda$

Hay un combinador de punto fijo , es decir, un -term Y tal que para cualquier λ -term f , tenemos f ( Y f ) ~ alpha ß Y f $\lambda$$Y$$\lambda$$f$

$$f(Y f)\sim_{\alpha\beta} Yf.$$

Observación

Lo que me deja atónito es que el combinador de punto fijo en $\lambda f.(\lambda x. f(x x))(\lambda x. f(x x))$$\lambda$ cálculo refleja directamente, de una manera muy limpia y no técnica, la prueba habitual del teorema lógico de punto fijo:

En términos generales , dada una fórmula , uno considera la formalización φ ( v ) de la declaración " v codifica una oración que, cuando se instancia consigo misma, satisface ϕ ", y pone A ( ϕ ) : = φ ( ⌈ φ ⌉ ) . La oración φ ( v ) es como λ x . f ( x x ) y φ ( ⌈ φ ⌉ ) ( $\varphi$$\varphi(v)$$v$$\phi$${\mathbf A}(\phi) := \varphi(\lceil\varphi\rceil)$$\varphi(v)$$\lambda x. f(x x)$$\varphi(\lceil\varphi\rceil)$ corresponde a$(\lambda x. f(x x))(\lambda x. f(x x))$ .

Pregunta

A pesar de su idea rápidamente descrita, encontré que la prueba del teorema lógico de punto fijo es bastante técnica y difícil de llevar a cabo en todos los detalles; Kunen lo hace, por ejemplo, en el Teorema 14.2 de su libro 'Set Theory'. Por otro lado, el combinador en $Y$$\lambda$ es muy simple y sus propiedades se verifican fácilmente.

¿El teorema lógico de punto fijo se sigue rigurosamente de los combinadores de punto fijo en $\lambda$ cálculo ?

Por ejemplo, ¿se puede modelar el cálculo mediante fórmulas L hasta la equivalencia lógica, de modo que la interpretación de cualquier combinador de punto fijo proporcione un algoritmo como se describe en el teorema del punto fijo lógico?$\lambda$${\mathcal L}$

Editar

En vista de las muchas otras instancias del mismo argumento de diagonalización descrito en las respuestas de Martin y Cody, uno debería reformular la pregunta:

¿Existe una generalización común de los argumentos de diagonalización siguiendo el principio expresado en el combinador ? λ f . ( λ x . f ( x x ) ) ( λ x . f ( x x ) $Y$

$$\lambda f.(\lambda x. f(xx))(\lambda x.f(xx))$$

Si lo entiendo correctamente, una propuesta es el Teorema del punto fijo de Lawvere , ver más abajo. Sin embargo, desafortunadamente no puedo seguir las especializaciones relevantes en ninguno de los artículos que Martin citó en su respuesta, y estaría feliz si alguien pudiera explicarlas. Primero, para completar:

Teorema del punto fijo de Lawvere

Sea una categoría con productos finitos y φ : A × A → Y tal que para cualquier morfismo f : A → Y en C haya alguna ⌈ f ⌉ : 1 → A tal que para todos los puntos p : 1 → A uno tenga 1 p → A f → Y = 1 p → A ⟨ ⌈ f ⌉ , ID ${\mathscr C}$$\varphi: A\times A\to Y$$f: A\to Y$${\mathscr C}$$\lceil f\rceil: 1\to A$$p: 1\to A$

$$1\xrightarrow{p} A\xrightarrow{\ f\ } Y\ \ =\ \ 1\xrightarrow{p} A\xrightarrow{\langle \lceil f\rceil,\text{id}_A\rangle} A\times A\xrightarrow{\varphi} Y.$$

Luego, para cualquier endomorfismo , poniendo f : = A Δ → A × A φ → Y $g: Y\to Y$cualquier elección de⌈f⌉da lugar a un punto de fijog, a saber, 1 ⟨ ⌈ f ⌉ , ⌈ f ⌉ ⟩ → A×A varphi → Y

$$f\ :=\ A\xrightarrow{\Delta} A\times A\xrightarrow{\varphi} Y\xrightarrow{g} Y,$$ $\lceil f\rceil$$g$ $$1\xrightarrow{\langle\lceil f\rceil,\lceil f\rceil\rangle} A\times A\xrightarrow{\varphi} Y.$$

Esta es una afirmación en la teoría (intuitiva) de primer orden de categorías con productos finitos y, por lo tanto, se aplica a cualquier modelo de este último.

Por ejemplo , tomar todo el universo teórico de conjuntos como el dominio del discurso da la paradoja de Russel (tome el conjunto hipotético de conjuntos, Y : = Ω : = { 0 , 1 } y ρ : A × A → Ω el ∈ -predicar) y el teorema de Cantor (tome A cualquier conjunto y ρ : A × A → Ω correspondiente a la supuesta hipótesis A → Ω $A$$Y := \Omega := \{0,1\}$$\rho: A\times A\to\Omega$$\in$$A$$\rho: A\times A\to \Omega$$A\to\Omega^A$) Además, la traducción de la prueba del Teorema de Lawvere da los argumentos diagonales habituales.

Problema más concreto:

¿Alguien puede explicar en detalle una aplicación del Teorema de Lawvere a funciones recursivas parciales o los teoremas lógicos de punto fijo? En particular, ¿qué categorías debemos considerar allí?

En D. Pavlovic, Sobre la estructura de paradojas , el autor considera la categoría generada libremente por con Fin ( N${\mathbb N}$${\text{End}}({\mathbb N})$ las funciones recursivas parciales.

Lamentablemente, no entiendo lo que esto significa.

Por ejemplo, ¿cuál debería ser la ley de composición en $\text{End}({\mathbb N})$ ? ¿Composición de funciones recursivas parciales? Después de todo, se dice que el teorema de Lawvere aplica con , de modo que, en particular, cualquier morfismo N → N debe tener un punto fijo 1 → N . Si los endomorfismos son funciones recursivas parciales y si la composición significa composición de funciones, esto parece extraño: si los puntos 1 → N son solo elementos de N , entonces la afirmación es incorrecta, y si un morfismo 1 → $A=Y={\mathbb N}$${\mathbb N}\to{\mathbb N}$$1\to {\mathbb N}$$1\to {\mathbb N}$${\mathbb N}$$1\to {\mathbb N}$ es también una función parcial, por lo tanto, puede ser indefinido, el teorema del punto fijo es trivial.

¿Cuál es la categoría que uno realmente quiere considerar?

Tal vez el objetivo es obtener el teorema del punto fijo de Roger, pero de alguna manera uno debería construir una codificación de funciones recursivas parciales por números naturales en la definición de la categoría, y no puedo entender cómo hacerlo.

Sería muy feliz si alguien pudiera explicar la construcción de un contexto al que se aplica el Teorema del punto fijo de Lawvere, dando lugar a un teorema lógico de punto fijo o un teorema de punto fijo para funciones recursivas parciales.

¡Gracias!

Probablemente no estoy respondiendo directamente a su pregunta, pero hay una generalización matemática común de mucha paradoja, incluidos los teoremas de Gödel y el combinador Y. Creo que esto fue explorado por primera vez por Lawvere. Ver también [2, 3].

1. FW Lawvere, argumentos diagonales y categorías cerradas cartesianas .

2. D. Pavlovic, Sobre la estructura de las paradojas .

3. NS Yanofsky, Un enfoque universal para paradojas autorreferenciales, incompletitud y puntos fijos .

No tengo una respuesta completa a su pregunta, pero sí tengo esto:

Según Wikipedia dice

Para cada función recursiva parcial existe un índice p tal que φ p ≃ λ y . Q ( p , y $Q(x, y)$$p$

$$\varphi_p\simeq \lambda y.Q(p, y)$$ $\varphi$$\mathbb{N}$

$\lambda$

$\phi$${\mathscr T}$$n$

$${\mathscr T}\vdash \phi(\overline{n}) \Leftrightarrow {\mathscr T}\vdash \exists y, \varphi_n(y)=0$$

Esto no es exactamente lo que quieres, pero un truco de internalización puede darte una declaración más sólida

${\mathscr T}\vdash \phi(\overline{n})\leftrightarrow \exists y, \varphi_n(y) = 0$

Ahora, nuevamente, este no es el teorema lógico de punto fijo, pero puede servir para el mismo propósito.

Prueba: Definir $Q(x,y)$

$$Q(x,y) = 0 \mbox{ iff }{\mathscr T}\vdash \phi(\overline{x})\mbox{ in at most $y$ steps}$$ $Q$$\exists y, Q(x, y)$${\mathscr T}$$\phi(\overline{x})$${\mathscr T}\vdash\exists y,Q(\overline{x}, y)$$\omega$$Q$$\square$

Con un poco de reflexión, probablemente pueda fortalecer este argumento para darle el teorema completo directamente sin la internalización.