SPEC-005: Defeasible Reasoning

Adds the logical reasoning layer using concepts/Spindle Lisp embedded in Markdown. See Reason Commands for the CLI interface and Reasoning Engine for the architecture.

(given spec-005-documented)

Core insight

Zettelkasten notes make claims that can be formalized. SPL code blocks in Markdown express defeasible rules that zetl extracts, combines into a unified theory, and reasons over using spindle-core.

Key requirements

ID	Requirement
REQ-026	SPL extraction from Markdown
REQ-027	Theory construction with provenance
REQ-028	Vault reasoning (+D/-D/+d/-d conclusions)
REQ-029	Explanation with document provenance
REQ-030	Hypothetical reasoning (what-if)
REQ-031	Failure explanation (why-not)
REQ-032	Knowledge gap detection (require)
REQ-033	Conflict detection
REQ-034	SPL validation in check
REQ-035	Theory export
REQ-036	Cross-reference graph and theory

Eight commands

reason status — current conclusions
reason explain — proof tree with provenance
reason why-not — why something can’t be proved
reason require — abductive reasoning (missing facts)
reason what-if — hypothetical reasoning
reason conflicts — unresolved contradictions
reason export — theory export (JSON or SPL)
reason provenance — cross-referenced source tracing

Architecture decisions

ADR-005: Embed spindle-core as Rust library behind Feature Gates
ADR-006: Theory caching in .zetl/theory.json — see architecture/Cache
ADR-007: Provenance via spindle-core Meta API

Performance targets

Reasoning: <= 500ms for 10,000 rules
Memory: <= 50 MB for reasoning
Incremental extraction from cache

SPL-in-Markdown as literate programming

Embedding logic in prose follows the literate programming tradition (Knuth). The SPL blocks are grounded in their surrounding prose — see SPEC-006 Merkle Tree for content-addressed grounding.

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

Spec	Title	Status	Primary Feature
SPEC-001 Link Graph CLI	Bi-directional Link Graph CLI	Implemented	Wikilinks, graph queries, SimHash, cache
SPEC-002 Full-Text Search	Full-Text Content Search	Implemented	`zetl search`
SPEC-003 Agent Ergonomics	Agent Ergonomics & Robustness	Implemented	JSON errors, dedup, list/export
SPEC-004 Distributed Sync	Distributed Vault Sync	Proposed	Goblins sidecar, OCapN
SPEC-005 Defeasible Reasoning	Defeasible Logic over Markdown	Implemented	`zetl reason` (8 subcommands)
SPEC-006 Merkle Tree	Content-Addressed Merkle Tree	Implemented	BLAKE3 hashing, grounding, drift
SPEC-007 Graph Diff	Git-Backed Graph Diff	Implemented	`zetl diff`
SPEC-008 Watch Mode	Vault Watch with Event Stream	Implemented	`zetl watch`
SPEC-009 Xanadu View	Xanadu-Inspired Transclusion TUI	Implemented	`zetl view`

ID	Requirement
REQ-037	Merkle tree construction during index
REQ-038	SPL block dual hashing (content + AST)
REQ-039	Two-tier cache invalidation (mtime + content hash)
REQ-040	SPL-specific theory cache invalidation
REQ-041	Implicit section grounding
REQ-042	Explicit grounding via `(meta ... (source ...))`
REQ-043	Drift detection in `zetl check --drift`
REQ-044	Durable provenance with content hashes
REQ-045	Content block discovery (`zetl blocks`)