Búsqueda sistemática de contraejemplos por fuerza bruta

Question

Este no llega a ninguna parte en math.stackexchange.com, así que lo pongo aquí.

El teorema de completitud de Gödel dice que para cada afirmación en el cálculo de predicados de primer orden con igualdad, hay una prueba de que se cumple en todas las estructuras, o un contraejemplo --- una estructura en la que no se cumple. Lo que parece que no se enfatiza lo suficiente es la conexión con la computabilidad: hay un algoritmo eficiente de comprobación de pruebas. Sin eso, la conclusión tendría mucho menos interés del que tiene. (Sobre todo porque se podría declarar que toda fórmula universalmente válida es una prueba de sí misma. Entonces uno no tendría absolutamente ninguna manera de saber qué es una prueba válida y qué no lo es, pero la conclusión del teorema seguiría siendo cierta).

Otro teorema descubierto en los años 30 es que, aunque hay un algoritmo de comprobación de pruebas para esta situación, sólo hay la mitad de un algoritmo de búsqueda de pruebas:

• Uno puede buscar sistemáticamente una prueba de tal manera que si existe, la encontrará.
• Pero después de un trillón de años de búsqueda sin éxito, no hay manera de saber que no aparecerá diez minutos después, ni que lo hará.

Ambos de las viñetas fueron probadas en los años 30. (¿Es el "teorema de Church" el nombre convencional para la conjunción de los dos puntos con viñetas, o sólo el segundo, o qué? Ahora mismo no estoy seguro).

Creo que hay una amplia literatura sobre la eficiencia computacional (¿o la falta de eficiencia?) de estas búsquedas de pruebas. ¿Existe bibliografía sobre la búsqueda sistemática de contraejemplos por fuerza bruta? Estos contraejemplos serían estructuras en las que una sentencia de primer orden propuesta es falsa.

Answer 1

Alg enumera los modelos finitos de las teorías de primer orden de orden simple. Obviamente, puede encontrar contraejemplos, ya que sólo hay que añadir la negación del enunciado que queremos violar. Mi experiencia con este tipo de cosas es que básicamente equivale a resolver un problema de satisfabilidad, por lo que toda la teoría sobre los solucionadores SAT podría ser relevante aquí.

Para el problema general de encontrar un contramodelo (posiblemente infinito) no tengo nada inteligente que decir. Pues yo sí. Para hablar de computabilidad, primero tenemos que especificar qué significa para un ordenador "encontrar" un modelo infinito. Esto lleva a la cuestión de cómo representar modelos infinitos, y en ese punto estás haciendo teoría de modelos efectivos.

Answer 2

Las pruebas son objetos finitos, por lo que se pueden buscar pruebas de forma sistemática.

Los contraejemplos pueden ser modelos infinitos, por lo que no se pueden buscar de la misma manera.

Por lo tanto, un resultado positivo completo parece poco probable.

Ejemplo 1: ¿Son los axiomas de la aritmética de Peano consistentes con el conjunto infinito de sentencias $\exists x. n=Sx, \exists x. n=SSx, \exists x. n=SSSx, \ldots$ ? No se puede derivar una contradicción de ellos, pero tampoco se encontrará un contraejemplo por búsqueda porque los modelos no estándar de la aritmética de Peano no son recursivos.

Ejemplo 2: Lerman y Schmerl han propuesto una frase $\phi$ en la teoría de los árboles sin modelos recursivos. Así que los contraejemplos a $\phi\rightarrow\psi$ tampoco aparecerá en ningún tipo de búsqueda ordinaria.

Answer 3

Esto es algo tangencial a su consulta específica, pero quizás no sea del todo irrelevante. Ha habido un progreso considerable en el subdominio de los teoremas de geometría, algunos de cuyos probadores proceden a buscar y eliminar posibles contraejemplos. No soy un experto, pero permítanme citar tres referencias, separadas por cerca de una década cada una, para indicar el progreso continuo en esta subárea:

1988 : Chou, Shang-Ching. Demostración de teoremas de geometría mecánica . Vol. 41. Springer, 1988. ( Enlace de Springer )
   
    _{p.109: Cinco líneas de Gauss son concurrentes: Un "teorema posiblemente nuevo" [en 1988].}

2001 : Jacques Fleuriot. "Demostración de teoremas de geometría". 2001, pp 11-30. Un estudio. ( Enlace de Springer )

2011 : Stojanović, Sana, Vesna Pavlović y Predrag Janičić. "Un prover de teoremas geométricos basado en la lógica coherente capaz de producir pruebas formales y legibles". Deducción automática en geometría . Springer Berlin Heidelberg, 2011. 201-220. ( Enlace de Springer )

   
       _{Charla de Ulrik Buchholtz <a href="http://math.stanford.edu/~utb/slides.pdf" rel="nofollow noreferrer">descarga de diapositivas en PDF </a>, 2010.}