Berarducci and Otero in [7] constructed a recursive nonstandard model of IOpen with an unbounded set of infinite prime elements. It turns out that their model is also normal, i.e., it is integrally closed in its fraction field. Normality is a first-order property; we need to express that any element of the fraction field of M which is a root of a monic polynomial with coefficients in M is in fact an element of M . The formalization of such property is the following formula N

where n £ N. In general, models of IOpen are not normal: normality follows from unique factorization and, for example, this does not hold in the Shepherdson model. Van den Dries was the first to consider normal