I posted this earlier on the "narrowly-missed discoveries" thread, but I think it addresses the two paragraphs below address your three questions. For the most recent scholarly account of Post's work, see the article "Emil Post" by Alasdair Urquhart, which may be found here. In a nutshell: Gödel was first to fully formalise the notion of proof in a particular system, but Post came damn close to a more general idea.
Emil L. Post was very close to proving Gödel's incompleteness theorem, and the existence of algorithmically unsolvable problems in the early 1920s. He realized that one could enumerate all algorithms, and hence obtain an unsolvable problem by diagonalization. Moreover, the "problem" can be viewed as a computable list of questions Q_1,Q_2,Q_3,\ldots $Q_1,Q_2,Q_3,\ldots$ for which the sequence of answers (yes or no) is not computable. It follows that there cannot be any complete formal system that proves all true sentences of the form "The answer to Qi $Q_i$ is yes" or "The answer to Qi $Q_i$ is no," because this would solve the unsolvable problem.
But then Post was stuck because he needed to formalize the notion of computation. He had in fact (an equivalent of) the right definition, but logicians were not ready for a definition of computation, and did not believe there was such a thing until the Turing machine concept came along in 1936. Gödel avoided this problem when he proved his theorem (1930) by proving incompleteness of a particular system (Principia Mathematica).
