Do We Have All the Information?

In the last chapter a requirement could remain undetermined: no negative ground was available to confirm it. In the first examples the absence of an entry also left the question open. But sometimes we want to report not only separate pieces of information, but also that the supplied list is complete. Then a gap in it gains meaning.

Picture a list of points on a straight line. If it names A and B, nothing is yet known about point C. Now make the conditions more precise: C belongs to the drawing under consideration, and the list of points in that drawing that lie on this line is declared complete. Then C’s absence from the list becomes a ground for a negative answer. It matters to state exactly to which relation and which objects the word “all” refers.

What the drawing contains

Consider the package on David Hilbert’s Foundations of Geometry. Its source is the pinned English translation[^chapter-7-source]. The objects of the first examples are points and lines, and the source information reports which of them belong to the presented configuration and which points lie on which lines.

One feature of this package needs explaining before we begin. In our scenarios, separate answers about whether a point lies on a line are computed, but the drawing’s description violates some of the axioms’ requirements. In the reviewed public runtime, these incidence queries receive COMPUTED together with diagnostics of violated constraints. The violations concern requirements outside the chain of facts and rules on which these queries depend, so they do not block these answers. This differs from Chapter 6, where the violated constraints directly concern the queried property. We will examine the reasons for the violations after introducing closure: a declaration that specified information is complete within a defined domain.[^chapter-7-runtime]

The vocabulary calls the point type Punkt, the line type Gerade. Belonging to the configuration is recorded by two relations:

relation punkt_der_figur(p: Punkt) kind empirical {
    label ru unofficial "точка входит в предъявленную конфигурацию";
}

relation gerade_der_figur(l: Gerade) kind empirical {
    label ru unofficial "прямая входит в предъявленную конфигурацию";
}

Each has one argument of the corresponding type. The link between a point and a line is recorded by a separate relation:

@source(GDG_I_1)
relation liegt_auf(p: Punkt, l: Gerade) kind empirical {
    label en official "A lies upon a";
    label ru unofficial "точка лежит на прямой";
}

In liegt_auf(p, l) the point stands first, then the line. This is the familiar two-argument form, but now the arguments have different types. The German names here are the vocabulary’s identifiers. The Russian labels describe the same three relations explained above: a point belongs to the configuration, a line belongs to it, and a point lies on a line.

Scenario 01 records three points A, B, C and three lines ab, bc, ac. For each point and line there is an entry about belonging to the configuration. Positive assertions that a point lies on a line look like this:

The dash so far means only the absence of a positive entry. The source case contains no not liegt_auf assertion for these pairs. The table presents six positive liegt_auf entries. The complete scenario’s other entries list the objects and give them names via punktname and geradenname.

Where the negative answer comes from

Ask whether C lies on ab. The query and the first expectations in scenario 01 read:

evaluate truth(liegt_auf(entity_ref("urn:de:hilbert:case:point:C"), entity_ref("urn:de:hilbert:case:line:ab")));
expect result_kind == PROPOSITION;
expect truth_status == FALSE_ONLY;

FALSE_ONLY is expected, though the case contains no negative entry. To see the ground, run from the reader companion directory:

chapter7_explain=$(mktemp -d)
python3 reader_tools/prepare_question.py corpus/laws/doctrine/math/hilbert-grundlagen/tests/01-gerade-meidet-punkt.lawtest \
  --program corpus/clir/de-hilbert-grundlagen.lawir.json --imports \
  contexts/de-hilbert-grundlagen.json --out "$chapter7_explain"
law engine explain "$chapter7_explain"

The result:

