Base de datos de declaraciones FOL y pruebas
¿Existe una base de datos en alguna parte de declaraciones FOL simples, con sus pruebas escritas en un sistema de deducción al estilo de Hilbert, o quizás una herramienta para tomar tales declaraciones y producir pruebas? Si bien veo inmediatamente cómo codificar * declaraciones * arbitrarias en FOL, he tenido meses de problemas tratando de entender cómo las * pruebas * formales se relacionan con las pruebas intuitivas que conozco al hacer matemáticas ordinarias. Creo que ver pruebas formales de afirmaciones obvias como \ begin {ecuación *} (\ forall x \ forall y \; P (x, y)) \ rightarrow (\ forall y \ forall x \; P (x, y)) \ final {ecuación *} y \ begin {ecuación *} (\ forall x \ forall y \; P (x, y)) \ rightarrow (\ forall x \; P (x, x)) \ end {ecuación *} podrían finalmente consigue que me despegue.
Respuestas
Existe un generador de árboles de prueba hecho por Wolfgang Schwarz que toma declaraciones arbitrarias en algunas lógicas diferentes (lógica de primer orden, lógica modal, lógica proposicional) y proporciona una prueba de que son tautologías, contingentes, siempre falsas, declaraciones válidas, etc. automáticamente.
https://www.umsu.de/trees/
La única desventaja es que utiliza un método de árbol de prueba en lugar del estilo de Hilbert que mencionaste. Con suerte, otra respuesta puede proporcionar un enlace a dicho generador de pruebas.
Aquí están las pruebas de sus dos ejemplos ( 1 , 2 ).
Es posible que desee echar un vistazo a Metamath (http://metamath.org), específicamente la Parte 1 Lógica clásica de primer orden con la igualdad del Explorador de pruebas de Metamath .
Una prueba de su primer ejemplo es ax11w .
Probablemente este no sea el tipo exacto de prueba que está pidiendo, pero estas pruebas han sido útiles para otros en el pasado, para comprender la lógica y las pruebas.