On the computational content of the Loeb measure

The Loeb measure is one of the cornerstones of Nonstandard Analysis. The traditional development of the Loeb measure makes use of saturation and external sets. Inspired by [13], we give meaning to special cases of the Loeb measure in the weak fragment $\mathsf{\text{P}}$ of Nelson’s internal set theory from [1]. Perhaps surprisingly, our definition of the Loeb measure has computational content in the sense of the `term extraction’ framework from [1].