Sam Buss, UC San Diego

Title: Feasibility in mathematics, computability, and provability

Abstract: This survey talk will discuss ultrafinitism, beginning with theories of Ed Nelson based on Robinson's theory Q, and how this extends to feasible reasoning in theories of bounded arithmetic. We also discuss connections to fundamental open problems in computational complexity, such as the P versus NP problem, and the status of independence results in bounded arithmetic for computational complexity.  We will discuss the notion of feasible provability as proposed by Steve Cook.

Ultrafinitism, finitism, and feasibility are three strict philosophical strands of constructivity in mathematics.  Ultrafinitism is generally viewed as the strictest philosophy, as it doubts, or even disavows, the existence of numbers that are too large to be written out in practice; for instance, $2\Uparrow 6$, i.e., $2^{2^{65526}}$.  The related notion of feasibility from computability theory generally refers to limiting computations or proofs to handling objects that are not too large to be handled in practice. Polynomial-time computability is generally used as the appropriate mathematical model for feasibility.  Finitism is a looser form of ultrafinitism; primitive recursive computability is often taken as the computational complexity of objects subject to finitistic reasoning. Constructivism is a broader term that generally allows consideration of any computable (recursive) objects.  Formal constructions, via interpretability in Robinson's theory Q, show that even the restriction to ultrafinitistic constructions can be expectedly strong.