Calibrating the negative interpretation

TL;DR

This paper explores how classical logic can be embedded into intuitionistic theories through negative interpretations, analyzing their properties, limitations, and the classical content preserved in various constructive systems.

Contribution

It introduces the concept of minimum classical extensions via negative interpretations and characterizes their properties across different intuitionistic and constructive theories.

Findings

Intuitionistic arithmetic contains its classical content.

Recursive analysis cannot prove certain negative interpretations.

Classical content is preserved in Bishop's constructive analysis.

Abstract

The minimum classical extension S$^{+g}$ of a classically sound theory S based on intuitionistic logic, defined by adding to S the Gentzen negative interpretations of its mathematical axioms, contains a faithful translation S$^g$ of the classical version S + (--A -> A) of S. S$^g$ may be called the classical content of S. First and second order intuitionistic arithmetic contain their classical contents, but intuitionistic recursive analysis cannot prove the negative interpretation of its quantifier-free countable choice axiom. Variants of Kuroda's double negation shift principle (including the G\"odel-Dyson-Kreisel axiom equivalent to the weak completeness of intuitionistic predicate logic), and doubly negated characteristic function principles, provide neat characterizations of the minimum classical extensions of classically sound subsystems of Kleene's intuitionistic analysis I. Two-sorted basic constructive recursive mathematics contains its classical content. Bishop's constructive analysis has the same classical content as the neutral subsystem B of Kleene's I. By a result of Vafeiadou, minimum classical extensions of consistent, classically unsound theories (such as I) depend essentially on omega-models of their classically consistent subtheories.