List of Mathematical Logic Formalization

Stream: general

[SnO2WMaN]

Hello. We're currently working on formalizing mathematical logics in Lean4 and its documentation.

We have a list of related works of formalization of all fields of logics (including modal logics and non-classical logic) with theorem prover (Lean 4, Lean 3, Isabelle, Coq, etc.) as far as we know.
If you know anything not on this list, please let us know.

Thanks.

[Luigi Massacci]

I was about to tell you to check out lean4-logic, but then I noticed the actual URL :rolling_on_the_floor_laughing:

[SnO2WMaN]

edited. sorry confusing.

[Yaël Dillies]

You're missing Con(NF)

[Luigi Massacci]

For Coq there was also this formalisation of propositional calculi by @Floris van Doorn , and I participated two years ago in this project, that along the way formalised an intuitionistic version of the Calculus of Structures in Coq. There’s also some lean3/lean4/isabelle related work there, but the full formalisation (with some soundness results as well) is only for Coq. This is the GitHub repo

[SnO2WMaN]

Ah, I forgot to mention that more works to add on this PR. I checked many Coq implementation.

https://github.com/iehality/lean4-logic/pull/79

[Jason Rute]

For Lean 3 and 4, have you included the stuff mentioned in #Is there code for X? > Completeness theorem for first-order logic and #general > Gödel's first incompleteness theorem ?

[Jason Rute]

I’m not sure if you would consider formalization of type theory based logics to be in scope, but there are a lot of meta-theorems about the logics of the various provers. For example, https://link.springer.com/chapter/10.1007/11814771_17

[SnO2WMaN]

Jason Rute said:

For Lean 3 and 4, have you included the stuff mentioned in #Is there code for X? > Completeness theorem for first-order logic and #general > Gödel's first incompleteness theorem ?

Of course included (because these result are exactly the result of lean4-logic, i.e. this list hosted on)