4
$\begingroup$

Gödel's Completeness Theorem for first-order logic states that there is a proof system with a finite number of rules and axioms that is both sound and complete for first-order logic: that there exists a derivation within such a proof system for all valid statement from first-order logic.

My question is: did Gödel merely prove that there exists some such a derivation, or did Gödel's proof show what such a derivation would actually look like, i.e. how to derive any valid statement?

Of course, given the truth of the Completeness Theorem, we can always obtain a derivation as follows: systematically iterate through all possible derivations (which is possible, since the set of derivations is enumerable), and if the statement is valid, then eventually we'll run into a derivation for it.

However, pointing to such an algorithm will of course not prove that there is a derivation. So, I was wondering if maybe Gödel had an algorithm that he pointed to and for which he proved that it would always create a derivation of any valid statement. Or, at the very least: does Gödel's proof naturally translate itself into such an algorithm?

If not, is there a well-known alternative proof of the Completeness Theorem that does provide such an algorithmic proof?

|cite|improve this question
$\endgroup$
  • 1
    $\begingroup$ See en.wikipedia.org/wiki/… $\endgroup$ – J.G. Jan 6 at 21:21
  • $\begingroup$ @J.G. Yeah, I saw that, and I also went to: en.wikipedia.org/wiki/… but I couldn't quite figure it out from there ... it doesn't look like he is producing an algorithm ... $\endgroup$ – Bram28 Jan 6 at 21:29
  • $\begingroup$ You may want to look at the semantic (or analytic) tableau approach. $\endgroup$ – Fabio Somenzi Jan 6 at 23:30
  • $\begingroup$ @FabioSomenzi Yes, that;'s exactly what I was thinking: it seems like we should be able to make that into an algorithmic proof ... do you know if anyone has actually done that? Also, any tableaux can be converted into a more traditional natural deduction style proof ... so even before these tableaux were around, I am thinking someone must have had the insight to effectively use the basic method of tableaux (one big proof by contradiciton, and then just exploring al possible options for satisfiability) in a more traditional style proof ... who was the first to think of this? $\endgroup$ – Bram28 Jan 6 at 23:32
  • $\begingroup$ Perhaps, you want to take a look at Melvin Fitting's First-Order Logic and Automated Theorem Proving, Springer 1996? A naive implementation of the semantic tableau approach for first-order logic does not guarantee that the tableau will be closed whenever it's possible, but there ways to obviate that. $\endgroup$ – Fabio Somenzi Jan 6 at 23:42
2
$\begingroup$

No, the completeness theorem is far from algorithmic. It uses the axion of choice and in fact is equivalent to the ultrafilter lemma, a weaker form of choice.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ OK, thanks ... but there are algorithms to construct derivations, assuming derivations exist, right? I mean the 'dumb' brute force method I describe is one such algorithm. But are there more directly algorithmic proofs? If so, who was the first to do so? $\endgroup$ – Bram28 Jan 6 at 21:31
  • $\begingroup$ Only needs axiom of choice for uncountable languages, (and I don't think Godel's original version covered uncountable languages). $\endgroup$ – spaceisdarkgreen Jan 6 at 21:32
  • $\begingroup$ @Bram28 The brute force method you described is not an algorithm: if the statement is valid, you'll find a proof, but if the statement is not valid, you will run forever. In fact, there is no algorithm in many cases. $\endgroup$ – Ted Jan 6 at 21:34
  • 1
    $\begingroup$ @Ted I am well aware of that. The 'dumb' brute force method I describe will of course run forever if the statement is not valid. And yet, for all the valid ones I will eventually get a derivation. I am wondering if there are more efficient ways to produce a derivation for the valid ones, even if that way will sometimes run forever for the invalid ones. If you don't want to call that an algorithm, ok, let's just call it a set of instructions then. $\endgroup$ – Bram28 Jan 6 at 21:38
  • $\begingroup$ @Bram28 you may be refrring to automatic theorem provers. This is a very active area of research. $\endgroup$ – Ittay Weiss Jan 6 at 21:46

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.