Proof Trees

zetl reason explain <literal> shows why a conclusion holds. The output is a proof tree: the rules that fired, the facts they rested on, and any defeaters that were considered. This page is about when and how to read one.

Requires --features reason at install. See Installation.

What a proof tree is

When zetl concludes that some literal holds (or doesn’t), it found — or failed to find — a chain of rules and facts that lead to that literal. A proof tree is that chain laid out as text:

The root is the literal you asked about.
Each node is a rule that fired, labelled with the rule’s name.
Each leaf is a fact (given) or a dead end (a body literal that couldn’t be proved).
Defeaters that were considered — and either won or were overridden — appear alongside the main chain.

Every node carries provenance: the source file, line number, and page name where that rule or fact was written. You can walk from any conclusion back to the exact prose that originated it.

The command

zetl reason explain "acme-ready-to-start"

By default the output is JSON. Three other formats are available via --as:

`--as`	What you get
`json`	Structured proof tree (default)
`table`	A tabular view of nodes, rules, and sources
`natural`	English prose: “The literal X is defeasibly provable because …”
`dot`	Graphviz DOT source — pipe to `dot -Tpng` for a diagram

There is also --depth N (default 10) which caps how deep the tree goes. Unbounded trees in large vaults can be overwhelming; 4 or 5 is usually enough for day-to-day use.

The natural-language form

--as natural is the one to use when you want a sentence you can paste into Slack:

zetl reason explain "acme-ready-to-start" --as natural

Output looks like:

The literal 'acme-ready-to-start' is defeasibly provable.
It follows from rule r-acme-ready (theories/project-readiness.spl:4)
whose body (acme-approved, acme-has-owner, acme-budget-signed-off)
is supported by facts given in projects/Acme Website.md lines 6–8.
No active defeater blocks this conclusion.

No formal notation, no symbols — just the chain of reasoning written out.

The diagram form

--as dot emits Graphviz source. Good for architectural reviews and posters:

zetl reason explain "release-candidate" --as dot \
  | dot -Tpng -o release-proof.png

The resulting diagram has one node per rule and fact, with arrows showing how conclusions flow. Defeaters appear as dotted edges.

When to read one

The usual trigger is surprise. You ran zetl reason status, you saw a conclusion that doesn’t match what you expected, and you need to know why. A few concrete cases:

“Why does zetl say the release candidate is ready?” You expected one more review. explain tells you which facts made the readiness rule fire — including, possibly, an outdated given still sitting in an old meeting note.
“Who signed off on docs-updated?” The rule fired, which means somewhere a given docs-updated was asserted. The proof tree names the file and line. Go look; it might be three months old.
“Why isn’t the build-blocked literal holding?” When you expected a negative conclusion but got silence. The tree shows which body literals failed to be proved, pointing you at the missing premise.

When the conclusion is negative and you want the failure analysis — what’s missing, what defeated what — reach for zetl reason why-not <literal> instead. It is the explicit counterpart to explain, and it lists candidate rules with their blockers:

zetl reason why-not "acme-ready-to-start"

For each rule that could have produced the conclusion, why-not shows which body literals were unprovable or which defeater fired.

Cross-referencing with provenance

reason explain is the deep-dive view of a single conclusion. [[Running Queries|reason provenance]] is the shallower, graph-oriented view — “what pages contributed?” rather than “what tree of rules fired?”. Use them together:

# Drill down into the logical chain
zetl reason explain "acme-ready-to-start" --as natural

# Zoom out to the pages involved
zetl reason provenance "acme-ready-to-start"

A worked pattern

A habit worth adopting: whenever zetl reason status tells you something you didn’t expect, pipe the literal straight into explain --as natural:

zetl reason status --literal "acme*" --positive
# Oh — acme-ready-to-start is +d, but legal hasn't cleared yet?
zetl reason explain "acme-ready-to-start" --as natural

Nine times out of ten, the explanation points at a stale given or a missing (prefer ...) — the kind of thing you fix in thirty seconds once you can see it.

Backlinks

Linked Pages

What is Defeasible Reasoning

A short primer on the kind of logic zetl uses when you ask it to reason over your notes. No symbols, no formal notation — just an explanation of why this flavour of logic suits knowledge work.

Requires --features reason at install. See Installation.

Classical logic: everything is final

In classical logic, facts combine and the conclusion is permanent. If you write down that every bird flies, and that Tweety is a bird, then Tweety flies. Forever. Adding new information can only produce new conclusions — it can never retract one you already made.

