Please use this identifier to cite or link to this item:
http://hdl.handle.net/11375/27875
Title: | Explorations in Padic Model Theory |
Authors: | Crighton, Aaron |
Advisor: | Haskell, Deirdre |
Department: | Mathematics |
Keywords: | Model Theory, Formal Verification, p-adics |
Publication Date: | Nov-2022 |
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. |
URI: | http://hdl.handle.net/11375/27875 |
Appears in Collections: | Open Access Dissertations and Theses |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
AaronCrightonThesisFinal.pdf | 749.39 kB | Adobe PDF | View/Open |
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.