search

teorth / equational_theories

A project to map out the relations between different equational theories of Magmas.
https://teorth.github.io/equational_theories/
Apache License 2.0
177 stars 45 forks source link

METATHEOREM: remove the use of choice in Completeness #499

Open codyroux opened 1 week ago

codyroux commented 1 week ago

Is your feature request related to a problem? Please describe. Sadly, we use choice in the proof of completeness, to pick a substitution which "lifts" an interpretation into the free magma quotiented by the laws. https://github.com/teorth/equational_theories/blob/e56c7bcc86b799cded72a3912d672fb225c9da3b/equational_theories/Completeness.lean#L106

Describe the solution you'd like Ideally, we'd determine whether that use of choice is required (I strongly suspect that it is not) and remove it if possible. It's likely some use of the excluded middle are unavoidable though.

Describe alternatives you've considered The alternative here is to do nothing.

Additional context Here is a gorgeous proof of the same (slightly more general, actually) theorem in Agda by Andreas Abel. One could simply carry out an identical proof. https://www.cse.chalmers.se/~abela/agda/MultiSortedAlgebra.pdf

teorth commented 1 week ago

While not essential to the rest of the project (at least, not yet), this is an aesthetically nice improvement to the proof, so if you want to volunteer for this project, be my guest. (It seems that you could also help get the ball rolling on formalizing the abstract nonsense chapter as well, which is a bit more tied to the rest of the project, so you could consider directing effort to that direction instead in the near-term. Of course it is up to you.)

codyroux commented 5 days ago

I'm having a rough work week, but if it's still up for grabs after I'd be happy to.

I should note that the Abel exercise doesn't actually trivially solve the problem (I now realize): it works in setoids rather than quotient types, so the "get a representative" function is trivially constructive: it's the identity. In some sense it proves something weaker: the models in which equality is an arbitrary relation are complete.

I'll have to take a closer look at the proof.