Comprender la integridad sintáctica

Question

Un sistema formal es sintácticamente completo si para cada frase (fórmula cerrada) $\varphi$ o bien $\varphi$ o $\lnot \varphi$ es demostrable.

Un sistema formal es semánticamente completo si cada frase (fórmula cerrada) $\varphi$ que es una tautología es demostrable.

Lo que me pregunto es

1. El primer teorema de incompletitud de Godel afirma que existe una sentencia $\varphi$ en la aritmética de Peano que es verdadera, pero que no es demostrable y cuya negación no es demostrable, por lo que es al mismo tiempo teorema de incompletitud sintáctica y semántica, ¿verdad? ¿Es correcto decir que la incompletitud semántica es el resultado más esencial, ya que implica la incompletitud sintáctica bajo el supuesto de solidez?

2. Considere la fórmula $P$ en el cálculo proposicional donde $P$ es una variable proposicional de la firma. Es sintácticamente incompleta ya que ni $P$ ni $\lnot P$ no es una tautología, y por la completitud semántica del cálculo proposicional, podemos concluir que ni $P$ ni $\lnot P$ son deducibles. Sin embargo, ¿hay alguna manera de demostrar que ninguno de ellos es deducible sintácticamente, sin el argumento semántico?

3. ¿Existen ejemplos de sistemas formales sintácticos completos útiles?

Answer 1

En (1). En una terminología más estándar:

A teoría formal es [negación] completa si para cada sentencia (fórmula cerrada) φ es demostrable φ o ¬φ.

Una lógica sistema deductivo es semánticamente completo si cada frase (fórmula cerrada) φ del sistema que es una verdad lógica es demostrable.

El teorema de incompletitud de Gödel muestra que la Aritmética de Peano de primer orden no es completa en cuanto a la negación. (Y trivialmente, ya que uno de los dos φ o ¬φ es verdadero en la interpretación estándar, hay una verdad que PA no puede demostrar).

Pero el sistema deductivo de primer orden incorporado en PA sigue siendo semánticamente completo (¡por el teorema de completitud de Gödel!).

Era/es importante que el resultado oficial de incompletitud de Gödel sea puramente sintáctico, demostrado en supuestos puramente sintácticos. Para recordar el contexto en torno a 1930. Las nociones semánticas (antes de Tarski) se consideraban en general turbias y "no científicas"; y el principal programa de investigación en fundamentos en el entorno de Gödel era el programa hilbertiano, que presupone que podemos axiomatizar por completo franjas de las matemáticas. Por lo tanto, demostrar que los hilbertianos tendrían que comprar que ni siquiera podemos obtener una teoría completa de la aritmética elemental fue devastador.