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.