 The sequent-style version of Peano arithmetic with the \(\omega\)-rule will be denoted by \(\PA_{\omega}\). \(\PA_{\omega}\) has no use for free variables. Thus free variables are discarded and all terms will be closed. All formulae of this system are therefore closed, too. The numerals are the terms \(\bar{n}\), where \(\bar{0}=0\) and \(\overline{n+1}=S\bar{n}\). We shall identify \(\bar{n}\) with the natural number n. All terms t of \(\PA_{\omega}\) evaluate to a numeral \(\bar{n}\).