¿Existen lógicas no triviales que exiban solidez y completitud que no sean de primer orden?

Question

En nuestra clase de lógica, acabamos de completar las pruebas de solidez y completitud. Para mí, estas pruebas dependen de que los modelos se filtren a través de la lógica de primer orden.

Por ejemplo, podría establecer un sistema formal trivial, con un solo wff. Digamos que es "sí".

Para la solidez, defino un mapeo de cualquier modelo a "sí".

Para completar, si se da "sí", devuelvo un modelo que exhibe "sí", así que devuelva su modelo favorito (números naturales con menos entonces?).

¿Existen sistemas formales no triviales que tengan solidez y completitud?

(Como siempre, disculpas si es una pregunta tonta)

Answer 1

Henkin demostró que la lógica de orden superior conocida como teoría de tipos simple de Church es sólida y completa para lo que ahora se denominan modelos de Henkin. El artículo de Henkin Completitud en la teoría de los tipos no es muy largo y es muy legible (una vez que se sabe que Church y Henkin escriben $\alpha\beta$ para el tipo de funciones del tipo $\beta$ para escribir $\alpha$ , que ahora escribiríamos como $\alpha \rightarrow \beta$ ).

Sorprendentemente, debido a que la lógica de orden superior es mucho más expresiva que la lógica de primer orden, la prueba de completitud de Henkin es en muchos aspectos mucho más simple que la prueba de completitud para la lógica de primer orden.