Constructive aspects of classical mathematics

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

The investigator is pursuing two lines of research, relevant to the general proof-theoretic program of extracting constructive, computational, and combinatorial information from theories of classical mathematics. The first involves extending a semantic approach to ordinal analysis to Kripke-Platek set theory, and extracting combinatorial and computational principles for the constructible hierarchy from the analysis. The second involves trying to find sharp conservation results for weak theories of nonstandard arithmetic, preferably via "natural" interpretations of the nonstandard theories in the standard ones, and exploring ways in which ordinary mathematics can be carried out in these frameworks. Since the beginning of the 20th century, there has been a gradual divergence between two different ways of thinking about mathematics. On the one hand, mathematics is viewed as a general investigation into abstract concepts, many of them involving infinitary objects and structures. On the other hand, many see mathematics as grounded by concrete symbolic representations and calculation. One goal of proof theory is to reconcile these two viewpoints, by finding the concrete, computational content that is hidden in general forms of abstract mathematical reasoning. The investigator aims to apply proof-theoretic methods to the study of theories of nonstandard analysis, and fragments of set theory.