Arithmetical Characterizations of Two Intuitionistic Logical Principles

This paper investigates the role of negation in arithmetic by analyzing subsystems based on subminimal logic.We introduce NA PR , a system of subminimal arithmetic equipped with all primitive recursive functions, and answer the following four questions: (1) Can we develop reasonable arithmetic within NA PR ?(2) Can we characterize logical rules Absorption of Negation (An) and Ex Falso Quodlibet (ECQ) by arithmetical principles?(3) Are there strict differences in deductive power among NA PR , MA PR , and HA? (4) Do MA PR and MA, and NA PR and NA have a similar mutual interpretability relationship as HA?We show the following: First, Heyting Arithmetic (HA) is shown to be a conservative extension of NA PR for positive formulas.Based on NA PR , we prove that (ECQ) is equivalent to the definability of disjunction, and that (An) is equivalent to a variant of the least number principle.Furthermore, using the constant domain neighbourhood semantics, we show that the systems NA PR , MA PR (written as NA PR + (An)) and HA (written as NA PR + (An) + (ECQ)) form a strictly increasing hierarchy of strength.Finally, we demonstrate the essential role of primitive recursive functions in weak arithmetic using classical countermodels.