Axiomatisabilité et décidabilité de corps valués henseliens

In this mémoire we explore model theoretic questions around the axiomatizability and decidability of theories and fragments of theories of henselian valued fields, particularly those of positive residue characteristic. Perhaps the most important open problem in this area is the question of the decidability of fields Fq((t)) of formal power series over finite fields. While the full theories of such fields remain mysterious, their existential theories are increasingly well understood: in 2003, Denef and Schoutens gave an algorithm, based on the assumption of Resolution of Singularities in positive characteristic, to determine whether or not an existential sentence in the language of rings together with a symbol for t holds in Fq((t)). With Fehm, in 2016, we gave unconditionally a decision procedure to decide the existential theory in a language without the additional symbol for t. Later in 2023, also with Dittmann, we gave a decision procedure to existential theory with t conditionally on an assumption called (R4), which we know follows from Resolution of Singularities, but seems in principle significantly weaker. We present here a unified exposition of these two results. In mixed characteristic, with Dittmann and Jahnke in 2024, we gave an axiomatization of the theories of finitely ramified henselian valued fields of mixed characteristic, in terms of the value group and of the structure induced on the residue field. We give a brief exposition of this result, and represent it slightly to give a resplendent statement that is essentially uniform in the residue characteristic. Two other topics explored in this text are "existentially henselian" fields — those fields existentially equivalent to a field admitting a nontrivial henselian valuation —, and theories of separably tame valued fields, which we extend to allow infinite imperfection degree.