While Zermelo-Fraenkel set theory provides a broad and flexible framework for the formalization of mathematics, recent proof-theoretic research has shown that a good deal of day-to-day mathematical argumentation correlates more closely with much weaker subsystems of second-order arithmetic. In this project Avigad will use model-theoretic techniques to explore the finitary combinatorial consequences of these theories. This includes finding Ramsey-theoretic independences akin to the Paris-Harrington theorem, and developing a combinatorial, model-theoretic approach to ordinal analysis. The aim of mathematical logic is to create formal models that describe various aspects of mathematical practice, and apply mathematical techniques to the analysis of these models. Since the beginning of this century, two conflicting and antagonistic views of mathematics have shared an uneasy coexistence. From a classical point of view, mathematics is "about" the infinite, yielding powerful and compelling abstractions. From a constructive point of view, mathematics must always have some concrete, computational meaning, from which it derives its applicability. This project aims to obtain a better understanding of the interplay between these two aspects of mathematical practice, through the formal exploration of infinitary assumptions and their finite, combinatorial consequences.
