A note on non-classical Nonstandard Arithmetic

TL;DR

This paper investigates the inconsistencies of the Dinis-Gaspar nonstandard arithmetic system with classical Transfer and other axioms, revealing its limitations and boundary within nonstandard analysis.

Contribution

It identifies the minimal fragments of Transfer and other axioms incompatible with the Dinis-Gaspar system, clarifying its logical boundaries and relation to classical and intuitionistic principles.

Findings

Dinis-Gaspar system is inconsistent with Transfer axiom.

The system conflicts with several continuity theorems.

It involves a standard part map, challenging its classification.

Abstract

Recently, a number of formal systems for Nonstandard Analysis restricted to the language of finite types, i.e. nonstandard arithmetic, have been proposed. We single out one particular system by Dinis-Gaspar, which is categorised by the authors as being part of intuitionistic nonstandard arithmetic. Their system is indeed inconsistent with the Transfer axiom of Nonstandard Analysis, and the latter axiom is classical in nature as it implies (higher-order) comprehension. In this paper, we answer the following questions: (Q1) In the spirit of Reverse Mathematics, what is the minimal fragment of Transfer that is inconsistent with the Dinis-Gaspar system? (Q2) What other axioms are inconsistent with the Dinis-Gaspar system? Perhaps surprisingly, the answer to the second question shows that the Dinis-Gaspar system is inconsistent with a number of (non-classical) continuity theorems which one would -- in our opinion -- categorise as intuitionistic. Finally, we show that the Dinis-Gaspar system involves a standard part map, suggesting this system also pushes the boundary of what still counts as 'Nonstandard Analysis' or 'internal set theory'.