Note on $\Pi^0_{n+1}$-LEM, $\Sigma^0_{n+1}$-LEM and $\Sigma^0_{n+1}$-DNE

TL;DR

This paper explores the independence and behavior of certain logical principles related to arithmetical and analysis systems, extending previous results to a broader intuitionistic framework and examining their negations.

Contribution

It extends prior independence results of arithmetical principles from HA to the FIM system of intuitionistic analysis, and analyzes their double negations.

Findings

Independence results hold over FIM, not just HA.

Double negations of principles behave differently in HA and FIM.

Some elementary questions remain open.

Abstract

We show that results of Akama, Berardi, Hayashi and Kohlenbach, on the relative independence of certain arithmetical principles over intuitionistic arithmetic HA, hold also over Kleene and Vesley's system FIM of intuitionistic analysis, which extends HA and is consistent with classical arithmetic but not with classical analysis. The double negations of the universal closures of these principles are also considered, and shown to behave differently with respect to HA and FIM. Various elementary questions are left open.