 \(\PA_{\omega}\) has all the inference rules of the sequent calculus except for \(\forall R\) and \(\exists L\). In their stead, \(\PA_{\omega}\) has the \(\omega R\) and \(\omega L\) inferences. The Axioms of \(\PA_{\omega}\) are the following: (i) \(\emptyset\Rightarrow A\) if A is a true atomic sentence; (ii) \(B\Rightarrow \emptyset\) if B is a false atomic sentence; (iii) \(F(s_1,\ldots,s_n)\Rightarrow F(t_1,\ldots,t_n)\) if \(F(s_1,\ldots,s_n)\) is an atomic sentence and the \(s_i\) and \(t_i\) evaluate to the same numerals, respectively.