Database di dichiarazioni e prove FOL

Question

Esiste un database da qualche parte di semplici affermazioni FOL, con le loro dimostrazioni scritte in un sistema di deduzione in stile Hilbert, o forse uno strumento per prendere tali affermazioni e produrre dimostrazioni? Mentre vedo immediatamente come codificare * affermazioni * arbitrarie in FOL, ho avuto mesi di difficoltà nel cercare di capire come le * dimostrazioni * formali si relazionano alle dimostrazioni intuitive che conosco facendo matematica ordinaria. Penso di vedere prove formali di affermazioni ovvie come \ 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 *} potrebbe finalmente mi sblocca.

Answer 1

Esiste un generatore di albero delle prove realizzato da Wolfgang Schwarz che accetta affermazioni arbitrarie in poche logiche diverse (logica del primo ordine, logica modale, logica proposizionale) e fornisce una prova che sono tautologie, contingenti, sempre false, affermazioni valide e così via automaticamente.

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

L'unico svantaggio è che utilizza un metodo dell'albero della prova invece dello stile di Hilbert che hai menzionato. Si spera che un'altra risposta possa fornire un collegamento a un tale generatore di prove.

Ecco le prove dei tuoi due esempi ( 1 , 2 ).

Answer 2

Potresti voler dare un'occhiata a Metamath (http://metamath.org), in particolare la Parte 1 Logica classica del primo ordine con l'uguaglianza del Metamath Proof Explorer .

Una prova per il tuo primo esempio è ax11w .

Questo probabilmente non è il tipo esatto di prova che stai chiedendo, ma queste prove sono state utili ad altri in passato, per comprendere la logica e le prove.