Explorations in Padic Model Theory

Abstract

This thesis explores various aspects of the model theory of p-adic fields. It is divided into two distinct parts. The first part pertains to the theory of P -minimal structures. The main focus is exploring a class of P -minimal structures which display a certain tameness property with respect to the approximation of definable functions by their Taylor polynomials, and builds to a proof of a theorem for passing from local ap- proximations by Taylor polynomials to global (piecewise-definable) approximations of functions by their Taylor polynomials in such structures. The final chapter of this part discusses some aspects of classifying the scope of the class of structures that this theorem applies to. The second part of the thesis describes a formally verified proof of Macintyre’s quantifier elimination theorem for p-adic fields in the Isabelle proof assistant. The algebraic formalisations to required state and prove this theorem are outlined, including constructions of the p-adic integers and fields, as well as a formally verified proof of Hensel’s Lemma.