# Is it possible to create a software to find formal proofs?

Let's say I have a Hilbert style system, with a few axioms and rules of inference, and I want to find a proof for some formula $\varphi$, is it possible to create an algorithm that would find a proof for it with the given system (guaranteeing it'd be in finite time)?

I know a bit of programming, but I think answering this question goes beyond my abilities.

• en.wikipedia.org/wiki/Automated_theorem_proving – reuns Feb 6 '16 at 20:21
• Yes. But finite does not mean practical or even before the end of the Universe – Hagen von Eitzen Feb 6 '16 at 20:22
• A proof is a certain type of sequence of words. List all possible sequences, check for each whether it is a proof, and whether it ends in $\varphi$. – André Nicolas Feb 6 '16 at 20:22
• Perhaps you mean "guaranteeing the program terminates on all inputs" ? If a program ends, it will always be in finite time. – DanielV Feb 6 '16 at 23:48
• The wording of your question is unclear: what is the algorithm to do if presented with an unprovable input? Also, if you are only interested in propositional logic, then please state that in your statement of the question. – Rob Arthan Feb 7 '16 at 1:58

• I'm looking for an algorithm just for propositional logic, using the standard language ($(\{p_0,p_1,\dots\},\{\neg,\wedge,\vee,\rightarrow\},\{(,)\})$), could you provide some sources about your statement? – YoTengoUnLCD Feb 6 '16 at 21:07
• @YoTengoUnLCD : in propositionnal logic, everything reduces to boolean functions $B^n \to B$, so your proof program reduces to computing boolean functions (and checking they are equal), this should be less than $100$ lines of code with simple recursive functions and data structures (binary trees) – reuns Feb 6 '16 at 21:48
• It is not true that only complete theories are decidable: if you add an uninterpreted constant symbol, $c$, say, to the signature of a decidable theory like the theory of real closed fields, the resulting theory is decidable but not complete. Given a sentence $\phi$, $\phi$ is valid iff $\forall x\phi[x/c]$ is valid in real closed fields, but the sentence $c = 0$ is neither valid nor unsatisfiable. – Rob Arthan Feb 7 '16 at 1:43