Discussion: FormalizedFormalLogic

Stream: general

[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.