Obelisk is an interactive proof assistant engineered for mathematical clarity and high assurance. Featuring an LCF-style trusted kernel in Standard ML, declarative syntax, and rigorous class theory foundations.
Every statement is formally decoupled into Morse–Kelley Semantic Objects and Ambient Type-Theoretic Syntactic Side Conditions. Browse the honestly ML-generated catalog in generated/manual.html, generated/variant1.html, generated/variant2.html, or the archived frozen/ directory.
In standard ZFC and dependent type systems (Lean 4, Coq), collections like the universal class \(V\) or the category of all sets \(\mathbf{Set}\) cannot be manipulated as ordinary elements without triggering Russell's paradox or ascending into infinite universe hierarchies (Type u).
Obelisk adopts Morse–Kelley (MK) class theory: proper classes are native first-class objects with full impredicative comprehension over classes.
Standard Kuratowski pairs \((\langle A, B \rangle = \{\{A\}, \{A, B\}\})\) fail for proper classes because proper classes cannot be elements of sets. Obelisk solves this via Dunaev Tagged Pairs \(([A, B]_D = (\mathrm{mark}(A, 1) \cup \mathrm{mark}(B, 2)))\), allowing proper classes and infinite families to form pairs and lists with minimal rank growth and full algebraic projection injectivity.
Type-theoretic proof assistants suffer from fragile computational reduction (\(\beta\delta\iota\)): definition updates break proof scripts invisibly. Obelisk separates syntax from semantics through the explicit valuation bracket \(\llbracket \cdot \rrbracket\). Every deduction is a checkable syntactic tree; inference rules have explicit side conditions with no hidden normalization noise.
The prover and its generated manual are continuously re-audited. These are the latest changes now visible in the Theory Manual and the publication PDFs.
(([A,B]D = [C,D]D) → ((A = C) ∧ (B = D))) is now proved for arbitrary classes
(proofDunaevPairInjectivity and surface dunaev_pair_injective).
The general Pair/Func interface no longer falls back to Kuratowski pairs.
ThmWithPrf.cheat now raises, and derive, check,
slow_check, and checkPlus all reject PCheat_prf.
Unsupported legacy PS1_prf/PHenkin_prf constructors fail explicitly. A closedness gate also rejects theorem statements with free class variables, so an open formula cannot be packed as a Set witness.
The dependent catalog now reports 77 derived proofs, 16 conservative definitions, and 7 irreducible MK axioms (100 certified items total). Plan witnesses are classified, and an unclassified witness prevents the catalog from loading.
Inspect the catalog →
All 100 machine-checked NBG records are now generated directly by nbg_html_generator.ML,
including Dunaev pair injectivity, dependent Σ/Π models, and Cartesian-product elimination (dunaev_cartesian_elim), with algorithmic symbol links in Unicode and LaTeX.
ℰ (sEau, \mathcal{E}) is an elementary metatheory chosen from {IΣ1, 𝒯, NBG, MK}—not Robinson's Q, which lacks the Σ1-induction required for HBL Condition D3 (Hájek & Pudlák 1993; Bezboruah & Shepherdson 1976; Boolos 1993).
ℱ (sFau, \mathcal{F}) is a non-r.e. sound Henkin-complete extension of the r.e. base theory 𝒯 where Co-Necessitation (4.03) is justified by Soundness (3.73).
μA transforms typed terms of sort A into Class terms under a fixed background model and variable valuation.
Legacy hand-authored pages (embedding_anti.html, archive/*.html) are preserved with explicit (deprecated) banners pointing to their live Poly/ML-generated replacements in generated/ and the interactive split-view portal embedding.html.
Toggle between formal mathematical notation (Unicode / LaTeX) and concrete executable SML/Obelisk syntax. Side conditions are made fully visible and explicit.
Significantly reduces the steep learning curve for working mathematicians.
Eliminates opaque tactic noise (intro, apply, rewrite) and normalisation tricks.
Every proof step forms an explicit, checkable syntactic tree without hidden reduction steps.
Constructs a new high-assurance language with full polymorphism (types depending on values) by introducing a clean abstraction and code-generation layer above the verified CakeML compiler.
Modernized Morse–Kelley (MK) class-theoretic foundations equipped with Tarski–Grothendieck universes, regularity via powerclasses (∈-induction), and an innovative independent construction of tagged pairs and lists for proper classes.
In Obelisk, we establish a strict 1-to-1 Curry–Howard correspondence between mathematical theorems of Morse-Kelley (MK) Impredicative Class Theory and compiler types. Because MK allows quantification over proper classes in class comprehension, it provides the full expressive strength of higher-order logic over sets, while the compiler operates under the foundational principle: it compiles not to generate runtime executable bytecode, but strictly to verify whether the proof expression type-checks.
Eliminates dynamically typed languages like Python from the trusted kernel. Fully written in Standard ML 97 targeting the CakeML verified compiler for machine-code assurance down to silicon.
Every mathematical theorem (Modus Ponens, Conjunction Symmetry, Russell Paradox Refutation) corresponds to a unique type. Proof terms are formal witnesses checked by the SML type checker.
Replaces Kuratowski pairs (which collapse on proper classes) with [A, B]_D tagged pairs that preserve well-foundedness and algebraic projections without universe elevation.
Validates all 69 core catalog entries, 90 verified higher-order theorems, and 30 NBG standard library theorems in <50 MB RAM under Poly/ML & CakeML or zero-install browser JS, contrasting with multi-gigabyte JVM/LSP heaps.
| Surface Declaration | Kernel AST Category | Example in .nbg Surface Language |
Checked by NBGCompiler.typeCheck |
Epistemic Meaning |
|---|---|---|---|---|
formula F = ...; |
Type Definition (Fm / NBGCompiler.Type) |
formula False_RussellIsSet = Set({ x | ((x in x) -> Bot) });(ASCII Set(X) compiles to catalog isSet(X)) |
Verifies syntactic well-formedness & Stage I/II quantifier bounds | Defines a proposition (Type) — even a false/uninhabited one. Never proves a theorem! |
theorem T : F = e; |
Proof Term (NBGCompiler.Expr) |
theorem thm_russell_not_set : (Set(R) -> Bot) = fn (hSet : Set(R)) => ...; |
Synthesizes exact type of term e via NBGCompiler.typeCheck and verifies definitional (α/β/δ) equivalence with F |
Constructive witness inhabiting type F. Uninhabited/false formulas are deterministically rejected (relative to MK/NBG consistency). |
| System | Logical Foundation | Proof Execution | Trusted Kernel | Mathematical Workflow |
|---|---|---|---|---|
| Obelisk | Morse–Kelley Class Theory + Tarski Universes | Zero Implicit Computation (Syntactic Trees) | Small LCF Kernel (~20k LOC SML) | Declarative, human-readable, stable under definition updates |
| Lean 4 | Calculus of Inductive Constructions (CIC) | Type reduction, unification, tactic elaboration | Complex C++ kernel + elaborator | Tactic-heavy, dependent types, steep learning curve |
| Rocq (Coq) | Calculus of Inductive Constructions (CIC) | Computational reduction (β, ι, δ) | OCaml kernel (~30k LOC) | Constructive type theory, Ltac scripting |
| Isabelle/ZF | ZFC over Higher-Order Logic (Isabelle/Pure) | Term rewriting, tableau provers, Sledgehammer | Standard ML LCF kernel | Isar declarative proofs, Isabelle framework |
| Metamath | First-Order Logic + Set Theory (ZFC) | Pure syntactic replacement & verification | Minimalist (~1k LOC) | Very low-level, lacks higher polymorphism & reflection |
Live demonstration of Obelisk proofs, axiomatics, and mathematical derivations directly from the kernel.
