[Merged by Bors] - feat(model_theory/basic): First-order languages, structures, homomorphisms, embeddings, and equivs

[awainverse]

Defines the following notions from first-order logic:

• languages
• structures
• homomorphisms
• embeddings
• equivalences (isomorphisms)
  The definitions of languages and structures take inspiration from the Flypitch project.

---

[jesse-michael-han]

nice work, LGTM

[adamtopaz]

This looks great!

[semorrison]

bors d+

[bors]

✌️ awainverse can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

Could you add a test file with an example of some non-trivial language object? Can language be used to describe a monoid, for instance?

[awainverse]

Could you add a test file with an example of some non-trivial language object? Can language be used to describe a monoid, for instance?

I was planning on creating a file of algebra examples in a follow-up PR. Would it suffice to post that separate PR as a proof-of-concept, and then merge this one?

[awainverse]

(I'll be following closely to https://github.com/flypitch/flypitch/blob/lean-3.14.0/src/abel.lean)

[awainverse]

I have an example at https://github.com/leanprover-community/mathlib/tree/fo_monoid

[awainverse]

bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[eric-wieser]

How does mul_assoc fit into that fo_monoid example?

[awainverse]

So far, I only have the ability to define a structure in the language of monoids, which is just a type with [has_one M] [has_mul M]. Later, I'll define terms, and formulas, and sentences, and what it means for a structure to satisfy a theory. Then it will be easy to define the theory of monoids, and it'll look something like M.satisfies T_monoids, where T_monoids is a set consisting of three axioms, one of which represents mul_assoc.