Intuitionistic nonstandard bounded modified realisability and functional interpretation

TL;DR

This paper develops a bounded modified realisability and a functional interpretation for intuitionistic nonstandard arithmetic, enhancing understanding of its constructive content and proof properties, and aligning with nonstandard methods for analyzing compactness.

Contribution

It introduces a novel bounded functional interpretation for nonstandard arithmetic, connecting existing interpretations with majorisability, and addresses gaps in the literature.

Findings

Constructive content of nonstandard arithmetic clarified

Proof-theoretical properties established

Alignment with nonstandard methods for compactness analysis

Abstract

We present a bounded modified realisability and a bounded functional interpretation of intuitionistic nonstandard arithmetic with nonstandard principles. The functional interpretation is the intuitionistic counterpart of Ferreira and Gaspar's functional interpretation and has similarities with Van den Berg, Briseid and Safarik's functional interpretation but replacing finiteness by majorisability. We give a threefold contribution: constructive content and proof-theoretical properties of nonstandard arithmetic; filling a gap in the literature; being in line with nonstandard methods to analyse compactness arguments.