Wednesday, April 27, 2017 (2:00 p.m. in Yost 306)

Title: Convex Geometry and Minkowski’s Linear Forms Theorem in Elementary Function Arithmetic

Speaker: Greg Knapp (Case Western Reserve University)

Advisor: Colin McLarty (Professor, Case Western Reserve University)

Abstract: A classical question in formal logic is “how much mathematics do we need to know in order to prove a given theorem?”  Of particular interest is Harvey Friedman’s grand conjecture: that every known mathematical theorem involving only finitary mathematical objects can be proven from Elementary Function Arithmetic (EFA)—a weaker variant of Peano Arithmetic.  If Friedman’s conjecture is correct, this would imply that Fermat’s Last Theorem is derivable from the axioms of EFA.  The vast task of proving Fermat’s Last Theorem from the axioms of EFA seems to require certain theorems on convex polytopes and an important corollary: Minkowski’s Linear Forms Theorem.  I show that certain theorems of convex geometry—e.g. representation of polytopes both in vertex form and as the intersection of half-spaces, monotonicity of volume, the existence of a separating plane between disjoint polytopes, and Minkowski’s Linear Forms Theorem—can be both interpreted and derived in EFA.