The Answer That Needs a Human

In the last chapter we changed the rules and watched which grounds kept their force. Now leave the rules in place. Imagine that everything needed to consider a request is known, but the decision itself must still come from a human. No further calculation can replace that decision.

Arxo has a special declaration for this situation. It lets us name the question that calls for an outside decision and say who must make it. Before reading that entry, let us separate two questions that blend easily into one in ordinary speech: whether the way is open, and whether entry is permitted.

The gates are open

In Franz Kafka’s parable “Before the Law” a man comes to the doorkeeper and asks to be let in. The gates stand open. The doorkeeper says he cannot let him in now, but allows for the possibility later. The man stays to wait.

Take the model of this scene from the corpus. One distinction interests us: the state of the gates is known from the text, while permission to enter in the chosen formalization depends on a separate decision of the doorkeeper. That is one way of questioning the parable; it does not exhaust its meaning and invites discussion[^chapter-9-source].

The package’s relation names are German. weg_frei means that the way through the gates is free, and einlass_gestattet that entry is permitted. In both cases the argument is the man. A constant Mann is already declared for the petitioner:

const Mann: Person = entity_ref("urn:de:kafka:clir:vor-dem-gesetz#Mann") {
    label de official "der Mann vom Lande";
    label ru official "проситель из деревни";
}

After const come the name and the type, after the equals sign the reference to the particular object. So in the examples we can write Mann instead of the long entity_ref(...): the same petitioner is meant. DerTuerhueter likewise denotes the doorkeeper, and Tor the gates.

Some starting information already lives in the package. In particular, the request for entry is recorded thus:

@source(VDG_ANKUNFT)
assert eintritt_erbeten(Mann) { evidence VDG_1915_TEXT; }

The familiar assert states a fact. The @source mark binds it to a source fragment, and evidence VDG_1915_TEXT points at the evidence the entry carries. Here that is the parable’s text. We will examine the use of evidence in detail in the eleventh chapter. For now note that these entries are already available when the scenario runs: the request need not be repeated in every given block.

The premise a human must report

The assertion “the doorkeeper has permitted this petitioner to enter” is recorded by the relation tuerhueter_gewaehrt_einlass. Let us read its declaration:

@source(TO_JETZT_NICHT, TO_SPAETER_MOEGLICH)
external judgment relation tuerhueter_gewaehrt_einlass(m: Person) {
    authority Tuerhueter;
    label de official "der Türhüter gewährt diesem Mann den Einlaß";
    label ru official "привратник даёт этому просителю впуск";
}

The relation form is familiar to us: the name, the argument m of type Person, then the declaration body. The new words stand before the declaration: external judgment. They mark out the relation set aside for an outside judgment. Here that is the entry decision the model must receive from outside.

The line authority Tuerhueter names the one to whom the question is addressed: the doorkeeper[^chapter-9-judgment]. Here Tuerhueter is the name of the authorized person in the judgment’s declaration. The constant DerTuerhueter we met above denotes the character in the parable’s facts. These names play different roles in the model: Tuerhueter names the authority in the judgment declaration; DerTuerhueter can be an argument in an assertion about the character.

The declaration by itself does not yet establish permission. For that the package holds a rule:

@source(TO_JETZT_NICHT)
rule EinlassGestattet strict {
    label de official "Ob der Mann eintreten darf, entscheidet der Türhüter: er allein kann den Eintritt gewähren oder versagen";
    label ru official "Войти ли просителю — решает привратник: только он даёт вход и только он его не даёт";
    for m: Person;
    when eintritt_erbeten(m) and tuerhueter_gewaehrt_einlass(m);
    then einlass_gestattet(m);
}

The long labels are left as recorded in the package. The conclusion’s meaning is set by the when and then lines: if the man asked for entry and the doorkeeper permitted him to enter, then entry is permitted to him. The labels explain the rule; they add no conditions or conclusions of their own.

The first premise is already supported by the fact of the request. The second calls for a decision. The rule stays strict, strict: new here is the origin of one of its premises.

Before the decision is supplied

Start with the scenario VG-01. It states a context but no further assertions. Leave the date values as in the starting example: for now we change only the information about the decision.

