A valued field $ K $ is said to be Henselian if there is a unique extension of the valuation to the algebraic closure of $ K $. (TODO: double check that this definition is correct.)

There is always at least one extension, so the condition here is that this extension is unique.

Embedding $ K $ into a monster model of ACVF, Henselianity amounts to the claim that $ \operatorname{dcl}(K) $ is the perfect closure of $ K $. (right?)

Usually, henselianity is defined as saying that some version of Hensel's lemma holds in $ K $…

Non-archimedean local fields ($ \mathbb{Q}_p $, its algebraic extensions, and $ F((t)) $ for $ F $ a finite field) are Henselian. Puiseux series are Henselian (even in positive characteristic, if I recall correctly).

Henselianity is a first-order condition, so ultraproducts of Henselian fields are henselian. This was used by Ax, Kochen, and Ershov to transfer properties of $ \mathbb{F}_p((t)) $ to $ \mathbb{Q}_p $.

The Ax-Kochen-Ershov principle gives relative quantifier elimination, or something like that, for characteristic 0 Henselian fields that are absolutely unramified, meaning that either

- The residue characteristic is 0, OR
- The residue characteristic is $ p $, and $ p $ has minimal valuation among elements of the value group.

Here, relative quantifier elimination means "relative to the value group and the residue field."

Some verion of the AKE result says that if $ K $ and $ L $ are two absolutely unramified characteristic 0 Henselian fields, then $ K \equiv L $ (as valued fields) if and only if $ K $ and $ L $ have elementarily equivalent value groups (as ordered abelian groups), and elementarily equivalent residue fields.

Algebraically closed valued fields are Henselian, as are $ p $-adically closed fields, their finite algebraic extensions, and ultraproducts of $ \mathbb{Q}_p $. Another sort of Henselian valued field considered is RCVF, the theory of real-closed henselian valued fields. (This is the theory of Puiseux series over $ \mathbb{R} $, with the valuation. The residue field is real-closed, and the value group is divisible.)