Completitud / solidez de la lógica de segundo orden

Bosquejo de la prueba

1) Definimos la sintaxis para SOL y el aparato deductivo correspondiente, agregando axiomas y reglas para administrar la cuantificación de segundo orden (ver, por ejemplo , van Dalen, Logic and Structure (2013), Ch.5 ).

2) Definimos la semántica "estándar" para el lenguaje.

3) Definimos el concepto de validez estándar extendiendo de forma natural el concepto FOL.

Entonces probamos el:

Teorema de solidez : todos los teoremas del cálculo de predicados de segundo orden son estándarmente válidos.

4) Consideramos la versión FOL de los axiomas de Peano más el Axioma de inducción ; es importante señalar que, en la versión SOL, la Inducción es una fórmula y no un esquema axiomático .

5) Sea AR2 la conjunción de los axiomas de primer orden de la aritmética formal más el axioma de segundo orden de la inducción matemática.

Probamos que:

Cualesquiera dos interpretaciones estándar M y M' que sean modelos de AR2 son isomorfas .

6) Sea L2A el lenguaje de segundo orden para la aritmética (con las constantes no lógicas de la aritmética formal: cero, sucesor, suma, multiplicación).

Sea N la interpretación estándar de L2A con el conjunto de números naturales como su dominio y las interpretaciones usuales de las constantes no lógicas.

Probamos (usando 5) que:

Sea B cualquier fórmula del lenguaje de la aritmética. Entonces B es verdadero en N si y sólo si AR2 ⇒ B es estándarmente válido .

7) Probamos que:

El conjunto SV de fórmulas estándar válidas de L2A no es efectivamente enumerable.

Suponga que SV es efectivamente enumerable. Entonces, por 6, podríamos efectivamente enumerar el conjunto TR de todas las fórmulas verdaderas de la aritmética de primer orden recorriendo SV , encontrando todas las fórmulas de la forma AR2 ⇒ B , donde B es una fórmula de la aritmética de primer orden, y enumerando aquellas fórmulas B. _ Entonces la teoría TR sería decidible (que no lo es), ya que, para cualquier fórmula cerrada C , podríamos enumerar efectivamente TR hasta que aparezca C o su negación.

8) De 7 tenemos que el conjunto de todas las fórmulas estándar válidas no es efectivamente enumerable.

Una enumeración de todas las fórmulas estándar válidas produciría una enumeración de todas las fórmulas estándar válidas de L2A , ya que el conjunto de fórmulas de L2A es decidible.

9) No existe un sistema formal efectivo cuyos teoremas sean las fórmulas estándar válidas de L2A .

Si existiera tal sistema de axiomas, podríamos enumerar las fórmulas estándar válidas de L2A , contradiciendo 7.

10) Incompletitud de la semántica estándar : no existe un sistema formal efectivo cuyos teoremas sean todos fórmulas estándar válidas.

Si existiera tal sistema de axiomas, podríamos enumerar el conjunto de todas las fórmulas estándar válidas, contradiciendo 8.

El último hecho distingue claramente la lógica de segundo orden de la lógica de primer orden, ya que el teorema de completitud de Gödel nos dice que existe un sistema formal efectivo cuyos teoremas son todos fórmulas de primer orden lógicamente válidas.

Es una prueba complicada.

Supongamos que tenemos cálculo de predicados de primer orden y aritmética básica. Podemos codificar declaraciones lógicas numéricamente. (Toda esta publicación está representada por una cadena de bits cuando alguien la lee, por ejemplo). Ahora, suponiendo que tenemos un sistema lógico rígido, con axiomas y reglas de derivación, podemos probar algunas proposiciones y podemos probar que algunos no se puede probar Por ejemplo, dados axiomas razonables y reglas de derivación, se puede demostrar que "3 es primo", pero que "3 es compuesto" no se puede demostrar. Tenemos tres clases de proposiciones: las que podemos demostrar que son verdaderas, las que podemos demostrar que son falsas y las que aún no podemos demostrar de ninguna manera.

Ahora, si se imaginan un montaje de pizarrones y charlas de alguien que es mejor en lógica formal que yo....

La demostrabilidad es una relación numérica. Es posible expresar numéricamente si una proposición puede ser demostrada. La demostrabilidad es, por tanto, una relación numérica, y podemos expresar esa relación en una proposición, que podemos convertir en un número inimaginablemente grande, que también podemos llamar N. También podemos crear un número U que representa el complemento de la demostrabilidad.

Dada U, podemos construir un número P. (Imagina que se nos ocurre mientras vas al baño, ya que no recuerdo los detalles). Cuando decodificamos P, leemos que la proposición P no es demostrable.

Ahora, hay dos posibilidades. P podría ser verdadera, en cuyo caso tenemos una declaración verdadera que no se puede probar, por lo que el sistema lógico está incompleto. Podría ser falsa, en cuyo caso es demostrable, y podemos probar una proposición falsa, por lo que el sistema lógico es inconsistente.

Ahora, podemos agregar reglas para arreglar esto, de modo que P sea demostrablemente verdadero o demostrablemente falso. En ese momento, hemos cambiado lo que es la demostrabilidad, por lo que se nos ocurre un número N1 mucho más grande e inimaginablemente grande, y luego obtenemos U1 y obtenemos un nuevo P1, que dice "La Proposición P1 es improbable incluso con nuestras nuevas reglas". , y estamos de vuelta donde empezamos.