- ¿Cuál es exactamente el papel de la teoría de tipos en la creación de lógicas de orden superior? Lo mismo ocurre con la teoría de categorías/teoría de modelos, que creo que es una alternativa.
No piense en la teoría de tipos, la lógica categorial y la teoría de modelos como alternativas unos a otros. Cada paso en la progresión olvida progresivamente más estructura, y si esa estructura es esencia o desorden depende del problema que se intente resolver. A grandes rasgos, los dos polos son la teoría de tipos y la teoría de modelos, que se centran en las pruebas y la demostrabilidad, respectivamente.
Para un teórico del modelo, dos proposiciones son iguales si tienen el mismo valor de comprobabilidad/verdad. Para un teórico del tipo, la igualabilidad significa que tenemos una prueba de la biimplicación, que obviamente no es lo mismo que las proposiciones sean iguales. (De hecho, incluso la noción correcta de equivalencia para las pruebas aún no está resuelta a satisfacción de los teóricos del tipo).
Los lógicos categóricos tienden a moverse entre estos dos polos; por un lado, artilugios como las doctrinas de Lawvere y los topoi son esencialmente teórico-modelos, ya que son modelos de demostrabilidad. Por otro lado, artilugios como las categorías cartesianas cerradas dan modelos de demostraciones, hasta $\beta\eta$ -equivalencia.
- ¿Es la extensión a) de la deducción natural, b) del cálculo secuencial, o c) de algún otro sistema formal la mejor manera de crear lógicas de orden superior?
Depende de lo que haga. Si se está construyendo una herramienta informática, lo más adecuado es la deducción natural o el cálculo secuencial, porque ambos cálculos se ajustan a la práctica humana y ayudan a restringir la búsqueda de pruebas de forma útil para los ordenadores. Tiene sentido crear un sistema de cálculo secuencial o de deducción natural incluso si la teoría que se quiere utilizar (por ejemplo, la teoría de conjuntos) no se expresa normalmente en estos términos.
Por otra parte, la teoría de modelos ha tenido un éxito espectacular en las aplicaciones a las matemáticas, y esto se debe en parte a que porque no tiene una noción incorporada de sistema de pruebas, por lo que simplemente hay menos maquinaria que deba reinterpretarse antes de poder aplicarla a un problema matemático. (El uso correspondiente de la teoría de tipos está mucho menos desarrollado; los teóricos de la homotopía están en las primeras fases de convertir la teoría de tipos dependiente en matemáticas ordinarias).
- ¿Dónde entra el cálculo lambda tipado en la verificación de pruebas?
Toda lógica intuicionista bien llevada tiene su correspondiente cálculo lambda tipado. Véase Sorensen and Urcyczyn's Conferencias sobre la correspondencia Curry-Howard para (muchos) más detalles.
- ¿Existen otros enfoques distintos de la lógica de orden superior para la verificación de pruebas?
Sí y no. Si te interesan las matemáticas reales y serias, entonces no hay alternativa a HOL o a su equivalente moral (como la teoría de tipos dependientes o la teoría de conjuntos) porque las matemáticas tratan intrínsecamente con conceptos de orden superior.
Sin embargo, grandes partes de cualquier desarrollo no implican argumentos lógica o conceptualmente complejos: son sólo gestión de símbolos, que a menudo implican teorías decidibles. Esto suele ser automatizable, si los problemas en cuestión no se plantean en un lenguaje de orden superior. (A veces, como en el caso de la conjetura de Kepler, hay una forma artificial de plantear el problema en una teoría simple. Ésta es esencialmente la razón por la que la prueba de Hales depende tanto de los ordenadores: redujo muy cuidadosamente la conjetura de Kepler a una colección de enunciados comprobables por máquina sobre campos cerrados reales).
- ¿Cuáles son las limitaciones y deficiencias de los actuales sistemas de verificación de pruebas?
La principal dificultad de estas herramientas es encontrar el equilibrio adecuado entre automatización y abstracción. Básicamente, cuanto más expresiva sea la lógica, más difícil será la búsqueda automatizada de pruebas, y más fácil y natural será definir teorías abstractas que puedan utilizarse en muchos contextos diferentes.
