List of Formalizing Mathematical Logic in Lean

Stream: general

[SnO2WMaN]

I noticed that there're other projects working on formalization of mathematical logic in Lean 4 besides our projects (FFL). I'll note here those repositories similar aspiration to ours (still maintaining recently).

• FormalizedFormalLogic/Foundation: Maintained by @Palalansoukî and @SnO2WMaN .
  • We've done Gödel's 1st and 2nd Incompleteness for nice theory over resp. Cobham's weakest theory $\mathsf{R_0}$ and $\mathsf{I\Sigma}_1$, Moreover recently we formalized celebrating result about provability logic, Solovay's arithmetical completeness, that provability logic of $\mathsf{PA}$ is exactly modal logic $\mathsf{GL}$. Refer to README for more results (I omit about modal logic).
  • We're planning / working on
    • Classification of provability logic
    • Axiomatic set theory (ZF, ZFC): we contacts to some experts in set theory (not experts in Lean/formlization).
    • 2nd-order arithmetic
    • Bounded arithmetic
    • Functional Interpretation and related results (e.g. Gödel's T)
• staroperator/mathematical-logic-in-lean: Maintained by @Dexin Zhang
  • Gödel's Completeness Theorem, Representation Theorem of Robinson's $\mathsf{Q}$
  • 2nd-order arithmetic and ZF.
• ruplet/formalization-of-bounded-arithmetic: Maintained by @Paweł Balawender
  • About bounded arithmetic. Refer: #mathlib4 > Formalization of arithmetic: Reviewer needed!

Since these repos might be similar goals. It'd be delighted if we could exchange ideas or integrate results in some way. Let me know if there're any other repositories related mathematical logic. I'm not sure about computational theory, categorical logic, or many various area, so I have temporary omitted them from this list.

[Dexin Zhang]

Thanks for mentioning my repo :smile: I think FFL is pretty complete on collecting and formalizing results in mathematical logic, and I'm trying to make my repo as a playground of my personal ideas that FFL is not designed for, e.g. to formalize Hilbert's system or to write pure syntactic proofs. I'm definitely open to exchange ideas or integrate results anyway!

[Dexin Zhang]

By the way, I'm also working on formalizing some results about Presburger arithmetic, which are directly PRed to mathlib (see #27342 or #27100), and I know @Kenny Lau has made some work on axiomatic ZFC in #26644.

[Lukas Gerlach]

Existential rules (monsterkrampe/Existential-Rules-in-Lean) would be vaguely related. At least they form a fragment of FOL. However, my current efforts are quite different from what you people are working on. Right now, I'm mostly concerned with proving things about their reasoning algorithm called the "chase". For the chase, one can almost ignore that it's really FOL. Still, I think in the future it would make sense to make a few more connections to FOL.
So despite current efforts being sufficiently different, I just wanted to mention it here since I was not sure if the connection was obvious :)

[Thomas Waring]

cslib also has some preliminary results on logic —

• @Fabrizio Montesi & @Tanner Duve have been working on classical linear logic (sequent calculus, phase semantics)
• I have a branch with the basics of intuitionistic natural deduction (syntax, soundness & completeness of Heyting algebra semantics) — I suspected this might be duplicating work from FFL but that doesn't seem to be the case?

[Paweł Balawender]

Thanks for mentioning my repo and creating this thread! I love the work you’re doing in FFL - my work is replicating some of results you have, but in a faithful way; doing the proofs with B1-B9 axioms clearly displayed etc.

This is a big FOL project in the Rocq community: Rocq FOL Lib. They create a deep embedding of the deduction system for FOL and enable you to both prove theorems inside the weak logic, and prove meta-theorems about it such as completeness. As a matter of fact, I am currently at INRIA visiting Yannick Forster to exchange our ideas on formalization. For now I will not be able to replicate my results in their library, as it lacks some functionality I need and documentation. Ultimately though, operating in a library such as theirs (and conducting proofs in the deep embedding) would make code extraction easier, and also susceptible for formalization. I am interested to learn how the deep embeddings in Lean linked above work.

@SnO2WMaN are you interested in the style of formalization of a weaker logic that doesn’t use completeness theorem, but rather quantifies over every model and this way, enables you to transfer arithmetical proofs from paper to computer 1:1? If so, I will be glad to connect our work and, hopefully, get some of it to mathlib. My number 1 goal is to design this library in such a way that people who know logic / arithmetic, but don’t know Lean, will believe the formalization and, perhaps, will be able to write in it

[Paweł Balawender]

Thomas Waring said:

cslib also has some preliminary results on logic —

• Fabrizio Montesi & Tanner Duve have been working on classical linear logic (sequent calculus, phase semantics)
• I have a branch with the basics of intuitionistic natural deduction (syntax, soundness & completeness of Heyting algebra semantics) — I suspected this might be duplicating work from FFL but that doesn't seem to be the case?

