Model Theory - Is `inv` a function in the language of fields

Stream: maths

[Chris Hughes]

In !4#6468 I defined the first order theory of fields. Most references I've seen in FOL don't include inv as a symbol, they use that language of rings and include an axiom that says inverses exist. I included inv as a symbol along with axioms along the lines of Lean's field axioms. Does anyone have opinions on this, or can think of implications of it? My analysis is as follows

• Potential diamonds around linking models for the theory of fields with Lean's fields are not an issue. These diagrams won't commute by definition anyway and I had to other find ways around this.
• Including inv makes it slightly easier to write down a first order formula, although you can always multiply out the inverses in any equation so it might not be that much of an issue.
• If someone wants to prove the theory of algebraically closed fields admits quantifier elimination then this is arguably a weaker statement if inv is included in the language, but you can multiply out inverses so maybe not a huge problem (maybe annoying zero issues here though).
• Maybe when working with the theory of comm rings and the theory of fields at the same time it's easy if they're defined over the same language.

[Antoine Chambert-Loir]

It's important that inverse is not in the language, for then terms without quantifiers are just polynomials and not rational fractions.

[Aaron Anderson]

I think that this is an argument for an API for working with definable functions, as the only thing that you really want to include inv for is to make explicitly writing formulas easier. Morally speaking, you want to be flexible as to whether you include inv, for the reasons mentioned above, and so that you can control whether substructures are subrings or subfields (this is just a consequence of what the terms are).

[Aaron Anderson]

I think the real reason people avoid putting inv in the language in the literature is to avoid partial functions though, which in Lean is clearly not a good reason.

[Chris Hughes]

What is a definable function ? Is it a true sentence of the form $\forall x_1...x_n, \exists ! y, \phi(x_1,...,x_n,y)$? I agree that this would be very useful.

[Adam Topaz]

The way I think of it is as a function whose graph is a definable subset.

[Antoine Chambert-Loir]

In some cases, it is important to retain a particular choice of a formula that defines a graph uniformly in all models.