Reorganizing the ModelTheory Folder

Stream: mathlib4

[Aaron Anderson]

There are some substantial edits to the model theory library that I've been considering for ages, and another one recently suggested (removing CategoryTheory.Bundled).
However, some of the basic files are large and unwieldy to edit, so I think a reorganization may be in order before trying any substantial refactors.

[Aaron Anderson]

To this end, I've started this branch: https://github.com/awainverse/mathlib4/tree/modeltheoryreorg

[Aaron Anderson]

I've also added a bit more documentation. Does anyone have opinions on whether this is easier to read and understand?

[Aaron Anderson]

Paging some folks with relevant experience: @Floris van Doorn @Johan Commelin @Yaël Dillies

[Bryan Gin-ge Chen]

(Looks like you might not have committed the renamed files to the branch you linked?)

[Aaron Anderson]

Thanks - I'm out of practice with basic git.

[Aaron Anderson]

(If we do like this enough to implement it, I'll also have to be reminded the right way of dealing with Mathlib.lean.)

[Johan Commelin]

lake exe mk_all should take care of all things Mathlib.lean

[Mathias Stout]

Can I ask how substantial the changes would be? Do you e.g. want to go all the way back to say first-order formulas and redefine them to work in the setting of continuous or many-sorted logic?

[Shaopeng]

May I ask what downstream impacts it might make to remove CategoryTheory.Bundled?

A few ModelTheorymodules depend on Mathlib.ModelTheory.Bundled, including Satisfiability, IsFraisse and Order. For projects that heavily rely on these modules, should substantial rewrites be expected?

Thanks!

[Aaron Anderson]

Mathias Stout said:

Can I ask how substantial the changes would be? Do you e.g. want to go all the way back to say first-order formulas and redefine them to work in the setting of continuous or many-sorted logic?

I don't have any concrete proposals yet. Yes, I would consider modifying formulas, but I don't have any suggestions yet that would increase the scope of the logic itself. My main idea would be to shift emphasis to formulas mod a theory, and perhaps simplify some other aspects of the construction along the way: https://github.com/leanprover-community/mathlib4/pull/16801

[Aaron Anderson]

Shaopeng said:

May I ask what downstream impacts it might make to remove CategoryTheory.Bundled?

A few ModelTheorymodules depend on Mathlib.ModelTheory.Bundled, including Satisfiability, IsFraisse and Order. For projects that heavily rely on these modules, should substantial rewrites be expected?

Thanks!

I don't think much has to change meaningfully. The only aspect of that change that has much to do with this reorganization is the separation out of the Maps folder. Removing Bundled is related to, but does not require, actually using those maps to define interesting categories of structures.

[Aaron Anderson]

Removing Bundled does not require enough changes to need this reorganization: #32285