1  Interactive Diagnostics with parse-strat

1.1 The Diagnostic Sandbox

The parse-strat module provides a tactile, responsive Read-Eval-Print Loop (REPL) environment acting as a full Interactive Theorem Prover (ITP). Before dispatching hardcoded models to the formal Sequent verifier (seq-embed), researchers utilize this sandbox to manually explore the boundaries of weak stratification constraints in Quine’s New Foundations. It features a monolithic tactic ecosystem (including intro, simp, rewrite, focus_hyp, elevate, collapse_loop) driving a seamless AST-to-DAG compilation pipeline.

The REPL is supported by a powerful topological graph-flattening backend, giving immediate feedback on Extensionality bounds.

1.2 Tactical Workflow & Geometric Feedback

To effectively use this dual-engine architecture, users must understand how tactical symbolic reasoning maps down into raw spatial constraints. The internal constraint engine translates formulas into a geometric Directed Acyclic Graph (DAG) using specific weight mappings:

  • Equality (x = y) / Quine Pairs (Q(a,b)): Generates a 0 weight constraint.
  • Membership (x e y) / Application (z = u(v)) / Lambda / Set Comprehension ({x | P(x)}): Generates a +1 weight constraint.
  • Strict Typestate Offset (x < y): Generates a -1 weight constraint.

(Note: For a deep-dive on exactly how these constraints are extracted from the AST and verified mathematically via Bellman-Ford, see Chapter 4: The nf-validate Constraint Graph).

1.2.1 1. Interactive Proof Example: Strong Cantorian Preservation

To prove that the Quine pair preserves Strongly Cantorian (SC) sets, we first define our theorem and then use natural deduction to break it down.

> Starting proof of SC_Preservation
ITP> 
a : a = a
----------------------
forall b. ((a = Ta /\ b = Tb) -> Qab = TQab)

ITP> 
b : b = b
a : a = a
----------------------
((a = Ta /\ b = Tb) -> Qab = TQab)

ITP> 
H_SC : (a = Ta /\ b = Tb)
b : b = b
a : a = a
----------------------
Qab = TQab

ITP> 
H1 : a = Ta
H2 : b = Tb
b : b = b
a : a = a
----------------------
Qab = TQab

We then feed the equations into the eval command, which bypasses the tactical proof state to extract topological constraints directly from the strings and run Bellman-Ford cycle detection.

ITP> Stratification successful. Witness: {a@0 : 0, b@0 : 0, Ta@0 : 0, Tb@0 : 0, QTaTb@0 : 0, Qab@0 : 0, TQab@0 : 0}

Because no negative-weight cycles were generated, the system confirms mathematical consistency, proving that Quine pairs successfully preserve SC status without collapsing.

1.2.2 2. Exploring Extensionality with Diagnostic Cut

We can manually verify how Extensionality Collisions break typestate bounds using the cut tactic.

> Starting proof of Trivial_Identity
ITP> 
A : A = A
----------------------
A = A

ITP> Extensionality Collision!
Contradiction Path: x@0 ∈ x@0 (-1)
  Requires l(x@0) = l(x@0) + -1
ITP> Proof aborted.

By intentionally introducing a saturated boundary (x e x), we can use the engine to observe exactly where the unstratifiable loop causes the engine to flag a negative-weight cycle and abort the proof.

1.2.3 3. Subset Transitivity (Tactical Completion)

We can also execute complete formal derivations directly within the REPL, such as the proof of Subset Transitivity.

> Starting proof of Subset_Trans
ITP> 
A : A = A
----------------------
forall B. forall C. forall z. (((z e A -> z e B) /\ (z e B -> z e C)) -> (z e A -> z e C))

ITP> 
H : ((z e A -> z e B) /\ (z e B -> z e C))
z : z = z
C : C = C
B : B = B
A : A = A
----------------------
(z e A -> z e C)

ITP> 
H1 : (z e A -> z e B)
H2 : (z e B -> z e C)
z : z = z
C : C = C
B : B = B
A : A = A
----------------------
(z e A -> z e C)

ITP> 
Hz : z e A
H1 : (z e A -> z e B)
H2 : (z e B -> z e C)
z : z = z
C : C = C
B : B = B
A : A = A
----------------------
z e C