A lies upon a(C, ab): FALSE_ONLY
  assertion  ¬ A lies upon a(C, ab)
    (urn:proof:closure:urn:de:hilbert:clir:grundlagen#InzidenzAbschluss:2)

Author’s paraphrase of the engine output above: C’s lying on ab is refuted (FALSE_ONLY), on the ground of an explicit negation derived by the closure InzidenzAbschluss — not on a case entry of its own.

The output uses the English label A lies upon a with the particular arguments C and ab. The sign ¬ denotes negation. The ground’s identifier contains proof:closure, then the name InzidenzAbschluss. This is a negative ground obtained by closure, not an assertion with a name of its own from the source case.

A closure declaration states that the information at hand counts as complete for a specified relation in a specified domain. For our relation it is declared as follows:

closure InzidenzAbschluss {
    label ru unofficial "замыкание §70: точка, не записанная лежащей на прямой, на ней не лежит";
    predicate liegt_auf;
    domain punkt_gerade_paar;
    snapshot "urn:de:hilbert:snapshot:inzidenz:1899";
    complete_as_of @1899-06-17T00:00:00Z;
    derive_explicit_negative true;
}

The word closure introduces the declaration, and InzidenzAbschluss gives its name. The field predicate liegt_auf names the relation the completeness concerns. The declaration does not automatically extend to all information in the package[^chapter-7-closure].

domain punkt_gerade_paar defines the domain of pairs inside which the closure acts. If such a pair belongs to the domain, and there is no positive ground for liegt_auf, the closure may yield a negative ground. In this package, positive grounds for liegt_auf come from source entries; in general, positive grounds derived by rules must also be taken into account.

The field derive_explicit_negative true allows deriving an explicit negation. The value true enables it. The obtained ground is visible in the explanation, so the negation can be distinguished from an entry written directly into the case.

The snapshot field holds the name of the snapshot to which the completeness declaration refers, and complete_as_of sets its time. These are different fields: an identifier and a time. The year 1899 in this entry is part of the model’s declaration. It does not by itself prove that our study drawing was composed then, or that the list truly contains no gaps. We will examine time in detail in chapter 13.

For which pairs the list counts as complete

Look at what punkt_gerade_paar means. In the vocabulary it is a relation with two arguments, a point and a line. A small rule derives it:

rule PunktGeradePaare strict {
    label ru unofficial "область инцидентности: точка и прямая взяты из конфигурации";
    for p: Punkt; for l: Gerade;
    when punkt_der_figur(p) and gerade_der_figur(l);
    then punkt_gerade_paar(p, l);
}

Read it in ordinary words: if a point belongs to the configuration and a line belongs to the configuration, their pair belongs to the closure’s domain. For our three points and three lines this yields nine pairs — every cell of the table.

In six cells there is a positive liegt_auf entry. For the remaining three pairs the closure yields a negation. In particular, C and ab belong to the domain, while there is no positive ground for that incidence. That is how FALSE_ONLY results, with the closure’s name in the explanation.

The bare listing of three points does not mean that no other points exist at all. What is declared complete is the liegt_auf relation for the pairs of this configuration. Such a declaration does not settle the broader question about all points of geometry.

A point outside the list

In scenario 04 the source drawing is the same, but the question is asked about point D and line ab:

evaluate truth(liegt_auf(entity_ref("urn:de:hilbert:case:point:D"), entity_ref("urn:de:hilbert:case:line:ab")));
expect result_kind == PROPOSITION;
expect truth_status == NEITHER;

Point D is not declared as belonging to the configuration. So the rule PunktGeradePaare does not create the pair of D and ab, and the closure does not apply to it. There is neither a positive entry that D lies on ab nor a negative ground. The answer is NEITHER.

Scenario 05 takes the next step. In it, D is added to the configuration; the entry essential for the domain looks like this:

assert punkt_der_figur(entity_ref("urn:de:hilbert:case:point:D")) { id "hilb-t05-d1"; origin case_input; }

The complete file also contains the point’s label via punktname. What is essential for bringing the pair into the domain is exactly the entry punkt_der_figur: line ab already belongs to the configuration. No information that D lies on ab has been added yet. Now the closure covers this pair and yields FALSE_ONLY.

Compare the three cases:

The transition from the second row to the third is caused by new information: we brought D into the configuration for which completeness is already declared. That changed what the missing entry means. Adding an object to the configuration brings new pairs into the closure’s domain. Do this deliberately: it can create negative conclusions about those pairs.

If instead the case states that D lies on ab, this pair will gain a positive ground. On a new run the closure will not create a negation from lack of support, since support exists. On that run the answer will become TRUE_ONLY.

What the scenario check confirms

Run the supplied scenario 01:

law engine test \
  corpus/laws/doctrine/math/hilbert-grundlagen/tests/01-gerade-meidet-punkt.lawtest \
  --program corpus/clir/de-hilbert-grundlagen.lawir.json --imports \
  contexts/de-hilbert-grundlagen.json

The check passes[^chapter-7-tests]. Besides the answer’s state, the file states three more expectations:

expect evaluation_status == COMPUTED;
expect issue(CONSTRAINT_VIOLATED);
expect issues_within(info, CONSTRAINT_VIOLATED);

The first requires exactly COMPUTED for this incidence query. The second, issue(CONSTRAINT_VIOLATED), checks that a message about a violated constraint is present. The third admits messages above level info only with the named code. It does not bound the number of such messages, nor confirm that no other undetermined requirements remain.

Thus test PASS means the result matches the recorded expectations. It does not mean that the drawing satisfies all the axioms. In this scenario the violation is expected and forms part of the checked result. For scenarios 04 and 05 the same expectations of execution status and diagnostic messages are used.

A complete list is not yet a model of geometry

Which requirements does the configuration violate? The description contains a triangular configuration of three points, but no shared plane is named. Under the package’s closures, the absence of the required plane violates the constraint AxiomI3.

The constraints AxiomII2Innen and AxiomII2Fortsetzung check for an intermediate point and a continuation past a segment’s end. Our list contains no corresponding information, and the closures turn their absence into negative grounds. These requirements are violated as well.

An ordinary finite drawing and a complete geometrical model are different subjects. In picturing a line, we do not draw all its points one by one. But in the presented finite description the package considers the listed objects and the explicitly stated domains of completeness. The axioms’ conditions may require objects and links that this description does not supply.

So the negative answer about C and ab must be read together with the execution status. It shows the consequence of declaring completeness for the given pair. The violated constraints show that the configuration as a whole does not meet the checked requirements. The incidence answer and the constraint diagnostics must both be read.

Other requirements may remain undetermined. In I.7, for instance, the presence of three non-collinear points in a plane and four non-coplanar points in space is checked. If only a plane or a spatial configuration is declared, without the needed information about points, this package’s corresponding requirements receive UNDETERMINED. The liegt_auf closure does not establish completeness at once for all such properties.

These results concern this particular description of the configuration. It does not mean that the mathematical question of whether the needed points exist is unsolvable, or that the axiom itself is refuted. Here again the sixth chapter’s distinction is useful: missing ground and a detected violation are different results.

Try it yourself

Take copies of the supplied files, keeping the header and context. In the test and explain commands substitute the copy’s path; the path after --program stays the same. Change only the named entries, the question, and the state expectation you can justify. Keep the COMPUTED and diagnostics expectations for these incidence queries.

1. In a copy of scenario 01, ask whether A lies on bc. Do not change the source information. Predict the state and the ground’s kind: a case entry, a rule, or a closure. Then check the FALSE_ONLY expectation and read the explanation.
2. In another copy of scenario 01, ask about B and ab. First keep all entries: TRUE_ONLY is expected. Then delete only the assertion hilb-t01-14 reporting that B lies on ab. Predict the new answer, check the old expectation, and only then change it. Compare the grounds’ identifiers before and after deletion.
3. In a copy of scenario 05, add a positive liegt_auf assertion for D and ab with the new name book-d-ab. First keep the FALSE_ONLY expectation, then explain the mismatch and record a new one. Why does the negation by this closure not arise on the new run?

Check your predictions

In the first exercise the result will be FALSE_ONLY on the ground of InzidenzAbschluss. In the second, the source TRUE_ONLY rests on hilb-t01-14; after deletion, FALSE_ONLY will appear on a closure ground. In the third, the answer will become TRUE_ONLY and will rest on the case’s new entry. The named diagnostic expectations still hold under these changes.

In the first part the absence of an entry left the question open. Now we can find the extra condition that gives absence a meaning: declaring a certain relation complete in a certain domain. The next step is to read rules with exceptions and see how new grounds can change an earlier conclusion.

[^chapter-7-source]: Hilbert’s source and pinned translation. The relations, the domain rule, and the closure are in the package vocabulary. The English label A lies upon a is the package’s pinned wording, quoted verbatim in code; the surrounding prose renderings are the translator’s own. [^chapter-7-closure]: The Arxo specification, §70: local declarations of completeness. The domain must be finite and exactly stated; the absence of positive support is checked for the tuples belonging to it. [^chapter-7-tests]: Historical scenarios 01: C and ab, 04: D outside the configuration, and 05: D included. The runtime companion preserves these files and records their migration. Its copies expect COMPUTED for the independent incidence query while retaining the original truth-state and constraint-diagnostic expectations. [^chapter-7-runtime]: The runtime migration note records the reviewed CLI, the changed execution-status expectations and their checks. A diagnostic about another requirement does not make every answer non-executable; an answer depending on a violated blocking constraint still receives NON_EXECUTABLE.