Discussion: FormalizedFormalLogic

Stream: Formalized Formal Logic

[SnO2WMaN]

Memo: # FFL is not planed porting to Mathlib.

[Palalansoukî]

Discussion thread for #announce > FormalizedFormalLogic .

[Kim Morrison]

I'm curious, what subset of Mathlib do you depend on?

[Notification Bot]

A message was moved here from #announce > FormalizedFormaliLogic by Kevin Buzzard.

[Palalansoukî]

It relies on many of the fundamental theorems in Mathlib.Data and several complements in computability theory in Mathlib.Computability. Additionally, it depends on Mathlib.Algebra and Mathlib.Order for the model theory of arithmetic. However, it does not rely on Mathlib.ModelTheory for reasons discussed in #maths > Gödel's Incompleteness Theorem.

[SnO2WMaN]

Passing 9 month, There are many progress since this announcement #announce > FormalizedFormalLogic .
However we didn't write any reports. This is not good situation, we've decided to start writing monthly report.

Here is 2025/10 report: https://formalizedformallogic.github.io/Foundation/book/Monthly-Reports/Monthly-Report-2025___10/

I'd like to open thread for the October report, so please add _Formalized Formal Logic_ to the Projects topics on Zulip, as FLT-regular, etc. I'm not sure who I should ask, so it'd be helpful if the appropriate person could take care of it.

[Notification Bot]

This topic was moved here from #general > Discussion: FormalizedFormalLogic by Bryan Gin-ge Chen.

[Matt Diamond]

I'm curious why you needed to define your own model theory API instead of building upon Mathlib's. You have some great results and it's a shame that they aren't interoperable with Mathlib. (Though perhaps it isn't too hard to translate them to Mathlib's version... that could be a fun project.)

[Palalansoukî]

Matt Diamond said:

I'm curious why you needed to define your own model theory API instead of building upon Mathlib's. You have some great results and it's a shame that they aren't interoperable with Mathlib. (Though perhaps it isn't too hard to translate them to Mathlib's version... that could be a fun project.)

The reason is that the intended meaning of language in FFL differs from the one used in Mathlib. In Mathlib, the existence of the equality symbol is implicitly assumed, since equality is defined for all formulas regardless of their languages. But in FFL, the equality symbol is treated as one of the relational symbols, because we want to work in a more general setting (I understand this is convenient in the context of model theory, but we put more importance on proof theory).

For theories with equality, creating mutual translations is certainly straightforward. One need only add or remove the equality symbol, or simply define it redundantly through an obvious interpretation.