Preterms/Terms, Preformulas/Formulas

Stream: Is there code for X?

[Giacomo Maletto]

Me and a friend would like to develop some basic facts about model theory, just for fun.
Is there code for terms/formulas?

Actually, I found it here: https://flypitch.github.io/
But why are the definitions of preterms/preformulas defined only there and not in the main library?

[Kevin Buzzard]

Because nobody ported them to the main library yet

[Kevin Buzzard]

I have an MSc student who is going to attempt Ax-Grothendieck in Lean. @Yakov Pechersky kindly bumped one of the flypitch files so that it compiles with mathlib master and he's using that

[Johan Commelin]

@Giacomo Maletto There is a file model_theory.basic in mathlib. But that's it. The rest is in Flypitch

[Giacomo Maletto]

I see, makes sense
I can try to port the basic definitions/facts about terms and formulas in Mathlib

[Giacomo Maletto]

Or start from what @Yakov Pechersky has already done, if I can have access to that work

[Yakov Pechersky]

I'll see if the fork I have is up to date

[Yakov Pechersky]

@Giacomo Maletto If you only care about the fol file, you can start with this:
https://github.com/pechersky/flypitch/tree/3.33.0

[Giacomo Maletto]

Ok, I'll start by tinkering with these files. Thanks a lot!