# Gödel's Completeness Theorem: Did Gödel show how to construct derivations?

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?

• – J.G. Jan 6 at 21:21
• @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 ... – Bram28 Jan 6 at 21:29
• You may want to look at the semantic (or analytic) tableau approach. – Fabio Somenzi Jan 6 at 23:30
• @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? – Bram28 Jan 6 at 23:32
• 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. – Fabio Somenzi Jan 6 at 23:42