Joan Rand Moschovakis (Occidental College, Emerita)

Title:
Minimum classical extensions of constructive theories

Abstract:
Constructive reverse mathematics, based on the pioneering work of Kleene, Vesley, Kreisel, Troelstra, Bishop and Bridges in the last century, is being developed by Ishihara and others in the tradition of Simpson's and Friedman's classical reverse mathematics.  Wim Veldman's intricate reverse intuitionistic analysis splits notions in the style of Brouwer, resulting in still finer distinctions.  Negative interpretations feature in proof mining, where Kohlenbach and others extract computational information from classical proofs.

In this talk I focus on two families of principles consistent with, but independent of, constructive and intuitionistic analysis.  These double negation shift and weak comprehension principles quantify the constructive cost of adding to an axiomatic system  S, based on intuitionistic logic, the Goedel negative translations of its classically correct mathematical axioms. The resulting ``minimum classical extension'' of S includes a faithful image of its classical content, and preserves the effective meanings of disjunction and existence.

Any consistent theory based on intuitionistic logic has a minimum classical extension. Kleene's intuitionistic analysis, Bishop's constructive analysis, Markov's recursive analysis, and their subsystems are examples.