Maybe it would be cool to create Mathlib.ProofTheory next to Mathlib.ModelTheory, where one could, in a uniform way, study all the different proof calculi we have invented over the years? Much of the machinery (such as convenient syntactical macros, substitution, variable binding) would transfer between:

• Hilbert systems (also called Frege proof systems) + results about combinatory calculus
• Gentzen's systems: PK, PJ, LK, LJ
• systems for first- and second-order logic / for typed lamda calculi / for propositional calculus, quantifier propositional calculus etc.
• proof systems such as cutting planes and resolution

To be honest, even having the definitions and history of all of these in a single place would be a huge added value :)

[SnO2WMaN]

Thomas Waring said:

cslib also has some preliminary results on logic —

• Fabrizio Montesi & Tanner Duve have been working on classical linear logic (sequent calculus, phase semantics)
• I have a branch with the basics of intuitionistic natural deduction (syntax, soundness & completeness of Heyting algebra semantics) — I suspected this might be duplicating work from FFL but that doesn't seem to be the case?

In FFL, we also have formalizations of intuitionistic propositional logic as well as superintuitionistic propositional logics. Most of these are defined in the Hilbert style and studied via Kripke semantics, but it should also be possible to approach them through algebraic semantics. Please take a look at the following link. (In the latest branch, the work is still in progress and the code is quite messy!)

https://github.com/FormalizedFormalLogic/Foundation/tree/a8ac03ddfb54dd30c3f13b603a20088ba81535cd/Foundation/Propositional

[Fabrizio Montesi]

Paweł Balawender said:

Thomas Waring said:

cslib also has some preliminary results on logic —

• Fabrizio Montesi & Tanner Duve have been working on classical linear logic (sequent calculus, phase semantics)
• I have a branch with the basics of intuitionistic natural deduction (syntax, soundness & completeness of Heyting algebra semantics) — I suspected this might be duplicating work from FFL but that doesn't seem to be the case?

Maybe it would be cool to create Mathlib.ProofTheory next to Mathlib.ModelTheory, where one could, in a uniform way, study all the different proof calculi we have invented over the years? Much of the machinery (such as convenient syntactical macros, substitution, variable binding) would transfer between:

• Hilbert systems (also called Frege proof systems) + results about combinatory calculus
• Gentzen's systems: PK, PJ, LK, LJ
• systems for first- and second-order logic / for typed lamda calculi / for propositional calculus, quantifier propositional calculus etc.
• proof systems such as cutting planes and resolution

To be honest, even having the definitions and history of all of these in a single place would be a huge added value :)

Thanks for the mention, this is very interesting.

There's a big Logics directory in cslib, where we aim at having these and more (well, lambda calculus lives in Languages), including also different kinds of modal logics.
I started from the sequent calculus of classical linear logic just because I know it by heart, but I'd like to work actively on finding common pattern, developing encodings between logics, applying these logics to various problems, etc.

I'll have a look at the other pointers asap. If there's interest in discussing a joint effort (I have it!), I'd be happy to support it in cslib.

[SnO2WMaN]

Paweł Balawender said:

SnO2WMaN are you interested in the style of formalization of a weaker logic that doesn’t use completeness theorem, but rather quantifies over every model and this way, enables you to transfer arithmetical proofs from paper to computer 1:1? If so, I will be glad to connect our work and, hopefully, get some of it to mathlib. My number 1 goal is to design this library in such a way that people who know logic / arithmetic, but don’t know Lean, will believe the formalization and, perhaps, will be able to write in it

Paweł Balawender said:

Maybe it would be cool to create Mathlib.ProofTheory next to Mathlib.ModelTheory, where one could, in a uniform way, study all the different proof calculi we have invented over the years? Much of the machinery (such as convenient syntactical macros, substitution, variable binding) would transfer between:

• Hilbert systems (also called Frege proof systems) + results about combinatory calculus
• Gentzen's systems: PK, PJ, LK, LJ
• systems for first- and second-order logic / for typed lamda calculi / for propositional calculus, quantifier propositional calculus etc.
• proof systems such as cutting planes and resolution

To be honest, even having the definitions and history of all of these in a single place would be a huge added value :)

My specialty is modal logic, so I’m not especially interested in the approach that converts pen-and-paper proofs from bounded arithmetic or arithmetic in general into Lean proofs — sorry. I might be happy if someone could convert Lean proofs into the deep-embedded FOL-Formalized-in-Lean style, but that feels like a different goal.

From our perspective, porting formal-logic results into mathlib as a general library is not very realistic or practical. Since logical systems tend to be adapted to concrete applications, small differences between a canonical library and a project’s custom implementation can cause large mismatches, and at that point providing a single library doesn’t make much sense.
That said, IMO, the FOL part of FFL is well thought-out, and its notation is in many ways more polished than mathlib’s (I haven’t been involved in that work, the whole design is by @Palalansoukî ). You may compare ZFC PR in Mathlib #26644 and the current ZFC development in FFL (defining axioms and model discussion)
At the very least, I would personally be inclined to keep something like Mathlib.ProofTheory self-contained inside FFL/Foundation rather than trying to force it into mathlib.