test "VG-01 впуск без ответа привратника: REQUIRES_JUDGMENT, орган Tuerhueter" {
    given {
        context {
            decision_time @1000-01-05T12:00:00Z;
            knowledge_time @1000-01-05T12:00:00Z;
            legal_time @1000-01-05;
            timezone "UTC";
        }
    }

    evaluate truth(einlass_gestattet(Mann));
    expect evaluation_status == REQUIRES_JUDGMENT;
    expect truth_status == NEITHER;
    expect judgment_requests(1);
    expect judgment_request(tuerhueter_gewaehrt_einlass);
}

The first two expectations check different sides of the answer. truth_status == NEITHER means there is no support for the assertion of permitted entry, either for or against. evaluation_status == REQUIRES_JUDGMENT refines the reason: the derivation depends on a missing premise that calls for an outside decision.

The last two lines check the request itself. judgment_requests(1) expects one judgment request; judgment_request(...) checks which relation it concerns. So the test demands naming the missing decision, not only returning NEITHER.

All scenarios of this file can be run from the reader companion directory:

law engine test corpus/laws/fiction/kafka/vor-dem-gesetz/tests/vor-dem-gesetz.lawtest \
  --program corpus/clir/de-vor-dem-gesetz.lawir.json --imports \
  contexts/de-vor-dem-gesetz.json

To see the explanation of a single question, use a separate file containing the same case:

law engine explain \
  corpus/laws/fiction/kafka/vor-dem-gesetz/tests/01-entry-requires-the-doorkeepers-judgment.lawtest \
  \
  --program corpus/clir/de-vor-dem-gesetz.lawir.json

The start of the explanation looks like this; the node’s long address is omitted here:

der Einlaß ist ihm gestattet(Mann): NEITHER
  judgment  der Türhüter gewährt diesem Mann den Einlaß(Mann)

Author’s paraphrase of the engine output above (the engine’s text is in German and is quoted verbatim; what follows is the author’s English retelling): “entry is permitted to him” (Mann) — NEITHER; the missing piece is a judgment — “the doorkeeper grants this man entry” (Mann).

The judgment node shows which decision is missing. That is a description of the request. Running the command neither contacts the doorkeeper nor obtains a decision. Asking the human and recording the decision still lie ahead.

Supplying consent

Now consider a hypothetical version of the scene: the doorkeeper has agreed to let the petitioner in. We change the example’s input information; we ascribe no such continuation to the parable. In the scenario VG-02 an entry appears inside given:

assert tuerhueter_gewaehrt_einlass(Mann) {
    id "assert-adj0";
    origin adjudicated;
}

origin adjudicated marks the assertion as a supplied decision. It concerns the same man the question is asked about. Now both premises of the EinlassGestattet rule are supported, and the expectations change:

evaluate truth(einlass_gestattet(Mann));
expect evaluation_status == COMPUTED;
expect truth_status == TRUE_ONLY;
expect judgment_requests(0);

The conclusion receives TRUE_ONLY, the calculation COMPUTED, and there are no more judgment requests. The explanation shows the rule applied on two grounds: the request from the package and the decision from given.

The adjudicated mark reports how the entry is presented. By itself it does not certify who entered it, nor that this person is truly entitled to decide the question. In the shown example we supply a decision; checking its provenance remains a separate task. The authority declaration lets us name the required participant, but it does not replace such a check[^chapter-9-origin].

Supplying a refusal

In the scenario VG-03 one word changes:

assert not tuerhueter_gewaehrt_einlass(Mann) {
    id "assert-adj0";
    origin adjudicated;
}

not supplies an explicit negative answer: the doorkeeper does not grant entry. This is a refusal, not an absence of a decision. Before reading the expectations, ask yourself: what has become known about the doorkeeper’s decision, and what now follows about permitted entry?

The judgment itself has received negative support. But the question still concerns a different relation, einlass_gestattet:

evaluate truth(einlass_gestattet(Mann));
expect evaluation_status == COMPUTED;
expect truth_status == NEITHER;
expect judgment_requests(0);

