Establish the absence of a registry record

Intention

I want to treat the absence of a licence as a negative fact only inside a complete registry.

Incorrect form and why it stays silent

Without a snapshot the closure is rejected; a date instead of a completeness instant also does not work.

closure Registry { predicate licensed; domain registered; complete_as_of @2026-09-13; }

Correct form

language "law.core" version "0.2";
package recipes.v.r01 version "0.1.0";
namespace "urn:recipe:v-negation:01";

entity Person;
relation registered(p: Person);
relation licensed(p: Person);
relation pair_domain(p: Person, q: Person);
closure Registry {
    predicate licensed;
    domain registered;
    snapshot REGISTRY_2026;
    complete_as_of @2026-09-13T00:00:00+05:00;
    derive_explicit_negative true;
    effective [@2026-01-01, @2027-01-01);
}

Frozen execution scene

Facts	Question	Answer
registered(a), no record	licensed(a)	FALSE_ONLY
registered(a), licensed(a)	licensed(a)	TRUE_ONLY
outside the domain	licensed(a)	NEITHER
registered(a), legal_time 2027-01-01	licensed(a)	NEITHER
registered(a), without Registry	licensed(a)	NEITHER

absent record denies license

test "absent record denies license" {
    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 registered(entity_ref("urn:recipe:v-negation:01:a"));
    }
    evaluate truth(licensed(entity_ref("urn:recipe:v-negation:01:a")));
    expect truth_status == FALSE_ONLY;

}

present record grants license

test "present record grants license" {
    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 registered(entity_ref("urn:recipe:v-negation:01:a"));
        assert licensed(entity_ref("urn:recipe:v-negation:01:a"));
    }
    evaluate truth(licensed(entity_ref("urn:recipe:v-negation:01:a")));
    expect truth_status == TRUE_ONLY;

}

out-of-domain entity stays unknown

test "out-of-domain entity stays unknown" {
    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";
        }

    }
    evaluate truth(licensed(entity_ref("urn:recipe:v-negation:01:a")));
    expect truth_status == NEITHER;

}

closed effective window yields neither

test "closed effective window yields neither" {
    given {
        context {
            legal_time @2027-01-01;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        assert registered(entity_ref("urn:recipe:v-negation:01:a"));
    }
    evaluate truth(licensed(entity_ref("urn:recipe:v-negation:01:a")));
    expect truth_status == NEITHER;

}

Counterfactual

Mutations remove snapshot, replace Instant with a date, and substitute a binary relation for domain: E1307, E1307, E2114. Without the closure at all, evaluates gets NEITHER.

Boundary

Tuples are closed, not the whole world. The snapshot name in this witness is a policy identifier; the registry’s external bytes are not loaded. In a real case, completeness and provenance are supplied by the snapshot holder.

Pitfall

Absence of a debt without a producer of the negative yields NEITHER; closure fixes the answer. Closure allows any matching arity, not only the unary form.

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

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