Decidability in extensions of Fp((t)) - Rigler, B (2021)
In this thesis we primarily consider the first-order theory of the local field F_p((t)) and the question of whether it is decidable. To this end we expand the language of valued fields together with a constant symbol for t by adding predicates R_f representing the existence of a root of the multivariable polynomial f \in F_p(t)[X_1, ..., X_n], hoping in this way to control the behaviour of purely wild extensions of valued fields (which has historically caused problems in this area), and seek to prove a quantifier elimination result for a proposed axiomatisation of F_p((t)) (originally, we believe, due to F-V. Kuhlmann). This proceeds along classical lines, à la Shoenfield (used in Macintyre’s celebrated proof of quantifier elimination for the p-adic numbers Q_p). We obtain a conditional result, sketching a proof that if a particular technical condition is satisfied by an arbitrary \aleph_1-saturated model of our theory, then we will indeed obtain quantifier elimination and thereby (via the existence of an algebraically prime model) decidability of the first-order theory of F_p((t)). However, this technical condition is still largely mysterious. We sketch an (unsuccessful) attempt at an unconditional proof and highlight where difficulties arise.