The result is NEITHER again. The rule concludes permission from consent; under refusal its positive premise fails. The package holds no rule that would conclude not einlass_gestattet(m) from that refusal. Denying the premise does not automatically turn into denying the conclusion.

The calculation still has the status COMPUTED and no longer calls for the doorkeeper’s decision: the decision is already supplied. If you run why-not for separate scenario 03, the explanation will point at EinlassGestattet and the premise’s FALSE_ONLY state. Here it is known why the rule did not fire.

Compare the three cases for the same permission question:

Two identical NEITHERs hide different situations. In the first case a decision is still called for; in the third it is known but gives support to neither answer to our question. The value COMPUTED also promises neither “yes” nor “no”: a calculation can finish with no support on either side of the conclusion being queried.

What exactly the text says

A natural doubt remains: the doorkeeper did say “not now”. Why does the first scenario wait for a decision at all?

In the model his words are kept as a separate fact:

@source(TO_JETZT_NICHT, TO_NOCH_NICHT)
assert einlass_jetzt_versagt(DerTuerhueter, Mann) { evidence VDG_1915_TEXT; }

The relation einlass_jetzt_versagt records the refusal of entry for now. The words about a later possible entry are recorded by one more relation, einlass_spaeter_moeglich. No rule links these facts to the outside judgment tuerhueter_gewaehrt_einlass.

So the first scenario means exactly the absence of a supplied judgment in this formalization. From it one cannot conclude that the character said nothing or made no decisions at all. Another formalization can be proposed that reads his words as a negative judgment. Then the links between the facts and the answer will change; those links are what should be discussed when comparing readings.

And the open gates stay open meanwhile. A separate scenario 04 asks about the free way:

evaluate truth(weg_frei(entity_ref("urn:de:kafka:clir:vor-dem-gesetz#Mann")));
expect result_kind == PROPOSITION;
expect truth_status == TRUE_ONLY;
expect evaluation_status == COMPUTED;

The rule WegIstFrei rests on the information about the petitioner, the gates of the Law, and their open state. The doorkeeper’s decision is not among its conditions. So this question receives TRUE_ONLY and COMPUTED without a supplied judgment. Waiting for a decision belongs to one particular question; it does not block every answer of the model.

Try changing the decision

Work with a copy of the file vor-dem-gesetz.lawtest, keeping the file header and one test VG-02 in it. For each trial start from that copy, so changes do not accumulate.

1. Delete from given the assertion with origin adjudicated. Keep the expectations at first and run the test. The check must point out a mismatch in the answer state, the calculation status, and the number of requests. Account for each result, then record the expectations for the case without a supplied decision.
2. Restore the assertion and add not before the relation. Predict the permission question’s result. Then replace the question itself with truth(tuerhueter_gewaehrt_einlass(Mann)). Why is FALSE_ONLY now expected, although the permission question gave NEITHER?
3. Compare the explanation of the open way from scenario 04 with the decision-free permission’s explanation from scenario 01. Find the first conclusion’s grounds and the second’s missing premise. Which information does each of these questions need?

We have learned to reserve a specific question for a human decision and to continue the derivation once that decision is supplied. The next step is to distinguish an act from its normative position: whether it is permitted, required, or prohibited. Open gates, permission to enter, and actually entering already give us three different subjects of conversation.

No single published English translation of Kafka’s “Before the Law” was adopted for this chapter: the German quotations above stay in German, each with a brief English gloss beside it, and all English renderings of Kafka’s text in this chapter are the translator’s own.

[^chapter-9-source]: Franz Kafka, “Before the Law” (“Vor dem Gesetz”), first printed in Selbstwehr, 1915. The pinned German text and the fragment registry. The open gates and the free way are described in 01-tor.law. [^chapter-9-judgment]: The Arxo specification, §47.3: external judgment; the entry declaration and rule. The occasions without a decision, with consent, and with refusal are VG-01–VG-03. [^chapter-9-origin]: §47.3.1 tells apart an answer with a judgment object from the compatible form without one. In the first, authority and payload form are checked; the shown entry uses the second. On the provenance of assertions, see §73.