 Gentzen’s proof, though elementary, was very intricate and thus more transparent proofs were sought. As it turned out, the obstacles to cut elimination, inherent to PA, could be overcome by moving to a richer proof system, albeit in a drastic way by going infinite. This richer system allows for proof rules with infinitely many  premises.[15]  The inference commonly known as the \(\omega\)-rule consists of the two types of infinitary inferences: