It is well-known that the category of local rings and *ring* homomorphisms admits an axiomatisation in coherent logic. Explicitly, it is the coherent theory over the signature $0, 1, -, +, \times$ with the usual axioms for rings, plus the axioms
$$0 = 1 \vdash \bot$$
$$\top \vdash (\exists b . \; a \times b = 1) \lor (\exists b . \; (1 - a) \times b = 1)$$
See, for example, [*Sheaves in Geometry and Logic*, Ch. VIII, §6]. Unfortunately, because homomorphisms are only required to commute with the various things in the signature, the homomorphisms here are just ring homomorphisms and need not be local. It appears to me that the neatest way to fix this is to introduce a unary relation symbol $(\quad) \in \mathfrak{m}$, with the intention that $\mathfrak{m}$ is interpreted as the unique maximal ideal of the local ring. Then, by the usual rules for homomorphisms of models, a homomorphism $R \to R'$ must map elements of $\mathfrak{m}$ to elements of $\mathfrak{m}'$. But is there a way to axiomatise the theory so that

we get a coherent, or at least geometric theory, and

the category of models in $\textbf{Set}$ is indeed the category of local rings and local ring homomorphisms, and

the structure sheaf homomorphism $f^\ast \mathscr{O}_{Y} \to \mathscr{O}_{X}$ of morphism of locally ringed spaces $X \to Y$ is a homomorphism in the category of models for this theory?

Ideally, we'd like to define $\mathfrak{m}$ to be the subsheaf of nowhere invertible sections defined by
$$\{ s \in \mathscr{O} : \nexists t . \; s \times t = 1 \}$$
but unfortunately $\nexists t . \; s \times t = 1$ is not a geometric formula. (The formula $\forall t . \; s \times t \ne 1$ is equivalent to the previous one but has the same defect.) We can salvage one half of the biimplication as the geometric sequent
$$(a \in \mathfrak{m}) \land (\exists b . \; a \times b = 1) \vdash \bot$$
which merely expresses the requirement that "$a$ is not in $\mathfrak{m}$ if $a$ is invertible", but we also need to express the requirement that "$a$ *is* in $\mathfrak{m}$ if $a$ is *not* invertible". One possibility is the following:
$$\top \vdash (\exists b . \; a \times b = 1) \lor (a \in \mathfrak{m})$$
These two axioms appear to give the correct characterisation of $\mathfrak{m}$ in intuitionistic first order logic: it is easy to derive from these axioms that
$$a \in \mathfrak{m} \dashv \vdash \nexists b . \; a \times b = 1$$
so the interpretation of $\mathfrak{m}$ is completely determined by the axioms, at least in a topos.

But does every local ring object (in the sense of the first paragraph) admit an $\mathfrak{m}$ satisfying these axioms? The answer appears to be no, for the reason that these axioms assert that a every section of a sheaf of a local ring admits an open cover of the space by open sets on which the restriction is either invertible or nowhere invertible – and this is certainly not true in the contexts of interest. Can this idea be rescued with a more clever approach?