Condiciones de demostrabilidad de Hilbert-Bernays

En lógica matemática , las condiciones de demostrabilidad de Hilbert-Bernays , llamadas así en honor a David Hilbert y Paul Bernays , son un conjunto de requisitos para predicados de demostrabilidad formalizados en teorías formales de aritmética (Smith 2007:224).

Estas condiciones se utilizan en muchas demostraciones del segundo teorema de incompletitud de Kurt Gödel y también están estrechamente relacionadas con los axiomas de la lógica de demostrabilidad .

Sea T una teoría formal de la aritmética con un predicado de demostrabilidad formalizado Prov( n ) , que se expresa como una fórmula de T con una variable numérica libre. Para cada fórmula φ en la teoría, sea #(φ) el número de Gödel de φ . Las condiciones de demostrabilidad de Hilbert-Bernays son:

1. Si T prueba una oración φ entonces T prueba Prov(#(φ)) .
2. Para cada oración φ , T demuestra Prov(#(φ)) → Prov(#(Prov(#(φ))))
3. T demuestra que Prov(#(φ → ψ)) y Prov(#(φ)) implican Prov(#(ψ))

Obsérvese que Prov es un predicado de números y es un predicado de demostrabilidad en el sentido de que la interpretación pretendida de Prov(#(φ)) es que existe un número que codifica una demostración de φ . Formalmente, lo que se requiere de Prov son las tres condiciones anteriores.

En la notación más concisa de la lógica de demostrabilidad , denotando " prueba " y denotando :${\displaystyle T\vdash \varphi}$${\estilo de visualización T}$${\estilo de visualización \varphi}$${\displaystyle \Cuadro \varphi}$${\displaystyle {\text{Prov}}(\#(\varphi ))}$

1. ${\displaystyle (T\vdash \varphi )\to (T\vdash \Box \varphi )}$
2. ${\displaystyle T\vdash (\Box \phi \to \Box \Box \phi )}$
3. ${\displaystyle T\vdash (\Box (\varphi \to \psi )\to \Box \varphi \to \Box \psi )}$

Las condiciones de demostrabilidad de Hilbert-Bernays, combinadas con el lema de la diagonal , permiten demostrar en poco tiempo ambos teoremas de incompletitud de Gödel. De hecho, el principal esfuerzo de las demostraciones de Gödel consistió en demostrar que estas condiciones (o equivalentes) y el lema de la diagonal se cumplen para la aritmética de Peano; una vez que se establecen, la demostración se puede formalizar fácilmente.

Utilizando el lema diagonal, existe una fórmula tal que .${\estilo de visualización \rho}$${\displaystyle T\Vdash \rho \leftrightarrow \neg Prov(\#(\rho ))}$

Para el primer teorema sólo se necesitan la primera y la tercera condición.

La condición de que T es ω-consistente se generaliza por la condición de que si para cada fórmula φ , si T prueba Prov(#(φ)) , entonces T prueba φ . Nótese que esto de hecho es válido para una T ω -consistente porque Prov(#(φ)) significa que hay una codificación numérica para la prueba de φ , y si T es ω -consistente entonces al recorrer todos los números naturales uno puede realmente encontrar un número particular a , y luego uno puede usar a para construir una prueba real de φ en T .

Supongamos que T hubiera podido demostrar . Entonces tendríamos los siguientes teoremas en T :${\estilo de visualización \rho}$

1. ${\displaystyle T\Vdash \rho}$
2. ${\displaystyle T\Vdash \neg Prov(\#(\rho ))}$(por construcción del teorema 1)${\estilo de visualización \rho}$
3. ${\displaystyle T\Vdash Prov(\#(\rho ))}$(por la condición nº 1 y el teorema 1)

Por lo tanto, T prueba tanto como . Pero si T es consistente, esto es imposible y nos vemos obligados a concluir que T no prueba .${\displaystyle Prov(\#(\rho ))}$${\displaystyle \neg Prov(\#(\rho ))}$${\estilo de visualización \rho}$

Supongamos ahora que T hubiera podido demostrar . Entonces tendríamos los siguientes teoremas en T :${\displaystyle \neg \rho}$

1. ${\displaystyle T\Vdash\neg\rho}$
2. ${\displaystyle T\Vdash Prov(\#(\rho ))}$(por construcción del teorema 1)${\estilo de visualización \rho}$
3. ${\displaystyle T\Vdash \rho}$(por ω-consistencia)

Por lo tanto, T prueba tanto como . Pero si T es consistente, esto es imposible y nos vemos obligados a concluir que T no prueba .${\estilo de visualización \rho}$${\displaystyle \neg \rho}$${\displaystyle \neg \rho}$

Para concluir, T no puede probar ni .${\estilo de visualización \rho}$${\displaystyle \neg \rho}$

Usando el truco de Rosser , no es necesario asumir que T es ω -consistente. Sin embargo, sería necesario demostrar que la primera y tercera condiciones de demostrabilidad se cumplen para Prov ^R , el predicado de demostrabilidad de Rosser, en lugar de para el predicado de demostrabilidad ingenuo Prov. Esto se deduce del hecho de que para cada fórmula φ , Prov(#(φ)) se cumple si y solo si Prov ^R se cumple.

Una condición adicional utilizada es que T demuestra que Prov ^R (#(φ)) implica ¬Prov ^R (#(¬φ)) . Esta condición se cumple para cada T que incluye lógica y aritmética muy básica (como se explica en el truco de Rosser #La oración de Rosser ).

Usando el truco de Rosser, ρ se define usando el predicado de demostrabilidad de Rosser, en lugar del predicado de demostrabilidad ingenuo. La primera parte de la prueba permanece sin cambios, excepto que el predicado de demostrabilidad se reemplaza allí también por el predicado de demostrabilidad de Rosser.

La segunda parte de la prueba ya no utiliza la consistencia ω y se modifica de la siguiente manera:

Supongamos que T hubiera podido demostrar . Entonces tendríamos los siguientes teoremas en T :${\displaystyle \neg \rho}$

1. ${\displaystyle T\Vdash\neg\rho}$
2. ${\displaystyle T\Vdash Prov^{R}(\#(\rho ))}$(por construcción del teorema 1)${\estilo de visualización \rho}$
3. ${\displaystyle T\Vdash \neg Prov^{R}(\#(\neg \rho ))}$(por el teorema 2 y la condición adicional que sigue a la definición del predicado de demostrabilidad de Rosser)
4. ${\displaystyle T\Vdash Prov^{R}(\#(\neg \rho ))}$(por la condición nº 1 y el teorema 1)

Por lo tanto, T prueba tanto como . Pero si T es consistente, esto es imposible y nos vemos obligados a concluir que T no prueba .${\displaystyle Prov^{R}(\#(\neg \rho ))}$${\displaystyle \neg Prov^{R}(\#(\neg \rho ))}$${\displaystyle \neg \rho}$

Suponemos que T demuestra su propia consistencia, es decir que:

${\displaystyle T\Vdash \neg Prov(\#(1=0))}$.

Para cada fórmula φ :

${\displaystyle T\Vdash\neg\varphi\rightarrow (\varphi\rightarrow (1=0))}$(por eliminación de negación )

Es posible demostrar mediante la aplicación de la condición n.° 1 del último teorema, seguida del uso repetido de la condición n.° 3, que:

${\displaystyle T\Vdash Prov(\#(\neg \varphi ))\rightarrow (Prov(\#(\varphi ))\rightarrow Prov(\#(1=0)))}$

Y usando T para probar su propia consistencia se deduce que:

${\displaystyle T\Vdash Prov(\#(\neg \varphi ))\rightarrow \neg Prov(\#(\varphi ))}$

Ahora usamos esto para demostrar que T no es consistente:

1. ${\displaystyle T\Vdash Prov(\#(\neg Prov(\#(\rho )))\rightarrow \neg Prov(\#(Prov(\#(\rho )))}$(después de T demuestra su propia consistencia, con )${\displaystyle \varphi =Prov(\#(\rho ))}$
2. ${\displaystyle T\Vdash\rho\rightarrow\neg ​​Prov(\#(\rho ))}$(por construcción de )${\estilo de visualización \rho}$
3. ${\displaystyle T\Vdash Prov(\#(\rho \rightarrow \neg Prov(\#(\rho )))}$(por la condición nº 1 y el teorema 2)
4. ${\displaystyle T\Vdash Prov(\#(\rho ))\rightarrow Prov(\#(\neg Prov(\#(\rho )))}$(por la condición nº 3 y el teorema 3)
5. ${\displaystyle T\Vdash Prov(\#(\rho ))\rightarrow \neg Prov(\#(Prov(\#(\rho )))}$(por los teoremas 1 y 4)
6. ${\displaystyle T\Vdash Prov(\#(\rho ))\rightarrow Prov(\#(Prov(\#(\rho )))}$(por condición n°2)
7. ${\displaystyle T\Vdash \neg Prov(\#(\rho ))}$(por los teoremas 5 y 6)
8. ${\displaystyle T\Vdash \neg Prov(\#(\rho ))\rightarrow \rho }$(por construcción de )${\estilo de visualización \rho}$
9. ${\displaystyle T\Vdash \rho}$(por los teoremas 7 y 8)
10. ${\displaystyle T\Vdash Prov(\#(\rho ))}$(por la condición 1 y el teorema 9)

Por lo tanto, T prueba tanto como , por lo tanto, T es inconsistente.${\displaystyle Prov(\#(\rho ))}$${\displaystyle \neg Prov(\#(\rho ))}$

• Smith, Peter (2007). Introducción a los teoremas de incompletitud de Gödel . Cambridge University Press. ISBN  978-0-521-67453-9