First Check That the Object Exists

In the first part, the conclusion about amphiproticity required two abilities of a single particle. If one of the premises was not established, the rule did not apply. Now consider a similar problem with numbers: we are given the lengths of three sides and must find out whether they form a right-angled triangle.

For sides 3, 4, and 5 the answer is familiar: the square on five equals the sum of the squares on three and four. Here “the square on” a side means the square of that side’s length. But before using the right-angle test, we must make sure that the given sides can form a triangle at all. Let us record both steps so that one conclusion becomes a premise for the other.

We will work with the package on Euclid’s Elements. Proposition I.20 states the triangle inequality: the sum of any two sides of a triangle is greater than the third. Proposition I.48 gives the test for a right angle: if the square on one side of a triangle equals the sum of the squares on the other two, the angle between those two sides is right. In the package, separate rules correspond to these propositions[^chapter-5-euclid].

How to record three lengths

Objects of the new vocabulary have the type Trigonon. Its name means “triangle”, but assigning an object to this type does not yet confirm that the given lengths form a triangle. The object lets us gather information about one figure under consideration; we will establish separately whether its side lengths can form a triangle.

The relation pleurai records lengths:

relation pleurai(t: Trigonon, a: Integer, b: Integer, c: Integer)
    kind empirical {
    key(t);
    label grc unofficial "αἱ τρεῖς πλευραὶ τοῦ τριγώνου";
    label ru unofficial "три стороны треугольника в порядке записи дела; единица длины у всех трёх одна и та же по построению записи — величины безразмерны (Integer), и вопрос пакета от неё не зависит";
}

There are four arguments here. The first, t, denotes an object of type Trigonon. The other three denote the side lengths in the order of recording. Each carries the type Integer, a whole number. Thus the familiar declaration of a relation lets us join an object with numerical information about it.

Numbers are written without quotes. Here is the assertion from the scenario with three unit sides:

assert pleurai(entity_ref("urn:case:eucl:trigonon"), 1, 1, 1) {
    id "eucl-t10-1"; origin case_input;
}

First comes the reference to the object urn:case:eucl:trigonon, then the values 1, 1, and 1. The assertion’s name eucl-t10-1 and its origin case_input are already familiar.

This model assumes that all three lengths are expressed in one unit. The Integer values themselves store no units: from the record alone one cannot tell whether they were centimetres or metres, or check that the units were consistent. So convert all lengths to one unit before entering the numbers. For our questions, what matters are the ratios of the lengths, which stay the same when all lengths are scaled together. We will consider quantities with explicitly stated units in chapter 15.

The line key(t) binds one object to one triple of side values. If two different triples are accepted for the same object, a key conflict arises; the later entry does not replace the first. Repeating the same triple does not by itself mean a difference of values. We will examine consistency checks in detail later; here each case will contain one assertion about the sides[^chapter-5-key].

The code grc in the labels stands for Ancient Greek, and ru for Russian. In the explanations below, the tool uses the Greek labels. You do not need to read Greek to follow the explanation: the rule and entry names let us match each step against the code.

First rule: do the sides form a triangle

Let us check each pair of sides. The sum of the first and second must be greater than the third, of the second and third greater than the first, of the first and third greater than the second. For the triple 1, 1, 1, all three checks come down to one true inequality: two is greater than one.

In the model this is recorded by the rule TrigononEstin:

@source(STO_I20)
rule TrigononEstin strict {
    label grc official "Παντὸς τριγώνου αἱ δύο πλευραὶ τῆς λοιπῆς μείζονές εἰσι πάντῃ μεταλαμβανόμεναι";
    label ru unofficial "I.20: тройка составляет треугольник — каждые две стороны, взятые вместе, строго больше третьей";
    for t: Trigonon;
    for a: Integer;
    for b: Integer;
    for c: Integer;
    when pleurai(t, a, b, c) and (a + b > c) and (b + c > a) and (a + c > b);
    then trigonon_estin(t);
}

The rule has four variables. The line for t: Trigonon introduces the object, and the three lines with Integer introduce the numerical variables a, b, c. When the premise pleurai(t, a, b, c) is matched against our entry, all three receive the value 1.

