¿Puede demostrarse explícitamente el axioma de elección en lógica de predicados (intuicionista), o es necesario algo como la teoría de tipos intuicionista?

Question

En matemáticas intuicionistas, un axioma de elección de la forma

$$ \forall x \exists y R(x,y) \rightarrow \exists f \forall x R(x, fx) $$

es válido por el significado de los cuantificadores (comp. Dummett, Elementos del intuicionismo , 2000).

En la teoría intuicionista de tipos, es posible demostrar realmente el axioma de elección. Por ejemplo,

$$ (\lambda z)((\lambda x) p_{left}(z(x)),(\lambda x)p_{right}(z(x))) $$

es un objeto de prueba para un axioma de elección de la forma

$$ (\Pi x:A)(\Sigma y:B)R \rightarrow (\Sigma f :(\Pi x:A)B)(\Pi x:A)R(f(x)/y), $$ donde $p_{left}$ y $p_{right}$ son las funciones de proyección (comp. Martin-Löf, "Constructive Mathematics and Computer Programming", 1982).

Lo que me interesa es la relación precisa entre la lógica de predicados y la teoría de tipos. ¿Puede probarse el axioma de elección en la primera, o es necesario el lenguaje más expresivo de la teoría de tipos, que puede referirse a objetos de prueba y construcciones directamente? Según Dummett, en lógica intuicionista, el axioma de elección es verdadero debido al significado constructivista de los cuantificadores . Pero esto no corresponde a una formal prueba dentro del sistema, sino un resultado metateórico.

Ahora bien, mi opinión es la siguiente: la lógica de predicados no puede representar adecuadamente construcciones u objetos de prueba. Pero en la prueba de Martin-Löf del axioma de elección, se opera directamente con objetos de prueba. Por lo tanto, mientras que en la lógica intuicionista de predicados el axioma de elección es un axioma propiamente dicho, es decir, un principio indemostrable que aceptamos debido a nuestra comprensión informal, se convierte en demostrable en el sistema más expresivo de la teoría intuicionista de tipos. ¿Estoy en lo cierto o se trata de un malentendido?

Answer 1

Creo que básicamente tiene razón. La diferencia clave aquí es la diferencia de idiomas. En los tipos más simples de lógica intuicionista de predicados de orden superior, no tenemos la capacidad de crear nuevas funciones "internamente a la lógica" mediante el uso de términos lambda.

En versiones algo más complicadas, existen operadores de formación de términos que permiten la abstracción lambda, pero estos sistemas siguen sin demostrar el axioma de elección. Esto se debe a que el sistema no ve $(\forall x)(\exists y)R(x,y)$ como expresión de una función.

En estos entornos, a veces podemos demostrar el axioma de elección como una especie de metateorema, que si $(\forall x)(\exists y)R(x,y)$ es demostrable entonces $(\forall x)R(x,tx)$ es demostrable para algún término $t$ . Este tipo de metateorema ofrece una interpretación precisa de comentarios como el de Dummett. También muestra cómo estos sistemas se alinean con la interpretación BHK del razonamiento constructivo, aunque la alineación sólo es visible en la metateoría.

La teoría intuicionista de tipos es bastante diferente de la lógica de predicados, no sólo porque los cuantificadores $\forall$ y $\exists$ a menudo se ignoran, y las operaciones de tipo interno $\Sigma$ y $\Pi$ se estudian en su lugar. De este modo, los sistemas teóricos de tipos mezclan la metateoría y la teoría de objetos más de lo que lo hace la lógica de predicados. (En realidad, hay que trabajar un poco para evitar la inconsistencia, a la que son vulnerables las teorías de tipos fuertes a través de la paradoja de Curry y cuestiones similares).

Sistemas como la teoría de tipos de Martin-Löf consiguen interiorizar lo suficiente la interpretación BHK como para demostrar análogos del axioma de elección (de nuevo, con cuantificadores sustituidos por constructores de tipos) sin interiorizar lo suficiente como para volverse inconsistentes.