¿Existe una relación entre la duración de la condena y la duración de la prueba?

Question

Mi pregunta básica es: "¿Las tautologías más largas tardan más en demostrarse?" Pero obviamente esto está infradeterminado. Si se permite una regla de inferencia "Implicación Tautológica" entonces cualquier tautología tiene una prueba de 1 línea.

Pero digamos que estamos trabajando en la deducción natural, ¿es cierto que las tautologías más largas (tautologías con más letras y conectivas en ellas) requieren más pasos de prueba?

Pero esta pregunta sigue sin ser lo suficientemente buena, ya que podemos añadir pasos superfluos a una prueba y seguir demostrando el resultado. Así que la pregunta es:

En la deducción natural, ¿la prueba más corta de una tautología está relacionada con su longitud? O quizás: ¿una tautología más corta admite siempre una prueba más corta?

¿Y qué solidez tiene este resultado en diferentes conjuntos de conectivos/reglas de inferencia?

Answer 1

¿una tautología más corta admite siempre una prueba más corta?

parece que debería haber una tautología cuyo enunciado es más largo que el último teorema de fermats pero cuya prueba más corta es más corta

Answer 2

Supongamos que $\phi$ es cualquier frase de la forma $\lnot (\psi \land \lnot \psi)$ . Entonces hay un patrón para una prueba muy corta de $\phi$ que funciona para cualquier fórmula $\psi$ . No puedo formatearla aquí, pero la idea es obtener $\bot$ de $\psi \land \lnot \psi$ en un número fijo de pasos, y luego aplicar la regla de la prueba por contradicción para obtener $\phi$ . La contradicción original tendrá tres pasos en la deducción natural: dos son de eliminación de la conjunción y el tercero deriva $\bot$ . Así que todo el patrón de prueba tiene cuatro pasos en la deducción natural, independientemente de $\psi$ . Si se ajusta la configuración para la deducción natural, el número de pasos puede subir a cinco o seis, pero será constante en cualquier caso.

No estoy seguro de que exista un sistema en el que las tautologías más largas requieran siempre pruebas más largas y en el que la longitud se mida en pasos de prueba. Ciertamente tendría que tener versiones modificadas de las reglas relativas a $\bot$ .

Una forma de cambiar la cuestión es cambiar la forma de medir la longitud de una prueba. Si el tamaño de la prueba es el número total de símbolos, es evidente que los hechos más largos requieren pruebas más largas.

Answer 3

El tamaño de las pruebas no guarda casi ninguna relación con el tamaño de las afirmaciones que demuestran (en el peor de los casos).

Límite inferior: tamaño constante

El tamaño de la prueba más pequeña para declaraciones de tamaño N es constante. Basta con que las afirmaciones sean de la forma "Verdadero o S". (A menos que cuente la declaración de entrada como parte del tamaño, en cuyo caso es lineal).

Límite superior: tamaño incomputable

El tamaño de la prueba más grande que demuestre un enunciado de tamaño inferior a N crece tan rápido que no es computable a partir de N.

Prueba

Considere el tamaño de una prueba de que una máquina de Turing no se detiene en S pasos. Algunas máquinas de Turing funcionan eternamente pero no se puede demostrar que funcionen eternamente. Supongamos que tenemos una máquina de este tipo M. Probar que M no se detiene antes de S pasos debe tomar más pasos a medida que S crece. De lo contrario, tenemos una prueba para todo S y nos hemos contradicho.

Llamemos a esa función de número de pasos al tamaño de la prueba G. Voy a hacer una suposición, que es que hay una función computable G' tal que G(G'(X)) >= X.

Suponga que tiene alguna función computable F que afirma que es un límite superior asintótico en los tamaños de las pruebas dado el tamaño de los estados. Entonces simplemente genero una secuencia de declaraciones donde la Nª declaración es "M no se detiene dentro de los pasos de G'(N*F(N))". Las afirmaciones son todas demostrables (en el peor de los casos: simular M en la prueba; por eso asumí que G' es computable) y crecen en tamaño logarítmicamente. Pero los tamaños de las pruebas crecen asintóticamente más rápido que F, que es exponencialmente más rápido que F con respecto a los tamaños de las declaraciones. Así que F no es realmente un límite superior asintótico.

Por lo tanto, ninguna función computable es un límite superior asintótico del tamaño de la prueba dado el tamaño del enunciado, lo que significa que el límite superior es incomputable.

Answer 4

Esta cuestión es uno de los principales temas estudiados en complejidad de la prueba . La medida a la que se refiere se llama número de pasos en la prueba o la longitud de la prueba.

El tamaño de una tautología está relacionado con el número de pasos de su prueba más corta, pero esto no significa que el número de pasos sea una función monótona del tamaño de la tautología. Como han mencionado otros, la longitud de una tautología larga puede ser muy corta. No es difícil encontrar tautologías largas arbitrarias que tengan pruebas con un número de pasos constante (es decir, independiente del tamaño de la tautología).

Por otra parte, la tarea de elaborar tautologías con un gran número de pasos no es obvia y está abierta para muchos sistemas de pruebas proposicionales. Obsérvese que se deduce del teorema (constructivo) de la demostración de la exhaustividad que toda tautología de tamaño $s$ tiene una prueba de altura $O(s)$ con $O(2^s)$ pasos y tamaño $O(s2^s)$ .

Tenemos algunos límites inferiores muy débiles para el número máximo de pasos necesarios para una tautología de tamaño $s$ y la cuestión de que este límite superior sea ajustado está muy abierta para el cálculo secuencial y también para la deducción natural, que son esencialmente equivalentes a los sistemas de prueba de estilo Hilbert. El límite es estrecho si eliminamos la regla de corte del cálculo secuencial, es decir, hay tautologías que requieren un número exponencial de pasos.

Puede encontrar más información sobre la relación entre las diferentes medidas estudiadas en la complejidad de las pruebas y la relación entre los diferentes sistemas de pruebas proposicionales consultando encuestas/libros sobre el tema.

Para la lógica de primer orden, hay que tener en cuenta que la lógica de primer orden es indecidible, es decir, dada una fórmula no hay ningún algoritmo para comprobar si es una fórmula válida. Cualquier límite superior computable en el tamaño de la prueba daría un algoritmo para decidir la lógica de primer orden, comprobar todas las pruebas posibles hasta ese tamaño. (Obsérvese que un límite superior en la longitud de la prueba en la deducción natural/el cálculo secuencial dará un límite superior en el tamaño debido a la normalización/eliminación de cortes). Dado que no existe tal algoritmo, no puede haber ninguna cota superior computable.