OPA

Propositions-as-Types Walkthrough: Separating formula (Type Definition) from theorem (Kernel-Checked Proof Term) Checked deterministically by NBGCompiler.typeCheck

⚡ Open Interactive Compiler in repl.html →

Declaration Construct	Kernel AST Role	Example in `.nbg` Surface Syntax	Verification Action in `NBGCompiler.typeCheck`	Can a False MK Statement Pass?
`formula F = ...;`	Type Definition (`NBGCompiler.Type` / `Fm`)	`formula False_RussellIsSet = Set({ x \| ((x in x) -> Bot) });` (`.nbg` ASCII `Set(X)` compiles to catalog `isSet(X)`)	Checks syntactic sort well-formedness & Stage I/II comprehension bounds	Yes as an uninhabited Type (defining a proposition never proves it!)
`theorem T : F = e;`	Proof Term Witness (`NBGCompiler.Expr`)	`theorem empty_class_no_elements : (forall (z:Class). ((z in {x \| Bot}) -> Bot)) = Lam (z:Class) => ...;` (and `theorem thm_russell_not_set : (Set(R) -> Bot) = ...;`)	Bidirectionally synthesizes type of proof term `e` via `NBGCompiler.typeCheck` and checks definitional (α/β/δ) equivalence with `F`	Never (relative to MK/NBG consistency) — every candidate term for an uninhabited type is deterministically rejected

4-Step Walkthrough of empty_class_no_elements : ∀(z : Class) ((z ∈ {x | ⊥}) → ⊥): (Note: in .nbg ASCII surface syntax, Set(z) is the surface keyword for the sethood predicate rendered as isSet(z) in the Unicode/LaTeX catalog.)

Step 1 · Universal Intro (ELam)
Lam (z:Class) => ... introduces fresh class parameter z into context Δ.

Step 2 · Implication Intro (EFn)
fn (hIn : (z in {x | Bot})) => ... adds antecedent hypothesis hIn to proof context Γ.

Step 3 · Comprehension Axiom (ECompr)
compr(x. Bot, z) synthesizes ((z in {x | Bot}) <-> (Set(z) /\ Bot)).

Step 4 · Modus Ponens & Projection (EApp, ESnd)
snd(fst(compr(x. Bot, z)) hIn) : Bot completes the closed derivation tree. Run in repl.html →

ML-Generated Database & Frozen Archive
Generated Manual (HTML) • Generated DB (JSON) • Generated Table (TXT) • Frozen Legacy Archive