Reservoir

Foundation

Formalizing mathematical logics in Lean 4.

Summary

Main Result in this repository. More results and details are in Book and Doc.

• Propositional Logic
  • Tait-style calculus and completeness
  • Completeness for Kripke semantics
  • Disjunctive Property of intuitionistic logic
  • Rejection Law of Excluded Middle in intuitionistic logic and sublogic relations
• First-Order Logic and Arithmetics
  • Completeness Theorem
  • Gödel-Gentzen Translation
  • Cut-elimination of first-order sequent calculus (Gentzen's Hauptsatz)
  • Arithmetic and Arithmetization
  • Gödel's First and Second Incompleteness Theorems
• Basic Modal Logic (with modal operators )
  • Kripke completeness for well-known subsystems
  • Modal Cube, and sublogic relations for other logics
  • Gödel-McKinsey-Tarski Theorem and Modal Companions
• Provability Logic
  • Solovay's Arithmetical Completeness Theorem for GL

Documents

• Book, summary of results.
• Doc, documentation generated by doc-gen4.

Sponsor

This project is supported by Proxima Technology.