1000 Theorems about Mathematical Logic

Stream: Formalized Formal Logic

[SnO2WMaN]

In Category 03 of https://1000-plus.github.io/all at least, following problems was already formalized in FFL.

• Deduction theorem for various systems (not modal logic, it cannot be hold)
• Cut-elimination theorem for predicate logic
• Glivenko's theorem for propositional and predicate logics
• Soundness theorems for various systems among prop, pred, modal, etc.
• (Gödel's) completeness theorem (Gödel's one is for predicate, and we proved more systems)
• Tarski's indefinability theorem

I'll make PR for 1000-plus later, and more, I think, some remained problems is not so hard from now results, e.g. Craig's Interpolation Theorems (for propositional/modal/predicate logics), etc.

[Palalansoukî]

It should be noted that some of these theorems (e.g. soundness theorem, completeness theorem) are already formalized in flypitch.

[SnO2WMaN]

Update mathlib's 1000.yaml

• Fix URL of Gödel's Incompleteness: mathlib#33774
• Tarski's Undefinability Theorem: mathlib#33753

After I'll send about Löb's theorem

[SnO2WMaN]

Löb's Theorem in mathlib#34574