The remaining conditions are comparisons. The sign + denotes addition, > means “strictly greater”. Parentheses group each comparison, and and requires all conditions to hold, as in the rule about amphiproticity. Equality of the sum with the third side is not enough.

The conclusion trigonon_estin(t) reads: “the given sides form a triangle”. In the vocabulary this relation is declared with the mark kind derived. That is how a property obtained by derivation is marked here. This mark and the familiar institutional are different kinds of relations; by themselves they neither change the meaning of the four states nor perform inference. In our case the ground is the application of a particular rule to the assertion about the sides.

The scenario with unit sides states a question and expectations:

evaluate truth(trigonon_estin(entity_ref("urn:case:eucl:trigonon")));
expect result_kind == PROPOSITION;
expect truth_status == TRUE_ONLY;
expect evaluation_status == COMPUTED;

This is an excerpt from the complete file. The new line result_kind == PROPOSITION checks the kind of result: the query returns a proposition whose support can be assessed. The line with truth_status checks its state, and COMPUTED checks that the calculation ran. These three checks concern different properties of the result.

Run the supplied file from the reader companion directory:

law engine test \
  corpus/laws/doctrine/math/euclid-pythagoras/tests/10-trigonon-estin-111.lawtest \
  --program corpus/clir/grc-euclid-pythagoras.lawir.json --imports \
  contexts/grc-euclid-pythagoras.json

The check passes: TRUE_ONLY. Only the subject and the file paths changed; the procedure is the same. The file already contains the needed header and scenario context; for this trial they need no changes.

When the inequality fails

Take sides 1, 2, and 3. The first two together equal the third: the strict inequality fails. Geometrically this is a degenerate case: the segments can be laid along one straight line, but they do not form an ordinary triangle.

The rule TrigononEstin does not apply. But the package contains a separate rule for concluding that the sides cannot form a triangle:

@source(STO_I20)
rule OudeTrigononPleuraiAB strict {
    label grc official "αἱ μὲν ΒΑ, ΑΓ τῆς ΒΓ";
    label ru unofficial "I.20 нарушено первой парой: первая и вторая стороны, взятые вместе, не больше третьей — тройка не составляет треугольника";
    for t: Trigonon;
    for a: Integer;
    for b: Integer;
    for c: Integer;
    when pleurai(t, a, b, c) and (a + b <= c);
    then oude_trigonon(t);
}

The sign <= means “less than or equal”. It covers both a third side that is too long and the boundary case of equality. For our triple, 1 + 2 <= 3 holds, so the conclusion oude_trigonon(t) follows — “the sides do not form a triangle”.

Note the form: oude_trigonon is the name of a separate relation. There is no construction then not trigonon_estin(t) in the rule. The negative sense of the label does not turn one relation into an explicit negation of the other. So the question about oude_trigonon receives TRUE_ONLY, while trigonon_estin on this case stays NEITHER.

In the third chapter we already saw an explicit not. What matters here is recognizing the distinction in a real vocabulary: a separately named property and the negation of another property are linked only by the rules actually recorded. A similarity in meaning is not enough for such an inference.

For the other two pairs of sides the package contains analogous rules: OudeTrigononPleuraiBC and OudeTrigononPleuraiAC. They let us see which sum exactly failed to exceed the remaining side. For the triple 1, 2, 3, only the shown rule for the first and second sides fires.

Second rule: is there a right angle

Now return to sides 3, 4, and 5. They pass all three inequalities: 7 is greater than 5, 9 greater than 3, 8 greater than 4. For these sides, trigonon_estin is established. It can be used as a premise of the next rule:

@source(STO_I48)
rule OrthogonionProsTritei strict {
    label grc official "Ἐὰν τριγώνου τὸ ἀπὸ μιᾶς τῶν πλευρῶν τετράγωνον ἴσον ᾖ τοῖς ἀπὸ τῶν λοιπῶν τοῦ τριγώνου δύο πλευρῶν τετραγώνοις, ἡ περιεχομένη γωνία ὑπὸ τῶν λοιπῶν τοῦ τριγώνου δύο πλευρῶν ὀρθή ἐστιν";
    label ru unofficial "I.48, угол против третьей стороны: квадрат третьей равен сумме квадратов первых двух — треугольник прямоугольный";
    for t: Trigonon;
    for a: Integer;
    for b: Integer;
    for c: Integer;
    when trigonon_estin(t) and pleurai(t, a, b, c)
        and (a * a + b * b == c * c);
    then orthogonion(t);
}

