Banco de dados de declarações e provas FOL

Question

Existe um banco de dados em algum lugar de declarações FOL simples, com suas provas escritas em um sistema de dedução ao estilo de Hilbert, ou talvez uma ferramenta para pegar essas declarações e produzir provas? Embora eu veja imediatamente como codificar * declarações * arbitrárias no FOL, tive meses de dificuldade em tentar entender como as * provas * formais se relacionam com as provas intuitivas que conheço por fazer matemática comum. Acho que ver provas formais de afirmações óbvias como \ begin {equation *} (\ forall x \ forall y \; P (x, y)) \ rightarrow (\ forall y \ forall x \; P (x, y)) \ end {equation *} e \ begin {equation *} (\ forall x \ forall y \; P (x, y)) \ rightarrow (\ forall x \; P (x, x)) \ end {equation *} pode finalmente me descolar.

Answer 1

Há um gerador de árvore de prova feito por Wolfgang Schwarz que leva afirmações arbitrárias em algumas lógicas diferentes (lógica de primeira ordem, lógica modal, lógica proposicional) e fornece uma prova de que elas são tautologias, contingentes, sempre falsas, afirmações válidas e assim por diante automaticamente.

https://www.umsu.de/trees/

A única desvantagem é que ele usa um método de árvore de prova em vez do estilo Hilbert que você mencionou. Esperançosamente, outra resposta pode fornecer um link para esse gerador de provas.

Aqui estão as provas de seus dois exemplos ( 1 , 2 ).

Answer 2

Você pode querer dar uma olhada em Metamath (http://metamath.org), especificamente a Parte 1 Lógica de Primeira Ordem Clássica com Igualdade do Explorador de Provas de Metamatização .

Uma prova para seu primeiro exemplo é ax11w .

Este provavelmente não é o tipo exato de prova que você está pedindo, mas essas provas foram úteis para outros no passado, para entender a lógica e as provas.