Exercise 2. Four cases for one question

An exercise for the four states page. The package is the same as on the page, without a single new symbol: the rare-collections room norm and three relations.

Setup. Pick four cases so that the question “is Ivanova admitted to the rare-collections room” receives in turn all four answers: TRUE_ONLY, FALSE_ONLY, BOTH, NEITHER. The package must not be changed. Only facts may change.

Hint. The norm derives only a positive access. Where, then, would a denial and a contradiction come from, if there are no more rules?

Below is the solution. Try it yourself first.

Solution

The page’s package, same version:

Arxo Law

language "law.core" version "0.2";
package tutorial.archive version "0.2.0";
namespace "urn:law:tutorial:archive";

entity Person;

relation in_researcher_registry(p: Person) kind institutional;
relation accredited(p: Person) kind institutional;
relation may_enter_rare_room(p: Person) kind institutional;

rule RareRoomAccess strict {
    for p: Person;
    when in_researcher_registry(p) and accredited(p);
    then may_enter_rare_room(p);
}

Four cases:

Case	Facts	Answer on may_enter_rare_room(ivanova)
1	registry, accreditation	TRUE_ONLY — the norm fired
2	case record not may_enter_rare_room(ivanova)	FALSE_ONLY — the denial fed by the case
3	registry, accreditation, the same negative record	BOTH — the norm and the record argue
4	nothing	NEITHER

The key to cases 2 and 3: the case may state the norm’s head itself, not just premises, and in either polarity. Law does not ask “whether one may”: a negative access record is as much a case fact as a registry record. The norm is not cancelled thereby. In case 3 it fires, and its conclusion stands next to the case record, hence the answer is BOTH, not “the record won”.

Check

All four rows of the table execute on this package. A fifth case for self-check: the registry exists, accreditation holds two records, “yes” and “no”. Access here is NEITHER, already covered on the page: a BOTH-state premise does not count as established.

What the exercise teaches. Telling apart two sources of denial: a norm with a negative head, covered on the next page, and a case record. While the package lacks the first, FALSE_ONLY comes only from the second.