Spindle Lisp

Spindle Lisp (SPL) is a domain-specific language for expressing concepts/Defeasible Reasoning theories. zetl extracts SPL from fenced code blocks in Markdown and from standalone .spl files.

(given spl-documented)

Syntax reference

Facts

Unconditionally true propositions:

(given bird)
(given (not guilty))

Strict rules

Cannot be defeated. If the body holds, the head must hold:

(always r-penguin-is-bird penguin bird)

Defeasible rules

Can be defeated by stronger evidence. The label is optional:

(normally r-birds-fly bird flies)
(normally bird animal)

Defeaters

Block a conclusion without asserting the opposite:

(except d-broken-wing broken-wing (not flies))

Superiority

Resolves conflicts between competing rules:

(prefer r-stronger-rule r-weaker-rule)

Conjunction

Combine multiple conditions in a rule body:

(normally r-ready
  (and tested documented reviewed)
  ready-to-ship)

Negation

Use (not ...) in rule heads and bodies:

(normally r-penguins-dont-fly penguin (not flies))

Metadata

Attach metadata to facts for explicit grounding (see Drift Detection):

(given redis-fast-enough)
(meta redis-fast-enough (source "^benchmark-results"))

Comments

; This is a comment

Embedding in Markdown

Wrap SPL in a fenced code block tagged spl:

```spl
(given bird)
(normally r-birds-fly bird flies)
```

The architecture/Scanner extracts these blocks with line numbers for concepts/Provenance. Multiple blocks per page are supported.

Standalone files

Any .spl file in the vault is also picked up. This is useful for cross-cutting rules that don’t belong to a single page — see the theories/ directory in this vault for examples.

Conclusion types

Tag	Meaning
`+D`	Definitely provable (strict rules, no defeaters possible)
`-D`	Definitely not provable
`+d`	Defeasibly provable (inferred, no active defeaters)
`-d`	Defeasibly not provable (blocked or no derivation path)

See also: concepts/Defeasible Reasoning, Reasoning Engine, concepts/Provenance, Reason Commands

Backlinks

Linked Pages

Reason Commands

Reason Commands

zetl reason exposes the Reasoning Engine through eight subcommands. All require --features reason at build time — see Feature Gates.

(given reason-status-done)
(given reason-explain-done)
(given reason-why-not-done)
(given reason-require-done)
(given reason-what-if-done)
(given reason-conflicts-done)
(given reason-export-done)
(given reason-provenance-done)

Commands

`reason status`

What does the vault’s combined concepts/Spindle Lisp theory conclude? Filter by polarity (--positive, --negative), strength (--definite, --defeasible), or literal name (--literal "release*").

`reason explain <literal>`

Why does a conclusion hold? Produces a proof tree tracing the derivation through rules back to facts, with full concepts/Provenance (file, line, page). Output as JSON, table, natural language, or Graphviz dot.

`reason why-not <literal>`

Why can’t something be proved? Identifies missing facts, blocked rules, or active defeaters. This is the inverse of explain — useful for understanding gaps in the vault’s knowledge.

`reason require <literal>`

What facts would make a goal provable? Abductive reasoning — finds the minimal sets of missing facts. Useful for answering “what would it take to make release-candidate true?”

Provenance

Provenance is the ability to trace a conclusion back to its origins. In zetl, every fact, rule, and conclusion carries metadata recording the source file, line number, and page name where it was defined.

(given provenance-documented)

Why it matters

A reasoning system that says “X is true” is only useful if you can ask “why?” and get a concrete answer. Provenance connects the Reasoning Engine’s abstract logic back to the human-readable documents in your vault.

What is tracked

Element	Provenance
Fact	File path, line number, page name
Rule	File path, line number, page name, rule label
Conclusion	Full proof tree of contributing rules and facts
Grounding	Section hash or explicit source reference (see Drift Detection)

Commands

zetl reason explain <literal> — proof tree with source locations
zetl reason provenance <literal> — cross-referenced with the Link Graph
zetl reason export --format spl — reconstructed concepts/Spindle Lisp with provenance comments

Grounding freshness

Since SPEC-006 Merkle Tree, provenance includes grounding freshness. Each source in a provenance trace reports whether its grounding (section or explicit) is still fresh — i.e., whether the prose that justifies the fact has changed since the theory was built.

Example

Running zetl reason provenance "vault-ready-to-publish" on this vault traces the conclusion through rules in theories/vault-readiness.spl back to facts scattered across the architecture, reference, and concept pages.

Reasoning Engine

Reasoning Engine

The reasoning engine takes concepts/Spindle Lisp extracted by the Scanner from across the entire vault, merges it into a single theory, and computes conclusions using concepts/Defeasible Reasoning. Every conclusion carries full concepts/Provenance.

(given spindle-core-integrated)
(given four-conclusion-types)

Pipeline

