Our tech stack is ontological:
Hardware — Physics
Software — Mathematics
Our engineering workflow is simple: discover, build, grow, learn & teach
Acknowledgment
We humbly thank the collective intelligence of humanity for providing the technology and culture we cherish. We do our best to properly reference the authors of the works utilized herein, though we may occasionally fall short. Our formalization acts as a reciprocal validation—confirming the structural integrity of their original insights while securing the foundation upon which we build. In truth, all creative work is derivative; we stand on the shoulders of those who came before, and our contributions are simply the next link in an unbroken chain of human ingenuity.
Machine-checked formalization of the semantic Grz.2 classification for the category of sets. This project proves that modal formulas valid on all finite Boolean frames coincide with those valid at the bottom world of all finite join-semilattices — the semantic characterization of the modal logic Grz.2 — and establishes the complete paper-row correspondence for infinite-world partition elimination in both the all-functions and surjections subcategories.
A Lean 4 formalization (37 modules, 8253 lines, 376 theorems, 0 sorry) proving the semantic Grz.2 modal theory classification for the category of sets, including Kripke frame semantics, finite Boolean frame validity, and infinite-world partition elimination.
| Metric | Value |
|---|---|
| Lean modules | 37 |
| Total lines | 8,253 |
| Theorems | 376 |
| Definitions | 192 |
| Sorry count | 0 |
| Lean toolchain | v4.24.0 |
| Mathlib | v4.24.0 |
FormulaTheory.Grz2— The semantic Grz.2 theory: formulas valid on all finite Boolean frames.FormulaTheory.Grz2FiniteJoinSemilattice— Equivalent characterization: truth at the bottom world of every finite join-semilattice with bottom.grz2_iff_validAtBottomAllFiniteJoinSemilattices— The two characterizations are equivalent.infsets_formulaic_grz2_upper_bound_at_nat_root— Classification: Grz.2 membership ↔ validity on all infinite-world all-functions substitution instances at ℕ root.infsurj_formulaic_grz2_upper_bound_at_nat_root— Same classification for the surjections subcategory.
This formalization internalizes semantic Grz.2 as formulas valid on all finite Boolean frames. It does not claim a full internal Hilbert calculus or syntactic completeness proof for Grz.2. The classification is frame-semantic: the space of valid formulas is characterized by finite-frame conditions and infinite-world partition elimination, not by derivability in a proof system.
The formalization proves that each standard modal axiom belongs to the semantic Grz.2 surface:
grz2_of_axiomT— Reflexivity axiom Tgrz2_of_axiom4— Transitivity axiom 4grz2_of_axiomDot2— Directedness axiom .2grz2_of_axiomGrz— Grz axiom (Grzegorczyk)
HeytingLean.ModalCategorySets
├── Basic.lean (root import)
├── Propositional/
│ ├── Core.lean (formulas, models, satisfaction, validity)
│ ├── Axioms.lean (K, T, 4, 5, .2, .3, Triv, Grz)
│ ├── Frames.lean (reflexive, linear-order, directed frames)
│ ├── Substitution.lean (propositional substitution + closure)
│ └── Theories.lean (FormulaTheory.Grz2, axiom membership)
├── Framework/
│ ├── AssertionSemantics.lean (truth invariance, modal trivialization)
│ ├── EqualityLanguage.lean (equality-modal assertion language)
│ ├── EqualityMorphismBridge.lean (morphism classes ↔ modal formulas)
│ ├── FiniteCorrespondence.lean (partition ↔ surjective map)
│ ├── FiniteSententialCorrespondence (sentential row packaging)
│ ├── FiniteStateFrames.lean (lollipop + partition frames)
│ ├── FiniteTranslation.lean (finite formulaic translation)
│ ├── GuardedBooleanTransfer.lean (Boolean frame ↔ guarded substitution)
│ ├── InfiniteButtons.lean (button pattern machinery)
│ ├── InfiniteButtonsAudit.lean (button audit & witness verification)
│ ├── InfiniteGuardedButtons.lean (guarded infinite button patterns)
│ ├── InfinitePartitionElimination (partition elimination for ∞ worlds)
│ ├── KripkeCategory.lean (Kripke-categorical semantics)
│ ├── PartitionFormulas.lean (partition formula encoding)
│ ├── PartitionModalCorrespondence (partition ↔ modal frame)
│ ├── PureFormulaElimination.lean (pure formula elimination lemma)
│ ├── SubstitutionPartitionCorresp. (substitution↔partition bridge)
│ ├── SubstitutionValidity.lean (substitution preserves validity)
│ └── TypeWorlds.lean (type-theoretic world construction)
└── Validities/
├── BooleanFrames.lean (finite Boolean frame validity)
├── Concrete.lean (concrete frame instances)
├── ConcreteLocal.lean (local concrete frame lemmas)
├── ControlCore.lean (T+4+.2+Grz control core)
├── ControlStatements.lean (control statement packaging)
├── FiniteControlFrames.lean (finite frames validate control core)
├── FiniteLatticeCharacterization (Boolean ↔ join-semilattice equiv)
├── GrzFinite.lean (Grz on finite frames)
├── PaperRows.lean (full paper-row correspondence)
├── Pointed.lean (pointed frame validity)
├── PointedLabeling.lean (cardinality label realization)
└── S4Universal.lean (S4 universal validity)
# 1. Install Lean 4.24.0 via elan
curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh
# 2. Clone and build
git clone https://github.com/Abraxas1010/modal-category-of-sets-lean.git
cd modal-category-of-sets-lean
lake buildThe first build fetches Mathlib v4.24.0 and its dependencies (~15-30 minutes).
See docs/theorem_inventory.md for a complete enumeration of all 376 theorems with module paths, declaration names, and one-sentence descriptions.