Is there a database somewhere of simple FOL statements, with their proofs written out in a Hilbert-style deduction system, or perhaps a tool to take such statements and produce proofs? While I see immediately how to encode arbitrary *statements* in FOL, I have have had months of trouble trying to understand how formal *proofs* relate to the intuitive proofs I know from doing ordinary mathematics. I think seeing formal proofs of obvious statements like\begin{equation*} (\forall x\forall y\;P(x,y))\rightarrow(\forall y\forall x\;P(x,y)) \end{equation*}and\begin{equation*} (\forall x\forall y\;P(x,y))\rightarrow(\forall x\;P(x,x)) \end{equation*}might finally get me unstuck.
$\endgroup$ 12 Answers
$\begingroup$There is a proof tree generator made by Wolfgang Schwarz which takes arbitrary statements in a few different logics (first order logic, modal logic, propositional logic) and provides a proof that they are tautologies, contingent, always false, valid statements, and so forth automatically.
The only disadvantage is that it uses a proof tree method instead of the Hilbert style you mentioned. Hopefully another answer can provide a link to such a proof generator.
Here are proofs of your two examples (1,2).
$\endgroup$ $\begingroup$You might want to have a look at Metamath (), specifically Part 1 Classical First-Order Logic with Equality of the Metamath Proof Explorer.
A proof for your first example is ax11w.
This is probably not the exact type of proof that you are asking for, but these proofs have been helpful to others in the past, for understanding logic and proofs.
$\endgroup$ 1