Extract — the Scanner finds SPL blocks in Markdown fences and standalone .spl files
Parse — spindle-parser converts SPL text into rule objects
Provenance — source file, line number, and page name are attached to each rule and fact
Merge — all rules and facts are merged into a single vault-wide theory
Validate — check for undefined labels, duplicate definitions, broken source references
Reason — spindle-core computes conclusions using the defeasible reasoning algorithm
Annotate — each conclusion is traced back to its proof sources with grounding freshness

Conclusion types

Tag	Meaning
`+D`	Definitely provable — strict derivation, no defeating possible
`-D`	Definitely not provable
`+d`	Defeasibly provable — inferred, no active defeaters
`-d`	Defeasibly not provable — blocked or no derivation path

Theory caching

The merged theory and its conclusions are cached in .zetl/theory.json. Invalidation uses the SPL AST hash — prose-only edits don’t trigger a rebuild. See architecture/Cache and Merkle Tree.

Feature gate

The reasoning engine is compiled only when --features reason is enabled — see Feature Gates. Without it, zetl reason prints a clear error rather than failing silently.

Cross-referencing

The --with-conclusions flag on Links Command bridges the structural graph with the logical theory, showing what each linked page contributes to the vault’s conclusions.

Defeasible Reasoning

Defeasible Reasoning

Defeasible reasoning is a form of logic where conclusions can be drawn tentatively and later retracted when stronger evidence appears. This is how most real-world reasoning works — we act on the best information available, knowing new facts might change our minds.

(given defeasible-reasoning-documented)

Why it fits knowledge management

Decision documents, architecture records, and project plans all contain reasoning that is provisional. A conclusion like “use Redis” might be well-supported now but defeated by a future license audit. concepts/Spindle Lisp lets you express this directly in your notes, and zetl’s Reasoning Engine computes what follows.

Rule types

Type	Syntax	Meaning
Fact	`(given X)`	X is unconditionally true
Strict	`(always label body head)`	If body, then head — no exceptions
Defeasible	`(normally label body head)`	If body, normally head — can be defeated
Defeater	`(except label body head)`	If body, block head — but don’t assert the opposite

Superiority

When two rules conflict, a superiority relation resolves the tie:

(prefer stronger-rule weaker-rule)

Without a declared preference, the conflict remains unresolved — zetl reason conflicts will flag it. See Reason Commands.

Conclusion tags

Tag	Meaning
`+D`	Definitely provable — strict derivation, no defeating possible
`-D`	Definitely not provable
`+d`	Defeasibly provable — inferred, no active defeaters
`-d`	Defeasibly not provable — blocked or no derivation path

In zetl

Scanner

The scanner is zetl’s entry point for understanding a vault. It walks every Markdown file and standalone .spl file, extracting concepts/Wikilinks and concepts/Spindle Lisp blocks in a single pass.

(given wikilink-extraction)
(given spl-extraction)

Wikilink extraction

The scanner recognises all common wikilink forms:

[[Page]] — basic link
[[Page|alias]] — aliased link
[[Page#heading]] — heading anchor
[[Page^block-id]] — block reference
![[Page]] — embed

Extracted links feed into the Link Graph for query and traversal.

Exclusion zones

The scanner skips wikilink-like patterns that appear inside:

Fenced code blocks (```)
Inline code (`)
HTML comments ()
YAML frontmatter (--- fences)

This prevents false positives from code examples or metadata.

SPL extraction

Drift Detection

Drift Detection

Drift occurs when the prose surrounding an SPL block changes but the SPL itself does not. The facts and rules may no longer accurately reflect the arguments in the surrounding text.

The problem

SPL blocks in Markdown are grounded in their surrounding prose. When you write:

## Benchmark Results
Redis achieves 185,000 reads/sec at p99.

```spl
(given redis-fast-enough)


The fact `redis-fast-enough` is grounded in the benchmark paragraph. If someone later edits the benchmark numbers but forgets to update the SPL, the fact drifts from its grounding.

## How zetl detects it

zetl uses the [[Merkle Tree]] to track grounding freshness:

1. During indexing, each SPL block's containing section is identified (heading through next heading)
2. A section grounding hash is computed from the non-SPL leaves in that section
3. When the theory is built, section grounding hashes are stored in the theory cache
4. On subsequent `zetl check --drift`, current grounding hashes are compared against cached values
5. Mismatches are reported as drift warnings

## Implicit vs explicit grounding

### Implicit (section-based)

The default. Every SPL block is grounded in its containing section's prose. No annotation needed.

### Explicit (source metadata)

Facts can be explicitly grounded to specific content:

```spl
(given redis-fast-enough)
(meta redis-fast-enough (source "^benchmark-results"))

Explicit grounding uses ^block-id, Merkle hash prefixes, or cross-file [[Page^block-id]] references. See Blocks Command for hash discovery.

Using drift detection

zetl check --drift                       # report drift warnings
zetl check --drift --fail-on warning     # CI: fail on drift

Drift requires a baseline from a previous theory build. New files have no baseline and are not flagged.

Design decisions

SPL changes are NOT drift (the SPL was updated intentionally)
Section restructuring (inserting a new heading) correctly triggers drift because the section boundaries change
Drift is reported as a warning, not an error, by default