I'm currently reading about Inferentialism and proof theoretic semantics. I read in Peregrin's "Inferentialism: Why rules matter" and Baker's "Aspects of the Constructive Omega Rule within Automated Deduction" that replacing the introduction-rule for universal quantification and the induction axiom by the $\omega$-rule (P(0),P(1),.../$\forall xP(x)$) is enough to overcome the first incompletness theorem for first order PA. Peregrin uses this to argue that the gap between classical consequence and derivability in (semi-)formal systems can be closed.
Buldt in "The scope of Gödels first incompletness theorem" (https://rdcu.be/c2WO8) states that just adding the rule isn't enough and that we also have to allow infinitely many applications of the rule. He adds a proof that I unfortunately do not understand. I'm currious whether it's just left out by Peregrin and Baker or if there is something I'm missing.
I'd be thankful if someone could elaborate on that.