Markdown for LLMs

Check every element of a finite set

The source Markdown for this article. Copy it into your assistant or download it as a text file.

# Check every element of a finite set

## Intention

I want to check all reachable elements after their set has completed.

## Incorrect form and why it stays silent

A quantifier cannot be included in a cycle of its own domain:

```law title="Incorrect form"
rule Feedback strict { for p: Person; when all_checked(p); then reach(p, p); }
```

Unbounded `global_person_domain()` without a supplier also does not mean an empty set.

## Correct form

```law
language "law.core" version "0.2";
package recipes.v.r10 version "0.1.0";
namespace "urn:recipe:v-negation:10";

entity Person;
relation edge(a: Person, b: Person);
relation reach(a: Person, b: Person);
rule Base strict {
    for a: Person; for b: Person;
    when edge(a, b);
    then reach(a, b);
}
rule Step strict {
    for a: Person; for b: Person; for c: Person;
    when monotone(reach(a, b)) and edge(b, c);
    then reach(a, c);
}
relation root(p: Person);
relation checked(p: Person);
relation all_checked(p: Person);
rule AllChecked strict {
    for p: Person;
    when root(p) and forall x in (collect y: Person where monotone(reach(p, y))) satisfies checked(x);
    then all_checked(p);
}
```

## Frozen execution scene

| Facts | Question | Answer |
|---|---|---|
| a→b→c, checked(b), checked(c) | all_checked(a) | TRUE_ONLY |
| a→b→c, checked only b | all_checked(a) | NEITHER |
| root(a), no edges | all_checked(a) | TRUE_ONLY (empty domain) |
| reverse domain producer | check | E4102 |

```law
test "checked members pass forall" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert root(entity_ref("urn:recipe:v-negation:10:a"));
        assert edge(entity_ref("urn:recipe:v-negation:10:a"), entity_ref("urn:recipe:v-negation:10:b"));
        assert edge(entity_ref("urn:recipe:v-negation:10:b"), entity_ref("urn:recipe:v-negation:10:c"));
        assert checked(entity_ref("urn:recipe:v-negation:10:b"));
        assert checked(entity_ref("urn:recipe:v-negation:10:c"));
    }
    evaluate truth(all_checked(entity_ref("urn:recipe:v-negation:10:a")));
    expect truth_status == TRUE_ONLY;

}
```

```law
test "unchecked late member blocks forall" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert root(entity_ref("urn:recipe:v-negation:10:a"));
        assert edge(entity_ref("urn:recipe:v-negation:10:a"), entity_ref("urn:recipe:v-negation:10:b"));
        assert edge(entity_ref("urn:recipe:v-negation:10:b"), entity_ref("urn:recipe:v-negation:10:c"));
        assert checked(entity_ref("urn:recipe:v-negation:10:b"));
    }
    evaluate truth(all_checked(entity_ref("urn:recipe:v-negation:10:a")));
    expect truth_status == NEITHER;

}
```

```law
test "empty domain holds vacuously" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert root(entity_ref("urn:recipe:v-negation:10:a"));
    }
    evaluate truth(all_checked(entity_ref("urn:recipe:v-negation:10:a")));
    expect truth_status == TRUE_ONLY;

}
```

## Counterfactual

teaches adds a reach dependence on all_checked and requires E4102. The scene with a late c without checked catches early fixation of forall on a single b.

## Boundary

Truth on an empty collection does not prove completeness of a real registry. An unknown domain supplier is not equal to an empty collect: it yields NEITHER with MISSING_INPUT. The witness uses only finite relations; an arbitrary global enumeration is not attributed to it.

## Pitfall

The scene with a late element requires not accepting it unchecked: forall must wait for the domain to complete.