As known the second incompleteness theorem derailed Hilbert's program.
However, Hilbert himself tried to rescue it with the $\omega \text{-rule}$, according to the following paper:
http://repository.cmu.edu/cgi/viewcontent.cgi?article=1522&context=philosophy
The $\omega \text{-rule}$ says that if:
$$
\vdash \phi(c)
$$
for every constant $c$ can be proven then the following theorem can be added:
$$
\vdash \forall x: \phi(x)
$$
Important is to define in which system the prove is given. To improve the notation, I think it is best to add the system as subscript. So, $\omega \text{-rule}_{PA}$ means that the proof must be given in $PA$, which stands for First Order Logic + Peano Axioms.
EDIT
Given the answers the notation and the Hilbert's intend was not clear yet. If:
$$
K = L + \omega\text{-rule}_M
$$
Then $K$ and $L$ are two logics with the same syntax and sentences, but $M$ not necessarily. If:
$$
M \vdash \forall x : \lceil L \vdash \phi (x) \rceil
$$
Where the $x$ within $\lceil$ and $\rceil$ is expanded to $0, S(0), S(S(0))$, depended on the value of x, then:
$$
K \vdash \forall x: \phi(x)
$$
END EDIT
I have a little bit trouble in following the mentioned paper, there are a lot of notations. My question is whether the second incompleteness theorem makes the following impossible:
$$
PA + \omega\text{-rule}_{PA}\vdash Con(PA)
$$
I was convinced that this was not possible due to the following reasoning. If:
$$
PA + \omega\text{-rule}_{PA}\vdash\perp
$$
then the proof of that could easily be reduced to a proof of:
$$
PA \vdash \perp
$$
In such way that this is provable in $PA$. From that you have proven in $PA$ the relative consistency of $PA$ and $PA + \omega\text{-rule}_{PA}$. With that it would follow that $PA + \omega\text{-rule}_{PA}$ can prove its own consistency and then $PA$ could prove its own consistency.
However, I am not so sure anymore that the a proof of $\perp$ using the $\omega\text{-rule}_{PA}$ can easily be reduced to a $PA$ proof. If the result of $\omega\text{-rule}_{PA}$ is used in an induction hypothesis, then things get complicated.
I am now trying to prove $PA + \omega\text{-rule}_{PA}\vdash Con(PA)$ using Gentzen and don't see an obstacle yet, but these kind of proofs need a lot of care and I am not that far yet.
I also want to mention that the $\omega\text{-rule}$ will always a rule separate of all the other axioms and inference rules. If a system $L$ is created such that:
$$
L = PA + \omega\text{-rule}_L
$$
then the system $L$ is inconsistent. This is already the case with the reflection rule which is a special case of the $\omega\text{-rule}$.
Furthermore, the article uses $PRA$, but I consider that too restrictive. I prefer the $\Pi_2$ fragment of $PA$. And since it is believed that $PA$ is a conservative extension of this fragment, $PA$ in total can be used.
Best Answer
Addressing your issue with Godel: note that even the one-use $\omega$-rule is not computable. There's no obstacle to a non-recursive theory being complete.
Actually this is a bit more subtle than I'm giving it credit for, but the point still holds. Using your restricted $\omega$-rule, we do have finitary-ish proof objects: e.g. a proof of $PA+\omega_{PA}\vdash \forall x\varphi(x)$ is a Turing machine $\Phi_e$ such that for all $n$, $\Phi_e(n)$ is a $PA$-proof of $\varphi(n)$. In this sense, a proof is a finite object. However, telling whether $\Phi_e$ has this property is not computable! That is, proof-verification is non-effective.
Note that things get even worse once we allow more $\omega$-ruliness . . .