The Reverse Mathematics research program was introduced by Harvey Friedman with the goal of determining the minimal axioms needed to prove theorems of non-foundational mathematics. For my honors thesis, I have spent the last two semesters learning about said program in the context of commutative algebra.

In particular, while a standard proof of David Hilbert's Nullstellensatz uses his Basis Theorem, the former seems more constructive than the latter. For example, one may recall that upon learning about Hilbert's nonconstructive proof of the Basis Theorem, Paul Gordan, then at the forefront of invariant theory, exclaimed, "This is not mathematics. This is theology." Although this story has its caveats, it is, in fact, provable that the Basis Theorem needs strictly more machinery than the Nullstellensatz.

Through this talk, I aim to tell two parallel stories: the more mathematical story of formalizing the notion of being more or less constructive through subsystems of second-order arithmetic; and the more historical story of the broader shift from computational to conceptual argumentation. The overlap of these stories is surprisingly non-trivial, with connections to a partial realization of Hilbert's Program.

I am eternally grateful to Andreas Blass and Jamie Tappenden, who jointly advised my thesis.