Need for rewriting proof theory from flypitch (Lean 3)

Stream: mathlib4

[Paweł Balawender]

Hey, I am doing some proof-theoretical work. It involves defining first-order logic in Lean 4 as a deep embedding (i.e. i define what a variable is, i define a formula as an inductive type etc.). There are many design decisions involved, fortunately we have Mathlib.ModelTheory module which has well-designed code for defining formulas. But the module is about model theory and not proof theory, so there is no notion of 'provability' there. Provability was used in the Flypitch project, but this code is in Lean 3. I think it would be a nice addition to Mathlib 4, if I'm not blind and it really is not there. So, to add to mathlib code for:

• binding a free variable in a formula by a quantifier (ModelTheory is very close to implementing it but it is not convenient)
• defining a proof system with conjunction elimination, disjunction introduction, modus ponens etc.
• defining what it means for a sentence to be provable from axioms
• defining induction / min / max / comprehension rules for different classes of formulas
  and so on. Do you agree it would make sense to start the project of adding this to mathlib?

[Aaron Liu]

There is https://github.com/FormalizedFormalLogic/Foundation if you didn't know about it

[Paweł Balawender]

Wow! This is interesting to me, thank you!