I posted this earlier on the "narrowly-missed discoveries" thread, but I think 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$ 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 $Q_i$ is yes" or "The answer to $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).
The key idea Feferman is exploiting is that there can be two different enumerations of the axioms of a theory, so that the theory does not prove that the two enumerations give the same theory.
Here is an example. Let $A$ be a set of the axioms defined by some formula $\phi(n)$ (that is, $\phi(x)$ holds for exactly those $x$ that are in $A$). Define a new formula $\psi(n)$ like so:
$\psi(n) \equiv \phi(n) \land \text{Con}( \langle x \leq n : \phi(x)\rangle)$
Where Con(σ) is a formula which says that no contradiction is provable from the axioms listed in the sequence σ.
In the case where $A$ is the set of axioms for a suitable consistent theory $T$ that satisfies the second incompleteness theorem, the following hold:
(1) In the standard model, we have $\phi(n) \Leftrightarrow \psi(n)$ for all $n$, because $T$ really is consistent.
(2) T does not prove that $\phi(n) \Leftrightarrow \psi(n)$ for all $n$, because this equivalence implies that T is consistent.
(3) If we use $\psi$ to define a formula Conψ(T), then T will prove (under the assumption that the empty theory is consistent, if this is not provable in T) that the theory defined by ψ is consistent. However, T will not prove Conφ(T), which is the usual consistency sentence for T.
This kind of example is presented in a more precise way in Feferman's 1960 paper that you mentioned, along with precise hypotheses on the theory and sharper results.
My opinion is that we cannot regard a proof of Conψ(T) as a proof of the consistency of T, because although φ and ψ are extensionally identical, they do not intensionally represent the same theory. Feferman expresses a similar idea on his p. 69. Of course, this is a matter of philosophy or interpretation rather than a formal mathematical question.
Addendum
The difference between extensional and intensional equality is easiest to explain by example. Let A be the empty set and let B be the set of integers larger than 1 that do not have a unique prime factorization. Then we know B is also the empty set: so A and B are extensionally equal. But the definition of B is much different than the definition of A: so A and B are intensionally different.
This distinction is often important in contexts like computability and formal logic where the things that you work with are actually definitions (also called codes, indices, Gödel numbers, or notations) rather than the objects being defined. In many cases, extensional equality is problematic, because of computability or effectiveness problems. For example, in my answer above, we know that φ and ψ define the same set in the real world, but this fact requires proof, and that proof may be impossible in the object theory we are dealing with. On the other hand, intensional equality is easy to decide, provided you are working directly with definitions.
Best Answer
Some related information :
1) Volume 2 of Hilbert & Bernays, Grundlagen der Mathematik (1939) include full proofs of Gödel's 1st and 2nd Theorems (for the 2nd one, it was the first published complete proof), as well as Gentzen's concistency proof, with detailed discussion of their "impact" on the finitist standpoint.
See Wilfried Sieg & Mark Ravaglia, David Hilbert and Paul Bernays Grundlagen der Mathematik I and II : A Landmark.
2) See in : David Hilbert, Lectures on the Foundations of Arithmetic and Logic 1917-1933 (Wilfried Sieg ed - 2013), the Introduction to the Appendices, page 788-on, regarding Hilbert's lectures of the '30s (and thus, "affected" by Gödel's Theorems).
3) Assuming that the the work on Grundlagen was at least "supervised" or "agreed on" by Hilbert, we can see Paul Bernays' paper of 1967 : it seems that Hilbert carried on with his foundational project post-1930, in order to take into account Godel's works :
About Beweis des Tertium non datur, here is Wilfried Sieg's comment :
Sieg's introductions are expanded into :