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.

  • 3
    $\begingroup$ en.wikipedia.org/wiki/Automated_theorem_proving $\endgroup$ – reuns Feb 6 '16 at 20:21
  • $\begingroup$ Yes. But finite does not mean practical or even before the end of the Universe $\endgroup$ – Hagen von Eitzen Feb 6 '16 at 20:22
  • $\begingroup$ 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$. $\endgroup$ – André Nicolas Feb 6 '16 at 20:22
  • $\begingroup$ Perhaps you mean "guaranteeing the program terminates on all inputs" ? If a program ends, it will always be in finite time. $\endgroup$ – DanielV Feb 6 '16 at 23:48
  • $\begingroup$ 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. $\endgroup$ – Rob Arthan Feb 7 '16 at 1:58

You can only find proofs for any given valid formula, if your calculus is complete. Under the precondition that your calculus is complete, it is possible to create an algorithm that will terminate for every valid formula. However, if your language is undecidable (e.g. first-order logic), you cannot find an algorithm that will terminate for every (valid and non-valid) formula.

  • $\begingroup$ 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? $\endgroup$ – YoTengoUnLCD Feb 6 '16 at 21:07
  • $\begingroup$ A proof always has finite length. By induction on the string length (you first create strings of length 1, then of length 2, then of length 3, and so on) and checking if the strings are proofs you can eventually find a proof. This is essentially what "André Nicolas" already stated in his comment. $\endgroup$ – Xaver Feb 6 '16 at 21:16
  • $\begingroup$ @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) $\endgroup$ – reuns Feb 6 '16 at 21:48
  • $\begingroup$ @user1952009: Your statement is correct; however, the question is how to find a Hilbert-style proof. I think your statement doesn't cover that aspect. $\endgroup$ – Xaver Feb 6 '16 at 21:52
  • 1
    $\begingroup$ 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. $\endgroup$ – Rob Arthan Feb 7 '16 at 1:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.