Markdown for LLMs

Check a property on a finite domain

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

# Check a property on a finite domain

## Intention

I want to check that every element of the presented domain gets the expected conclusion.

The check runs over a finite domain; act goals use the same property form.

## Incorrect form and why it stays silent

A premise does not replace an expectation about the conclusion.

```law title="Incorrect form"
property AllRegistered {
    forall p in collect x: Person where eligible(x);
    expect eligible(p);
}
```
This checks the selection condition and stays silent on whether registered was obtained. Another incorrect form is `forall p in GeneratedPeople;`: an arbitrary generator is not declared here and does not replace a finite collect; that is exactly the mutation pinned by teaches.

## Correct form

The property reads the registered head. The collect domain is finite; there is no random generator and no seed here.

```law
language "law.core" version "0.2";
package recipes.n.r12 version "0.1.0";
namespace "urn:recipe:n-package:12";

entity Person;
relation eligible(p: Person);
relation complete(p: Person);
relation registered(p: Person);
rule Register strict {
    for p: Person;
    when eligible(p) and complete(p);
    then registered(p);
}
```

## Frozen execution scene

| Facts | Question | Answer |
|---|---|---|
| eligible(p), complete(p) | AllRegistered | PASS, domain 1 |
| eligible(p), no complete(p) | MissingRegistered | FAIL, counterexample p |
| Same incomplete input | Incorrect VacuousRegistration with expect eligible(p) | PASS |

```law
test "full input sustains property" {
    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 eligible(entity_ref("urn:recipe:n-package:12:p"));
        assert complete(entity_ref("urn:recipe:n-package:12:p"));
    }
    evaluate truth(registered(entity_ref("urn:recipe:n-package:12:p")));
    expect truth_status == TRUE_ONLY;
}

property AllRegistered {
    forall p in collect x: Person where eligible(x);
    expect registered(p);
}
```

```law
test "missing output counts as counterexample" {
    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 eligible(entity_ref("urn:recipe:n-package:12:p"));
    }
    evaluate truth(registered(entity_ref("urn:recipe:n-package:12:p")));
    expect truth_status == NEITHER;
}

property MissingRegistered {
    forall p in collect x: Person where eligible(x);
    expect registered(p);
}
```

```law
test "broken property checks only premise" {
    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 eligible(entity_ref("urn:recipe:n-package:12:p"));
    }
    evaluate truth(registered(entity_ref("urn:recipe:n-package:12:p")));
    expect truth_status == NEITHER;
}

property VacuousRegistration {
    forall p in collect x: Person where eligible(x);
    expect eligible(p);
}
```

## Counterfactual

The second scene leaves an element in the domain without a registered conclusion: the correct property yields FAIL. `teaches` replaces the finite collect with an undefined generator and requires a lowering rejection, not a fictitious empty run.

## Boundary

An act goal additionally carries a basis on a source fragment; across legal orders it is goals, not rules, that are checked. A seed is needed only by a generator, which this finite domain does not use. A property cannot be declared proven on an empty domain.

## Pitfall

A property once wrongly reported success on a resident without an age, because negation did not see the unknown. The fix is a separate not_known branch; the second scene checks exactly the absence of a conclusion.