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

If you want to try a larger experiment — a whole new rule, several facts — put it in a file and pass it with --file:

cat > /tmp/experiment.spl <<'SPL'
(given acme-legal-cleared)
(given acme-tests-green)
(prefer r-acme-ready d-acme-legal)
SPL

zetl reason what-if --file /tmp/experiment.spl --goal "acme-ready-to-start"

Useful when you are exploring “what if we relaxed this constraint?” without committing to the change.

Use cases

Planning. “If the client approves the proposal on Monday, are we clear to start?” — add (given client-approved) and look at the diff.
Gating a decision. “The build is red. Would merging this feature make any currently-+d conclusion flip to -d?” — add the facts your feature introduces and check.
Defensive checks. Before committing a new SPL rule, run what-if with it pasted in. If the conclusions diff is bigger than you expected, your rule is too broad.

`reason require` — backward abduction

require is the inverse question: you have a goal in mind, and you want to know what facts you’d need to add to make it provable. This is abductive reasoning — inference from goal to premises.

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

zetl returns the minimal sets of missing facts that would complete the derivation. Each set is a separate solution — there may be several ways to prove the goal, via different rules.

Example output

Literal: acme-ready-to-start
Status: requirements_found

Solution 1 (via r-acme-ready):
  - acme-approved          (not derivable; must be asserted)
  - acme-has-owner         (not derivable; must be asserted)

Solution 2 (via r-acme-ready-alt):
  - acme-exec-override     (not derivable; must be asserted)

Read this as a to-do list. Each required fact is something you (or the project) must actually produce; it can’t be derived from the rules currently in the vault.

Chaining assumptions with `--assume`

The --assume flag lets you say “treat these as already given” and ask what else is still needed:

zetl reason require "acme-ready-to-start" \
  --assume "(given acme-approved)" \
  --assume "(given acme-has-owner)"

This is the practical planning form: you know some things are already true, you want to know what remains. Chain multiple --assume flags for cumulative hypotheticals.

Capping results

--max-solutions N (default 5) caps how many distinct requirement sets are returned. For tightly constrained goals you usually get one; for goals reachable through many alternative rules you may want a higher cap to see all the options.

Use cases side by side

Question	Command
“What’s blocking the release?”	`reason require "release-candidate"`
“If the client approves, are we good?”	`reason what-if "(given client-approved)" --goal "ready"`
“Would adding this rule change any current conclusion?”	`reason what-if --file new-rule.spl`
“What single fact is closest to getting us unblocked?”	`reason require "ready-to-ship"`

require is the command to run at the start of a planning session — it turns a vague goal into a concrete list of facts to produce. what-if is the command to run in the middle, as you weigh one decision at a time.

Time travel

Both accept --at when --features history is installed. require --at "last monday" tells you what the required facts were at a past point, which is useful for decision retrospectives: “what did we think it would take to ship, before we knew about the legal issue?”. See Time Travel.

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.

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)

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.

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*"

Time Travel

Requires --features history at install. See Installation.

--at is a global flag that re-runs any read-only zetl command against a past state of your vault. Last Tuesday’s backlinks, the orphan list from before the big refactor, the link count on the day you published — all one flag away.

Why time-travel your notes

You remember writing about Glass-Steagall in the essay you posted in June, but the page doesn’t mention it any more. Did you delete the link, or did you never write it? Without history, you’d dig through git log (if you even use git on your notes) and eyeball old files. With --at:

zetl --at "2024-06-01" links "Banking Reform"

The graph as it stood that day. Same output format, same flags, same wikilink resolver — just a different snapshot under the hood.

Other uses:

Audit a stable conclusion. zetl --at "last monday" check to confirm the vault was clean when you claimed it was.
Recover a deleted page. zetl --at HEAD~5 view "Lost Thought" shows the full rendered page from five snapshots ago.
Compare statistics across time. zetl --at "3 months ago" stats against zetl stats — a graph-size delta without leaving the shell.
Retrace a thought. When did I first link Zettelkasten Method to Spaced Repetition? zetl --at "90 days ago" backlinks "Spaced Repetition".

What `--at` accepts

Expression	Example	Notes
ISO 8601 date	`--at "2024-01-15"`	Resolves to the latest snapshot on or before that date.
Natural-language relative	`--at "3 days ago"`	Also `"last monday"`, `"yesterday"`, `"2 weeks ago"`.
VCS ref	`--at HEAD~1`	One snapshot before the current tip.
Change-ID prefix	`--at abc12`	jj change-ID, any unique prefix.

Quote expressions that contain spaces — your shell will thank you.

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

What-if and Abduction

reason what-if — forward hypotheticals

Focus on a specific goal

From a file

Use cases

reason require — backward abduction

Example output

Chaining assumptions with --assume

Capping results

Use cases side by side

Time travel

Related

Backlinks

`reason what-if` — forward hypotheticals

`reason require` — backward abduction

Chaining assumptions with `--assume`