¿Cuál es la relación entre el cálculo lambda simplemente escrito y la lógica de orden superior?
Bajo Curry-Howard parece que el cálculo lambda simplemente escrito corresponde a la lógica proposicional. ¿Cómo se relaciona con la lógica de orden superior? Según este tutorial de Geuvers: http://typessummerschool07.cs.unibo.it/courses/geuvers-1.pdf, el lenguaje de HOL parece ser STT. ¿No debería ser PROP? Qué significa eso?
¿Tenía Church en mente HOL cuando definió STT?
Respuestas:
La distinción es esta: si STLC se toma como un lenguaje primitivo en los constructores de adición de nivel de tipo y un pequeño número de axiomas es suficiente para darle el poder expresivo completo de HOL.
fuente