That rule works beautifully inside a maths textbook. It breaks almost immediately when you try to write down the actual state of a research project, a release plan, or a set of beliefs you formed over six months of reading. Real knowledge is provisional. You revise it. You hedge. You say “normally X, but not when Y”.

Defeasible logic: conclusions have strength

Defeasible reasoning lets you write rules that are normally true but can be defeated by stronger evidence. In a project-tracking vault you might write:

Normally, a release candidate is ready if core features are done, docs are written, and tests pass.
Except when there is an outstanding critical bug.

Both rules live in the theory at the same time. When zetl reasons over them, the defeater wins if its conditions hold — the release is blocked. If the bug is later fixed, the block lifts and the conclusion flips. You never rewrote the rules; you just added and removed facts.

This is exactly how thinking about ongoing work feels. “We’re on track — unless the client pushes back on the design.” “The proposal is done — except we still need a legal review.” You already reason this way. zetl just gives you a notation for it.

What-if and Abduction

Two commands — zetl reason what-if and zetl reason require — let you play with the theory without actually editing it. One asks “what changes if I add this fact?”. The other asks “what facts would I need to prove this goal?”. Both are indispensable when planning.

Requires --features reason at install. See Installation.

`reason what-if` — forward hypotheticals

what-if takes a snippet of SPL, temporarily adds it to the theory, recomputes conclusions, and reports the diff. Your vault files are not touched.

zetl reason what-if "(given acme-legal-cleared)"

Output: every conclusion that changed — literals that newly hold, literals that stopped holding, tags that flipped between +d and -d. The rest is filtered out.

Focus on a specific goal

--goal narrows the diff to a single literal you care about. Answers the question “if I add this, does this become provable?”:

zetl reason what-if "(given acme-legal-cleared)" --goal "acme-ready-to-start"

From a file

Writing SPL

Spindle Lisp (SPL) is the small language zetl reads when you ask it to reason over your vault. This page walks through the syntax by example — no formal grammar, just enough to start writing useful theories.

Requires --features reason at install. See Installation.

Where SPL goes

SPL lives in two places:

Fenced code blocks inside any Markdown file, tagged spl.
Standalone .spl files anywhere in the vault.

# Q2 Release

We're tracking the release of the next minor version here.

```spl
(given core-features-done)
(given docs-drafted)
```

zetl merges every spl block and every .spl file across the vault into one combined theory before reasoning. A fact stated on one page can feed a rule defined on another. This is the point — rules and facts can live next to the prose that motivated them.

Facts

A fact is something you assert to be true. Use (given ...):

(given project-approved)
(given has-owner)
(given budget-signed-off)

Running Queries

Once your vault contains some SPL, zetl reason is how you ask questions of it. This page walks the everyday command surface: status, conflicts, export, and provenance.

Requires --features reason at install. See Installation.

`reason status` — the default view

zetl reason status prints every conclusion the combined theory produces, tagged with +D, -D, +d, or -d (see What is Defeasible Reasoning for what those mean).

cd ~/notes
zetl reason status

In a TTY you get a table. Piped or redirected, you get JSON — same data, machine-readable.

Filters

Status output gets long fast. A few flags keep it manageable:

Flag	Shows
`--positive`	Only `+D` and `+d` conclusions
`--negative`	Only `-D` and `-d` conclusions
`--definite`	Only `+D` and `-D` (the strict layer)
`--defeasible`	Only `+d` and `-d` (the soft layer)
`--literal "release*"`	Wildcard filter on the literal name (`*` and `?` supported)

Combine them. “What are all the things my Acme project is currently defeasibly committed to?” becomes:

zetl reason status --positive --defeasible --literal "acme*"

Installation

zetl ships prebuilt binaries for Linux, macOS, and Windows. The installer script handles platform detection, download, and wiring up the man page and shell completions. If you prefer to build from source, that path is documented below too.

Prebuilt binaries (recommended)

macOS and Linux:

curl -fsSL https://files.anuna.io/zetl/latest/install.sh | bash

The script detects your OS and architecture, downloads the right tarball, installs the binary to ~/.local/bin, and generates the man page and shell completions.

Windows:

Download zetl-windows-x86_64.zip from files.anuna.io/zetl/latest, extract zetl.exe, and place it somewhere on your PATH.

Pinning to a specific version

VERSION=0.6.1 curl -fsSL https://files.anuna.io/zetl/latest/install.sh | bash

Custom install location

INSTALL_DIR=/usr/local/bin curl -fsSL https://files.anuna.io/zetl/latest/install.sh | bash

Proof Trees

What a proof tree is

The command

The natural-language form

The diagram form

When to read one

Cross-referencing with provenance

A worked pattern

Related

Backlinks