First let me explain what I mean by algorithmically derivable. An algorithm must be able to come up with the proof without prior knowledge of the proof, in the same way mathematicians and computer scientists are able to create new proofs without prior knowledge of the proofs.
Our proof deriver enumerates all possible axiomatic systems, and with each system enumerates all possible proofs. It checks each proof to see if it proves Goedel's 1st theorem. This algorithm will necessarily derive all finite proofs eventually.
Goedel's 1st theorem states no sufficiently powerful axiomatic system can be complete and consistent at the same time. The deriver is complete, since it will eventually be able to prove all true statements and disprove all false statements. This means the deriver is inconsistent, so it cannot know whether a set of axioms used to prove Goedel's 1st are consistent.
Therefore, an algorithmic deriver is unable to derive the proof for Goedel's 1st theorem.
Does this proof succeed in showing Goedel's 1st theorem is not algorithmically derivable?