Spindle Lisp

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

Syntax reference

Facts

(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 ...) inside rule heads and bodies:

(normally r-penguins-dont-fly penguin (not flies))
(except d-wing broken-wing (not flies))

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 Scanner extracts these blocks with line numbers for Provenance. Multiple blocks per page are supported — see Reason Commands for how to query the combined theory.

Standalone files

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

See also: Defeasible Reasoning, Reasoning Engine, Provenance

Backlinks

Linked Pages

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.

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

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 Spindle Lisp with provenance comments

Example

Running zetl reason provenance "release-candidate" on this vault traces the conclusion through rules in theories/release-readiness.spl back to facts scattered across the architecture and feature pages.

See also: Reasoning Engine, Reason Commands, Defeasible Reasoning

Reasoning Engine

Reasoning Engine

The reasoning engine takes Spindle Lisp extracted by the Scanner from across the entire vault, merges it into a single theory, and computes conclusions using Defeasible Reasoning. Every conclusion carries full Provenance — you can trace any result back to the exact file and line that contributed to it.

Pipeline

Extract — Scanner finds SPL blocks in Markdown fences and .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
Combine — all rules and facts are merged into a single theory
Validate — check for undefined labels, duplicate definitions
Reason — spindle-core computes conclusions
Annotate — each conclusion is traced back to its proof sources

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

Conclusion types

The engine produces four types of conclusion — see Defeasible Reasoning for details:

Tag	Meaning
`+D`	Definitely provable
`-D`	Definitely not provable
`+d`	Defeasibly provable
`-d`	Defeasibly not provable

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.

See also: Reason Commands, Provenance, Spindle Lisp

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.

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. 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 name body head)`	If body, then head — no exceptions
Defeasible	`(normally name body head)`	If body, normally head — can be defeated
Defeater	`(except name 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.

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

In zetl

The Reasoning Engine implements defeasible reasoning via spindle-core. See Reason Commands for the CLI interface and Provenance for how conclusions trace back to source files.

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

`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?”

Scanner

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

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.

SPL extraction

Fenced code blocks tagged ```spl are extracted verbatim, along with their source file and line number. Standalone .spl files anywhere in the vault are also picked up. Both feed into the Reasoning Engine with full Provenance.

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

Implementation

Built on pulldown-cmark for Markdown parsing and ignore for .gitignore-aware file walking. The scanner is deliberately read-only — see Local-first Design.

See also: Cache, Link Graph, Reasoning Engine