[SnO2WMaN]

To expand on what I want to do within FFL, my focus is on modal logic.
Specifically, I want to formalize various sequent calculi for modal logic (for example, labeled sequent calculi, hypersequent calculi, display calculi, etc.), show their equivalences, and work on automating in modal logic. The latter seems feasible using labeled sequent calculi or tableau calculi. Achieving this would allow for a significant reduction in the size of modal-logic code. Currently, writing formal proof in modal logic is quite messy, for example, something as basic as the duality of □ and ◇ becomes extremely cumbersome if one doesn’t appeal to Kripke semantics once things get slightly complex. Auto-proving would be very convenient, but I don’t have much prior experience with formalization in this area. I would greatly welcome collaboration from anyone who has expertise in this aspect.

[Palalansoukî]

Hi @Paweł Balawender . I was impressed by how you are formalizing difficult results.

Paweł Balawender said:

SnO2WMaN are you interested in the style of formalization of a weaker logic that doesn’t use completeness theorem, but rather quantifies over every model and this way, enables you to transfer arithmetical proofs from paper to computer 1:1? If so, I will be glad to connect our work and, hopefully, get some of it to mathlib. My number 1 goal is to design this library in such a way that people who know logic / arithmetic, but don’t know Lean, will believe the formalization and, perhaps, will be able to write in it

I might be misunderstanding something, but I think this is the same as our approach.

For example, we formalized the well-known result that the graph of an exponential function is definable by a $\Delta_0$-formula and its inductive property is provable in $\mathsf I\Delta_0$ , showing that this holds for every quantified model V of $\mathsf I\Delta_0$ ([ORingStruc V] indicates that V has a interpretation of language of arithmetic, and [V ⊧ₘ* 𝗜𝚺₀] indicates that V is a model of $\mathsf I\Delta_0$). We do not use the completeness theorem in this proof itself; rather, we use it to obtain the existence of a formalized proof (LK, Hilbert-style, Tait-style, ... etc) from this fact.

[Paweł Balawender]

Palalansoukî said:

Hi Paweł Balawender . I was impressed by how you are formalizing difficult results.

Paweł Balawender said:

SnO2WMaN are you interested in the style of formalization of a weaker logic that doesn’t use completeness theorem, but rather quantifies over every model and this way, enables you to transfer arithmetical proofs from paper to computer 1:1? If so, I will be glad to connect our work and, hopefully, get some of it to mathlib. My number 1 goal is to design this library in such a way that people who know logic / arithmetic, but don’t know Lean, will believe the formalization and, perhaps, will be able to write in it

I might be misunderstanding something, but I think this is the same as our approach.

For example, we formalized the well-known result that the graph of an exponential function is definable by a $\Delta_0$-formula and its inductive property is provable in $\mathsf I\Delta_0$ , showing that this holds for every quantified model V of $\mathsf I\Delta_0$ ([ORingStruc V] indicates that V has a interpretation of language of arithmetic, and [V ⊧ₘ* 𝗜𝚺₀] indicates that V is a model of $\mathsf I\Delta_0$). We do not use the completeness theorem in this proof itself; rather, we use it to obtain the existence of a formalized proof (LK, Hilbert-style, Tait-style, ... etc) from this fact.

Wow, it sounds like our approaches are the same indeed. I remember our previous discussion, from which I got the feeling that you conduct the proofs in the actual Lean model. But now that I read your code again, I see that we are essentially doing the same thing. What tricked me is that you very early prove scoped instance : IsStrictOrderedRing M and then use theorems from Mathlib.Algebra, so the usage of actual Peano axioms is hidden in the later theorems.

[Palalansoukî]

Paweł Balawender said:

What tricked me is that you very early prove scoped instance : IsStrictOrderedRing M and then use theorems from Mathlib.Algebra, so the usage of actual Peano axioms is hidden in the later theorems.

The reason we defined this kind of instances is that models of even very weak arithmetic (here $\mathsf{PA^-}$) satisfies convenient algebraic structures. This allows us to use theorems from mathlib concerning algebra, and potentially even automatic proofs, making proofs about these models simpler.

[Paweł Balawender]

I think that what I'll do is leave my code in the current style (i.e. proving properties from scratch in IDelta0), as it better serves the purpose of formalizing Logical Foundations in a didactic way. Somewhat similarly to Terrence Tao's formalization of his 'Analysis' textbook - proofs could be written in a simpler way, but he decided to keep them as-is to be closer to what's in the book.

However, for formalization of the field, your approach of utilizing Mathlib.Algebra is more scalable and I'll be glad to help pushing a part of FFL (e.g. $I\Delta_0$ up to inductive property of exp) into mathlib!