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?