Multisorted languages/model theory

Stream: new members

[Mathias Stout]

I would be interested to know if there is already some work on first order languages with potentially multiple sorts, complementing the material available in Mathlib.

Or maybe someone here already has spent some time thinking about this?

[Yaël Dillies]

@Sky Wilshaw needs it for Con(NF)

[Mathias Stout]

Oh thanks! Great, I'll check the project.

[Mathias Stout]

If I gather correctly, precise design suggestions are given, but actual development of many-sorted model theory is not currently an aim of CON(NF) or follow-up projects? (I guess this is a question for Sky Wilshaw)

[Kenny Lau]

do you have a particular application in mind?

[Mathias Stout]

I'd like to talk about valued fields, with e.g. sorts for the main field, residue field and value group.
One does not strictly need the multisorted setup, as these are definable quotients of the valued field, but it seems does seem more natural to have a functioning multi-sorted setup.