ITP> No more goals. Proof complete!
ITP> Proof accepted.

1.2.4 4. Kuratowski Bounding Tests

The REPL natively parses and checks topological bounds instantly using the step command, useful for analyzing multi-level type deviations like the Kuratowski pair (\(P = \{\{a\}, \{a, b\}\}\)).

> --- Extracting Constraints ---
{ v1 := (Var.free "x", 0), v2 := (Var.free "K", 0), diff := 1, directed := false }
{ v1 := (Var.free "x", 0), v2 := (Var.free "a", 0), diff := 0, directed := false }
{ v1 := (Var.free "y", 0), v2 := (Var.free "K", 0), diff := 1, directed := false }
{ v1 := (Var.free "y", 0), v2 := (Var.free "a", 0), diff := 0, directed := false }
{ v1 := (Var.free "y", 0), v2 := (Var.free "b", 0), diff := 0, directed := false }
--- Graph Edges ---
{ src := (Var.free "x", 0), dst := (Var.free "K", 0), weight := 1 }
{ src := (Var.free "K", 0), dst := (Var.free "x", 0), weight := -1 }
{ src := (Var.free "x", 0), dst := (Var.free "a", 0), weight := 0 }
...
--- Running Bellman-Ford ---
Stratification successful.

The constraint extraction clearly visualizes how K acts as the set boundary, routing connections symmetrically across x and y while mathematically tracking exactly how K sits above a and b.

1.3 Core Command Reference

1.3.1 Logical Operators Syntax

  • -> or →: Implication
  • <->: IFF (If and only if)
  • forall or ∀: Universal Quantifier
  • exists or ∃: Existential Quantifier
  • /\: Conjunction (AND)
  • \/: Disjunction (OR)
  • ~: Negation (NOT)
  • e: Set Membership (e.g., x e y) (Note: Monist uses in, but Lean 4 reserves in, so e is used here)
  • <: Typestate Inequality (e.g., x < y)
  • {x | P(x)}: Set Comprehension

1.3.2 Axioms & Session Management

  • assume <name> <formula>: Register a named axiom globally.
  • theorem <name> <formula>: Start a new proof with a target goal.
  • save_session <file> / load_session <file>: Persist proof state JSONs.
  • deff <name> <args...> := <formula>: Pre-compile an AST Macro.

1.3.3 Interactive Tactics

  • intro [name]: Introduce a premise.
  • exact <name>: Close the current goal if it exactly matches the hypothesis.
  • apply <name>: Apply an implication hypothesis.
  • split: Split a conjunction goal into two separate goals.
  • left / right: Select a side of a disjunction goal.
  • destruct <name>: Break down conjunctions or disjunctions in context.
  • defer: Rotate the current goal to the back of the queue.
  • focus_hyp <name>: Bring a hypothesis to the front of the context.
  • cut <formula>: Introduce new hypothesis branches.
  • rewrite <name>: Substitute variables inside the goal.
  • schonfinkel: Compile quantified formulas directly into raw SKI combinator topology.
  • simp: Macro-expansion engine that unfolds definitions until reaching normal form (DNF).
  • have <name> <formula>: Assert intermediate topological lemmas and chain them into the context.
  • refl: DAG Isomorphism check utilizing Kosaraju’s SCC flattening.
  • stratify: Oracle Call: Closes existential/stratification goals automatically if no negative-weight cycles exist.
  • elevate: Applies the T-Functor (\(x \mapsto \iota"x\)) to manually neutralize stratification collisions.
  • collapse_loop: Reduces stable 0-weight self-referential cycles into a singular graph node using SCC mapping.

1.3.4 Diagnostics

  • eval <formula>: Parse topological shift and halt if structural loops emerge.
  • step <formula>: Process a logical formula step-by-step, providing immediate feedback on geometric bounds.

1.3.5 Differential SMT-LIB Ingestion

  • lake exe parse-strat --ingest-smt < out.smt: Directly ingest an exported standard SMT-LIB witness generated by the Rust monist-core engine. The Lean interpreter will parse the boundaries and topological node variables, independently run its native Bellman-Ford matrix evaluator, and perform a 1-to-1 Equivalence Check against the expected success_depths or extensionality-collision-trace defined in the SMT headers.