An infinitary rule of inference in the language of arithmetic according to which when $\phi \left(x\right)$ holds of every natural number $n$, then $\forall x\phi \left(x\right)$ may be inferred. Formally, this inference may be represented as:

The addition of the $\omega$-rule to first-order Peano arithmetic produces a stronger theory. Where $\text{Proves}\left(x,y\right)$ is the arithmetical formula corresponding to ‘$x$ encodes a proof terminating with the formula encoded by $y$,’ Peano Arithmetic proves $\neg \text{Proves}\left(n,\text{⌜}0=1\text{⌝}\right)$ for every standard natural number $n$, i.e., $\text{PA}$ proves of any standard $n$ that $n$ does not encode a proof of the absurd sentence $0=1$. Were one to employ the $\omega$ rule, then, one could make the following inference:

But the conclusion $\forall x\neg \text{Proves}\left(x,\text{⌜}0=1\text{⌝}\right)$ is just the sentence describing the consistency of $\text{PA}$, i.e., $\text{Con}\left(\text{PA}\right)$, which cannot be proved in $\text{PA}$, by Gödel’s First Incompleteness Theorem.