Check every element of a finite set

Intention

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

Correct formFrozen execution sceneBoundary

Incorrect form and why it stays silent

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

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

Arxo 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

checked members pass forall

Arxo 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;

}

unchecked late member blocks forall

Arxo 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;

}

empty domain holds vacuously

Arxo 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.