On the computational content of the Loeb measure

TL;DR

This paper explores the computational aspects of the Loeb measure within a weak logical framework, revealing that its definition possesses inherent computational content through term extraction methods.

Contribution

It introduces a novel interpretation of the Loeb measure in a weak set theory, demonstrating its computational content without relying on saturation or external sets.

Findings

Loeb measure can be meaningfully defined in a weak fragment of set theory.

The definition of the Loeb measure has computational content via term extraction.

Provides a new perspective on the computational aspects of Nonstandard Analysis.

Abstract

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 $\textsf{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].