Prenex normal form theorems in semi-classical arithmetic

TL;DR

This paper examines prenex normal form theorems within semi-classical arithmetic, identifies errors in previous proofs, provides counterexamples, and offers corrected and characterized versions of these theorems.

Contribution

It corrects and refines the prenex normal form theorems in semi-classical arithmetic, addressing previous errors and providing new characterizations.

Findings

Counterexample to previous prenex normal form theorem

Modified theorem with correct proof

Characterization of several prenex normal form theorems

Abstract

Akama et al. systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexample of their prenex normal form theorem, then modify it in an appropriate way. In addition, we characterize several prenex normal form theorems with respect to semi-classical arithmetic.