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 using classical Natural Deduction tactics.

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 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.2 Interactive Tactics

  • intro [name]: Introduce a premise.
  • exact <name>: Close the current goal if it exactly matches the hypothesis.
  • destruct <name>: Break down conjunctions or disjunctions in context.
  • rewrite <name>: Substitute variables inside the goal.
  • cut <formula>: Introduce new hypothesis branches.

1.3.3 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.4 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.