Start with the familiar parts. The variable t denotes the same object, and a, b, c receive the lengths from pleurai. The premise trigonon_estin(t) requires the established existence of a triangle with these sides.

The arithmetical condition uses multiplication * and an equality check ==. The expression a * a is the square of the first length. For the triple 3, 4, 5 we get 9 + 16 == 25. All conditions hold, and the rule derives orthogonion(t): the triangle is right-angled.

This rule checks the case in which the square of the third side equals the sum of the other two squares. Two more rules check the corresponding equalities for the first and second sides. So the package does not require the longest side always to be recorded last[^chapter-5-rules].

Read the explanation of the supplied case with sides 3, 4, 5:

chapter5_explain=$(mktemp -d)
python3 reader_tools/prepare_question.py corpus/laws/doctrine/math/euclid-pythagoras/tests/01-aigyptiako-345.lawtest \
  --program corpus/clir/grc-euclid-pythagoras.lawir.json --imports \
  contexts/grc-euclid-pythagoras.json --out "$chapter5_explain"
law engine explain "$chapter5_explain"

Below is the output with shortened rule-application identifiers:

ὀρθογώνιόν ἐστι τὸ τρίγωνον(trigonon): TRUE_ONLY
  rule_application  ὀρθογώνιόν ἐστι τὸ τρίγωνον(trigonon)
    (urn:proof:apply:OrthogonionProsTritei:5afa6b14…)
    rule_application  τρίγωνόν ἐστιν(trigonon)
      (urn:proof:apply:TrigononEstin:6c0e0a77…)
      assertion  αἱ τρεῖς πλευραὶ τοῦ τριγώνου(trigonon, 3, 4, 5)
        (urn:proof:assert:urn:grc:eukleides:clir:pythagoras#eucl-t01-1)
    assertion  αἱ τρεῖς πλευραὶ τοῦ τριγώνου(trigonon, 3, 4, 5)  ↑ раскрыт выше
      (urn:proof:assert:urn:grc:eukleides:clir:pythagoras#eucl-t01-1)

Author’s paraphrase of the engine output above: the triangle is right-angled (TRUE_ONLY) by applying the rule OrthogonionProsTritei, which itself rests on an application of TrigononEstin — both grounded in the entry eucl-t01-1 about sides 3, 4, and 5.

Under OrthogonionProsTritei we see the application of TrigononEstin, and under it the source assertion eucl-t01-1 about the sides. Now one rule’s conclusion serves as another’s premise. The same assertion about the sides is also needed for checking the squares; the mark “раскрыт выше” (“expanded above”) shows a repeated reference to it.

The arithmetical comparisons themselves are not written out as separate lines in this textual explanation. They can be checked in the rule’s condition by substituting the numbers from the source entry. So the explanation and the code complement each other.

The equality holds, but there is no triangle

Take sides 0, 3, and 3. The arithmetic checks out: zero squared plus nine equals nine. But the sum of the zero side with either of the other two is not greater than the remaining one. The triple fails the triangle-existence condition.

The check set contains a scenario with two questions about this case:

test "EUCL-16-GATE-033" {
    given {
        context {
            decision_time @2026-08-26T12:00:00+05:00;
            knowledge_time @2026-08-26T12:00:00+05:00;
            legal_time @2026-08-31;
            timezone "Asia/Qyzylorda";
        }

        assert pleurai(entity_ref("urn:case:eucl:trigonon"), 0, 3, 3) {
            id "assert-sides";
            origin case_input;
        }
    }

    evaluate truth(orthogonion(entity_ref("urn:case:eucl:trigonon")));
    expect truth_status == NEITHER;
    expect issues_within(info);

    evaluate truth(oude_trigonon(entity_ref("urn:case:eucl:trigonon")));
    expect truth_status == TRUE_ONLY;
    expect issues_within(info);
}

Each evaluate starts a new question, and the expect lines following it state expectations for that question only. The two questions share the same source information. The dates belong to the context of the test case and do not mark the time the Elements were composed.

The expectation issues_within(info) bounds the severity of diagnostic messages: there must be no messages above the informational level. It checks how the evaluation ran, and does not replace stating the expected answer status. We will examine violations of requirements in the next chapter.

Run the complete set containing this scenario as follows:

law engine test corpus/laws/doctrine/math/euclid-pythagoras/tests/pythagoras.lawtest \
  --program corpus/clir/grc-euclid-pythagoras.lawir.json --imports \
  contexts/grc-euclid-pythagoras.json

The two answers differ:

The first answer does not mean “the triangle is not right-angled”. The right-angle rule’s applicability condition is not met: trigonon_estin is not established. The second answer has grounds of its own: the inequalities for two pairs of sides are violated. The equality of the squares does not make up for the missing premise.

To see the reason for the first answer, use the separate supplied file with one question about the same triple:

chapter5_why_not=$(mktemp -d)
python3 reader_tools/prepare_question.py corpus/laws/doctrine/math/euclid-pythagoras/tests/05-pyle-033.lawtest \
  --program corpus/clir/grc-euclid-pythagoras.lawir.json --imports \
  contexts/grc-euclid-pythagoras.json --out "$chapter5_why_not"
law engine why-not "$chapter5_why_not"

In the analysis, three rules about the right angle are named. In each, find the premise τρίγωνόν ἐστιν(trigonon) with the status NEITHER: this is the Greek label of trigonon_estin. The text also contains messages about side variables not linked to the query’s goal. They belong to the rule’s analysis and do not mean that the equality of the squares was computed and found false. Here, the absence of the needed premise can be checked directly against the inequalities of the sides.

Try it yourself

Work on copies of the supplied files. Replace the scenario file’s path with your copy’s path. For test, it follows the command name; in the explain and why-not sequences, it follows the preparation script name. The prepared model after --program stays the same. Try all three exercises before reading the discussion below.

1. Copy pythagoras.lawtest, keeping the three header lines and only the scenario EUCL-16-GATE-033. Replace sides 0, 3, 3 with 5, 12, 13. First keep the old expectations and predict both answers. After running, explain the mismatches and correct the expectations for the new case.
2. In a copy of 02-ekfylismenon-123.lawtest, replace sides 1, 2, 3 with 2, 3, 5. This file asks about oude_trigonon. Name the rule that must apply, and check the old TRUE_ONLY expectation. Confirm the ground via explain.
3. In a copy of 01-aigyptiako-345.lawtest, reorder the sides: instead of 3, 4, 5 record 5, 3, 4. Will the answer about right-angledness change? Which rule must now appear in the explanation instead of OrthogonionProsTritei?

Check your predictions

In the first exercise, right-angledness will receive TRUE_ONLY, and the “not a triangle” assertion NEITHER. The status expectations must be swapped; the issues_within(info) checks stay. In the second, OudeTrigononPleuraiAB will apply: the sum of 2 and 3 equals 5. In the third, the answer will stay TRUE_ONLY, and the right-angle test will apply OrthogonionProsProtei, for the first side. The changed numbers explain the new results; the rules are unchanged.

We added numerical arguments, comparisons, and a chain of two rules to the familiar way of recording. The main distinction stayed the same: to obtain a conclusion, all its premises must be established. Naming the object a triangle in the vocabulary, or checking the equality of the squares, is still not enough.

Next we will consider another problem: how to record a requirement on the consistency of information, and how to tell its violation apart from deriving a new property.

[^chapter-5-euclid]: Euclid, Elements, I.20 and I.48: the right-angle test, the electronic edition of David Joyce. The package’s Greek fragments are pinned in sources.law. The English renderings of the propositions in this chapter are the translator’s own. [^chapter-5-key]: The Arxo specification, §§45–45.1: kinds of relations and key constraints. The declaration of pleurai is in the package vocabulary. [^chapter-5-rules]: The triangle-existence rules and the three right-angle rules. Each right-angle rule requires trigonon_estin(t).