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?
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.