Can the omega-rule rescue Hilbert's program? 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.
 A: 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 . . .
A: $PA+\omega$-rule certainly proves $Con(PA)$.  If $Con(PA)$ is false, PA proves everything.  If $Con(PA)$ is true, this is a $\Pi^0_1$-statement, and $PA+\omega$-rule proves every true $\Pi^0_1$-statement (for each $n$, take the proof in $PA$ that $n$ does not encode a proof of $\bot$ in $PA$, and apply the $\omega$-rule to these proofs).
Your subscript seems to imply that you're only allowing a single use of the $\omega$-rule (that is, that you don't allow the $\omega$-rule to be used in the proofs justifying other uses of the $\omega$-rule).  However not that $PA$ together with the full $\omega$-rule gives true statements in $\mathbb{N}$, by a straightforward induction on the complexity of the formula.
However $PA+\omega$-rule is conservative over $PA$ for $\Sigma_1$ statements, including $\bot$.  This is shown by Schutte in his infinitary proof of cut-elimination for PA.
I don't understand your last two comments at all; $PA+\omega$-rule (the usual $\omega$-rule, not one with restricted premises) satisfies $L=PA+\omega_L$, and is $\Sigma_1$ conservative over $PA$, so not inconsistent.
A: Note: In Buldt's paper "The Scope of Goedel's First Incompletness Theorem" (find it under title on the web), he has the following statement (in Section 3.3):
"When we enter the (small) transfinite, we achieve closure, though, which precisely at $\omega^2$, viz., $\mathcal F^{\Omega}$=$\mathcal F^{\omega}_{\omega^2}$ [where $\mathcal F$ is a semi-formal theory extending $\mathrm Q$, $\mathcal F^{\Omega}$ is its closure under the $\omega$-rule, and $\mathcal F^{\omega}_{\alpha}$ is the same theory under $\alpha$ applications of the $\omega$-rule--my comment].  We should mention that $G2$ [the Second Incompleteness Theorem--my comment] still applies, for $\mathcal F^{\Omega}$ [=True Arithmetic--my comment] cannot formally prove its own consistency, which is now a $\Sigma^1_1$-sentence."
So apparently $G2$ keeps reappearing, even with closure under the $\omega$-rule.    
