The strength of nonstandard analysis

A weak theory nonstandard analysis, with types at all finite levels over both the integers and hyperintegers, is developed as a possible framework for reverse mathematics. In this weak theory, we investigate the strength of standard part principles and saturation principles which are often used in practice along with first order reasoning about the hyperintegers to obtain second order conclusions about the integers.