Dada una lógica de primer orden de teoría de la $T$ y una fórmula $F$, supongamos que tengo semánticamente demostrado que $T\vdash F$. Que es, me han demostrado que cualquier modelo de $M$ de $T$ satisface $F$ y concluyo por Gödel integridad del teorema.
Tengo un algoritmo general para extraer de la anterior sintáctico prueba de $T\vdash F$, es decir, una secuencia finita de fórmulas que respeta las reglas de inferencia, usa $T$ y termina a las $F$ ?
Si no existe tal algoritmo, entonces ¿realmente demostrar $T\vdash F$ ? El teorema de completitud fue sólo un ejemplo de cómo indirectamente demostrar que no existe una prueba de $T\vdash F$, sin explícitamente dando esta última prueba. ¿Qué pasa si mi prueba indirecta utiliza un cardinal inaccesible, tengo que mencionar el torpe $$ (\text{ZFC + Inaccessible cardinal})\; \vdash\; (T \vdash F) $$ Y, a continuación, esta prueba también puede ser indirecta, por lo que podría continuar el apilamiento de las teorías a la izquierda y se convierte en una pesadilla. No semántica o indirecta pruebas algo derrota el propósito de la lógica formal, que debemos estar absolutamente seguros de que las pruebas existen y son correctos?
