 where \(A(x,P)\) is a formula of the language of PA augmented by P in which the predicate P occurs only  positively.[28]  The syntactic condition of positivity then ensures that the operator \(\Gamma_A\) is monotone. The language of \(\bID_1\) is an extension of that of PA. It contains a unary predicate symbol \(I_A\) for each positive arithmetical operator \(\Gamma_A\) and the axioms 