Please use this identifier to cite or link to this item:
http://hdl.handle.net/11375/27875
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | Haskell, Deirdre | - |
dc.contributor.author | Crighton, Aaron | - |
dc.date.accessioned | 2022-09-26T21:52:43Z | - |
dc.date.available | 2022-09-26T21:52:43Z | - |
dc.date.issued | 2022-11 | - |
dc.identifier.uri | http://hdl.handle.net/11375/27875 | - |
dc.description.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. | en_US |
dc.language.iso | en | en_US |
dc.subject | Model Theory, Formal Verification, p-adics | en_US |
dc.title | Explorations in Padic Model Theory | en_US |
dc.type | Thesis | en_US |
dc.contributor.department | Mathematics | en_US |
dc.description.degreetype | Dissertation | en_US |
dc.description.degree | Doctor of Philosophy (PhD) | en_US |
dc.description.layabstract | This thesis explores theoretical and computational aspects of the p-adic numbers, which are fundamental objects of study in number theory. The thesis approaches these problems using techniques from model theory, which is a branch of mathemat- ical logic which is particularly effective at analyzing algebraic structures. The thesis has two parts. The first is purely theoretical and focuses on the proof of a theorem about p-adic functions which can be defined in certain logical languages. The second part takes a computational approach and focuses on developing theoretical results about p-adic numbers using a special software system called a proof assistant (the particular proof assistant is called Isabelle). By developing theory of p-adics in Is- abelle, we can use software to automatically verify the correctness of proofs of results and coherence of definitions. The resulting libraries can then be imported and used in future developments of machine-verified mathematical theory for more complex results. | en_US |
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.