Hice la misma pregunta en Mathoverflow a la que respondió Andrej Bauer:
Las propiedades indeseables de la lógica de orden superior se deben a una noción insuficiente de modelo. Es decir, no podemos tener las tres, solidez, completitud y efectividad (decidibilidad de la comprobación de pruebas), si insistimos en que las fórmulas se interpreten de la manera "estándar" de la teoría de conjuntos. La semántica de Henkin no sufre esta deficiencia.
Lo que esto dice no es que algo vaya mal con la lógica de orden superior, sino que algo va mal con aquellos que se niegan a mirar los modelos semánticos, incluso cuando los tienen delante de sus narices, porque estos modelos son "involuntarios", "filosóficamente inaceptables", "no son lo que piensan los matemáticos", etc. Este fenómeno de negarse a aceptar nuevas interpretaciones de viejas teorías es bastante persistente, y siempre muy perjudicial. ¿No paralizó alguien el progreso de la geometría no euclidiana porque era impensable que hubiera nuevos modelos extraños? ¿No se llaman así los números imaginarios porque eran impensables y no "existían realmente"? ¿No sufre la lógica clásica de orden superior porque se le niega su noción natural de modelos alegando que no son estándar?
La noción natural de modelo para la lógica intuicionista de orden superior (IHOL) es la de topos. Con respecto a la semántica de topos, es un resultado estándar que IHOL goza de solidez, completitud y efectividad.
Podemos especializar este hecho estándar a la lógica clásica de orden superior (CHOL). El resultado es que, con respecto a la semántica de topos booleanos, CHOL goza de solidez, completitud y validez. A partir de aquí, podemos demostrar varios teoremas técnicos que nos permiten reducir la clase de topos booleanos que son suficientes para la completitud. Y entonces no es de extrañar que no podamos reducirnos a un único topos conocido como conjuntos clásicos, al que sus prisioneros llaman "Paraíso".
