Docs: defeater examples use the wrong head polarity and obsolete syntax #17

New issue

Open

opened 2026-07-16 04:27:48 +00:00 by anuna-02 · 1 comment

anuna-02 commented

2026-07-16 04:27:48 +00:00

(Migrated from codeberg.org)

Summary

Elephant's documentation teaches defeaters with the wrong head polarity, and several examples still use the rejected legacy ~> spelling. Following those examples produces an inert or oppositely-directed attacker rather than a rule that blocks the named conclusion.

This caused six signed defeaters in the FLF two-agent run to be retracted and reasserted with corrected heads, unnecessarily polluting the shared audit log.

Current examples

Several documents say that this blocks release-v230-ready:

(except r-incident-active active-incident release-v230-ready)

or use:

(~> r-incident-active active-incident release-v230-ready)

Affected locations include:

docs/dialect-spec.md ("Assert a defeater")
docs/spl-patterns.md ("Defeater as cancellation" and combined example)
docs/demo-walkthrough.md
docs/cli.md (task block)
the terse descriptions in docs/identity-and-corpus.md and the tech deck, which do not explain polarity

Actual engine semantics

To block positive q, the defeater must be an applicable rule for its complement:

(except d condition (not q))

The defeater uses (not q) as its attacking head but does not derive (not q) as a conclusion. This is also how the engine's own regression fixtures and reasoner tests are written.

For the recorded run, these were the required forms:

(except sx-proposal-site-no-engineering
  (and defuse-proposal furin-cleavage-site)
  (not engineered-signature))

(except sx-research-proximity-no-incident
  (and wiv-proximity wiv-coronavirus-research)
  (not lab-origin))

Expected / acceptance criteria

Replace every ~> example with canonical except.
Change examples intended to block q so their head is (not q).
State explicitly: the head names the attacking side; a defeater can attack but never establish its head.
Add an executable documentation fixture proving that the example changes q from +d to not provable while (not q) remains not provable.
Correct the corresponding stale examples in Spindle's SPL/reference documentation, which Elephant currently links as authoritative.

Environment

Observed with Elephant 0.1.2 during the FLF shared-theory run; current reasoner tests retain complement-head semantics.

### Summary Elephant's documentation teaches defeaters with the wrong head polarity, and several examples still use the rejected legacy `~>` spelling. Following those examples produces an inert or oppositely-directed attacker rather than a rule that blocks the named conclusion. This caused six signed defeaters in the FLF two-agent run to be retracted and reasserted with corrected heads, unnecessarily polluting the shared audit log. ### Current examples Several documents say that this blocks `release-v230-ready`: ```lisp (except r-incident-active active-incident release-v230-ready) ``` or use: ```lisp (~> r-incident-active active-incident release-v230-ready) ``` Affected locations include: - `docs/dialect-spec.md` ("Assert a defeater") - `docs/spl-patterns.md` ("Defeater as cancellation" and combined example) - `docs/demo-walkthrough.md` - `docs/cli.md` (`task block`) - the terse descriptions in `docs/identity-and-corpus.md` and the tech deck, which do not explain polarity ### Actual engine semantics To block positive `q`, the defeater must be an applicable rule for its complement: ```lisp (except d condition (not q)) ``` The defeater uses `(not q)` as its attacking head but does not derive `(not q)` as a conclusion. This is also how the engine's own regression fixtures and reasoner tests are written. For the recorded run, these were the required forms: ```lisp (except sx-proposal-site-no-engineering (and defuse-proposal furin-cleavage-site) (not engineered-signature)) (except sx-research-proximity-no-incident (and wiv-proximity wiv-coronavirus-research) (not lab-origin)) ``` ### Expected / acceptance criteria - Replace every `~>` example with canonical `except`. - Change examples intended to block `q` so their head is `(not q)`. - State explicitly: the head names the attacking side; a defeater can attack but never establish its head. - Add an executable documentation fixture proving that the example changes `q` from `+d` to not provable while `(not q)` remains not provable. - Correct the corresponding stale examples in Spindle's SPL/reference documentation, which Elephant currently links as authoritative. ### Environment Observed with Elephant 0.1.2 during the FLF shared-theory run; current reasoner tests retain complement-head semantics.

hugooconnor commented

2026-07-16 09:44:45 +00:00

(Migrated from codeberg.org)

Resolved on main by 834d4e7. Elephant's own docs now state defeater polarity explicitly — docs/concepts/Defeasible Logic.md has a "Defeater polarity" section ((except d p (not q)) blocks positive q, moving it +d→-D, while a positive head is an inert-for-blocking mistake), plus an executable fixture in tests/queries_cli.rs; docs/concepts/SPL.md links it and both note the legacy ~> spelling is rejected. No remaining ~> or wrong-polarity examples in this repo. The only outstanding item is the stale examples in the linked Spindle reference doc (spindle-rust/docs/src/reference/spl.md) — a separate repository, out of scope here.

Resolved on `main` by 834d4e7. Elephant's own docs now state defeater polarity explicitly — `docs/concepts/Defeasible Logic.md` has a "Defeater polarity" section (`(except d p (not q))` blocks positive `q`, moving it `+d`→`-D`, while a positive head is an inert-for-blocking mistake), plus an executable fixture in `tests/queries_cli.rs`; `docs/concepts/SPL.md` links it and both note the legacy `~>` spelling is rejected. No remaining `~>` or wrong-polarity examples in this repo. The only outstanding item is the stale examples in the linked Spindle reference doc (`spindle-rust/docs/src/reference/spl.md`) — a separate repository, out of scope here.

No labels

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference

anuna-research/elephant#17

No description provided.

Rows
Columns