LDC-E4112 — A defeater with no defeasible target

For LLMs5 sections

What it means

A defeater never produces its head: it only takes down a defeasible candidate with the same head and polarity. With no such producer in the package, the defeater is operationally dead — it attacks a claim nobody makes. The compiler refuses it at the attacked proposition.

Add the defeasible rule the defeater is meant to attack, or drop the defeater. A strict conclusion is no candidate and does not count.

Example

language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";

entity A;
relation p(a: A) kind institutional;
relation q(a: A) kind institutional;
rule lonely defeater { for a: A; when p(a); defeat q(a); then q(a); }

Fix

language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";

entity A;
relation p(a: A) kind institutional;
relation q(a: A) kind institutional;
rule maker defeasible { for a: A; when p(a); then q(a); }
rule lonely defeater { for a: A; when p(a); defeat q(a); then q(a); }

Engine message

The engine reports this in its own wording:

example.law:8:52: error LDC-E4112: DEFEATER_WITHOUT_CANDIDATE: defeater "lonely" attacks a positive head "q", but it has no defeasible producer (§107.3; DECISION-0111 §2.1)

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.