Modal Theory of the Category of Sets
Semantic Grz.2 Classification — Formalized in Lean 4
Formal Verification Certificate
Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.
Modal Theory of the Category of Sets • Lean 4 + Mathlib • Apoth3osis Labs
Research Objective
Characterize the modal theory of the category of sets at the semantic level. The category of sets, viewed through equality-modal logic, gives rise to a Kripke-categorical structure where worlds are types and accessibility is mediated by functions (all functions) or surjections. The central question: which propositional modal formulas are valid on this structure?
The answer is Grz.2 — the modal logic extending S4 with the Grzegorczyk axiom and the directedness axiom. This formalization proves the classification at the semantic level: a formula belongs to the theory if and only if it is valid on all finite Boolean frames, or equivalently, true at the bottom world of every finite join-semilattice with bottom.
Semantic boundary: This is a frame-semantic characterization, not a syntactic completeness proof. The formalization does not construct an internal Hilbert calculus for Grz.2.
Key Results
FormulaTheory.Grz2The semantic Grz.2 theory defined as the class of formulas valid on all finite Boolean frames
grz2_iff_validAtBottomAllFiniteJoinSemilatticesBoolean frame validity is equivalent to bottom-validity on all finite join-semilattices
infsets_formulaic_grz2_upper_bound_at_nat_rootCrown classification: Grz.2 membership via all-functions substitution instances at the natural number root
infsurj_formulaic_grz2_upper_bound_at_nat_rootCrown classification: Grz.2 membership via surjections substitution instances at the natural number root
infsets_formulas_partition_normal_formEvery equality-modal formula on an infinite world reduces to a finite disjunction of partition formulas
infsets_sentences_truth_invariantClosed equality-modal sentences are truth-invariant across all infinite worlds of the all-functions subcategory
Module Architecture
- Core — formulas, models, satisfaction
- Axioms — K, T, 4, 5, .2, .3, Triv, Grz
- Frames — reflexive, linear-order, directed
- Substitution — propositional substitution
- Theories — Grz.2 definition + axiom membership
- AssertionSemantics — truth invariance
- EqualityLanguage — equality-modal assertions
- GuardedBooleanTransfer — Boolean-to-infinite bridge
- InfiniteButtons — button pattern machinery
- InfinitePartitionElimination — core elimination
- KripkeCategory — categorical semantics
- + 14 supporting modules
- BooleanFrames — finite Boolean frame validity
- FiniteLatticeCharacterization — semilattice equiv
- PaperRows — crown classification theorems
- ControlCore — T+4+.2+Grz lower bounds
- GrzFinite — Grz on finite preorders
- S4Universal — universal S4 validity
- + 6 supporting modules
Resources
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.