Apoth3osis
>_PAPER_PROOF_CODE/MODAL_CATEGORY_OF_SETS

Modal Theory of the Category of Sets

Semantic Grz.2 Classification — Formalized in Lean 4

Formalization: Apoth3osis Labs|GitHub: modal-category-of-sets-lean
>_VERIFICATION.SEAL
FORMALLY VERIFIED • LEAN 4 • MACHINE-CHECKED • APOTH3OSIS∀∃⊢→∧∨¬≡QED376 theorems • 0 sorry37 modules0 SORRY

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.

376 THEOREMS VERIFIED37 MODULES8,253 LINES0 SORRY

Modal Theory of the Category of Sets • Lean 4 + Mathlib • Apoth3osis Labs

37
Modules
Lean 4 source files
376
Theorems
Machine-checked
8,253
Lines
Total Lean code
0
Sorry
Complete verification

Key Mathematics

MAIN DEFINITION
Grz.2  :=  { φ∣φ valid on all finite Boolean frames (P(Fin n), ⊆) }\text{Grz.2} \;:=\; \{\,\varphi \mid \varphi \text{ valid on all finite Boolean frames } (\mathcal{P}(\text{Fin}\,n),\, \subseteq)\,\}

FormulaTheory.Grz2 — the semantic characterization of the modal logic Grz.2 as a formula theory

CROWN THEOREMS
QED
Grz.2(φ)    ⟺    φ true at ⊥ of every finite join-semilattice\text{Grz.2}(\varphi) \;\iff\; \varphi \text{ true at } \bot \text{ of every finite join-semilattice}

grz2_iff_validAtBottomAllFiniteJoinSemilattices

QED
Grz.2(φ)    ⟺    ∀n, val,  HoldsInfAll(idN, n, val, φ)\text{Grz.2}(\varphi) \;\iff\; \forall n,\,\text{val},\; \text{HoldsInfAll}(\text{id}_{\mathbb{N}},\, n,\, \text{val},\, \varphi)

infsets_formulaic_grz2_upper_bound_at_nat_root — classification via all-functions substitution at natural number root

QED
Grz.2(φ)    ⟺    ∀n, val,  HoldsInfSurj(idN, n, val, φ)\text{Grz.2}(\varphi) \;\iff\; \forall n,\,\text{val},\; \text{HoldsInfSurj}(\text{id}_{\mathbb{N}},\, n,\, \text{val},\, \varphi)

infsurj_formulaic_grz2_upper_bound_at_nat_root — classification via surjections substitution at natural number root

SEMANTIC BOUNDARY

This formalization internalizes semantic Grz.2\text{Grz.2} as the class of formulas valid on all finite Boolean frames. The classification is frame-semantic: the space of valid formulas is characterized by finite-frame conditions and infinite-world partition elimination. It does not claim a full internal Hilbert calculus or syntactic completeness proof for Grz.2. The individual axioms T, 4, .2, and Grz are proved to belong to the semantic theory, but derivability in a proof system is not formalized.

Proof Blueprint

Verified Lean Artifacts

This project ships as a Lean-first artifact package. All 37 source modules are available for download and independent verification.

LEAN PROOFS (tar.gz)VIEW ON GITHUB

Resources

GITHUB
Standalone public repo with build instructions and theorem inventory
RESEARCH
Research project page with verification context
ALL PROJECTS
Browse all Paper → Proof → Code projects