Markdown for LLMs

Define necessary and sufficient conditions

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

# Define necessary and sufficient conditions

## Intent

I want to derive a concept from sufficient conditions and check its necessary conditions.

A backward step does not appear on its own.

## Wrong form and why it stays silent

```text title="Incorrect form"
// Из not young(p) автоматически получают not eligible(p).
```

exact creates a forward strict rule and a necessary constraint. Negative classification and backward inference do not arise automatically.

## Correct form

```law
language "law.core" version "0.2";
package recipes.g.r01 version "0.1.0";
namespace "urn:recipe:g-concepts:01";

entity Person;
relation young(p: Person) kind empirical;
definition eligible(p: Person) exact { when young(p); }
```

## Frozen execution scene

| Facts on 13.09.2026 | Question | Answer |
|---|---|---|
| sufficient condition | `truth(eligible(entity_ref("urn:recipe:g-concepts:01:p")))` | `truth_status == TRUE_ONLY;` / `COMPUTED` |
| no contraposition | `truth(eligible(entity_ref("urn:recipe:g-concepts:01:p")))` | `truth_status == NEITHER;` / `COMPUTED` |
| no backward inference | `truth(young(entity_ref("urn:recipe:g-concepts:01:p")))` | `truth_status == NEITHER;` / `COMPUTED` |
| necessity violated | `truth(eligible(entity_ref("urn:recipe:g-concepts:01:p")))` | `truth_status == TRUE_ONLY; issue(CONSTRAINT_VIOLATED);` / `NON_EXECUTABLE` |

```law
test "sufficient condition holds" {
    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 young(entity_ref("urn:recipe:g-concepts:01:p"));
    }
    evaluate truth(eligible(entity_ref("urn:recipe:g-concepts:01:p")));
    expect truth_status == TRUE_ONLY;
    expect evaluation_status == COMPUTED;
}
```

```law
test "no contraposition" {
    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 not young(entity_ref("urn:recipe:g-concepts:01:p"));
    }
    evaluate truth(eligible(entity_ref("urn:recipe:g-concepts:01:p")));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;
}
```

```law
test "no converse derivation" {
    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:g-concepts:01:p"));
    }
    evaluate truth(young(entity_ref("urn:recipe:g-concepts:01:p")));
    expect truth_status == NEITHER;
    expect evaluation_status == COMPUTED;
}
```

```law
test "violated necessity blocks document" {
    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:g-concepts:01:p")); assert not young(entity_ref("urn:recipe:g-concepts:01:p"));
    }
    evaluate truth(eligible(entity_ref("urn:recipe:g-concepts:01:p")));
    expect truth_status == TRUE_ONLY; expect issue(CONSTRAINT_VIOLATED);
    expect evaluation_status == NON_EXECUTABLE;
}
```

Constraint verdicts are read from separate CONSTRAINT results and checked together with constraint_check nodes.

```python
>>> import runpy
>>> check = runpy.run_path("docs/recipes/g-concepts/resources/check.py")
>>> check["check_constraints"](https://github.com/arxohq/law/blob/master/docs/recipes/g-concepts/1)
'Г1: вердикты ограничений проверены; lawc = lawref'
```

## Counterfactual

Mutation `definition eligible(p: Person) exact` → `relation eligible(p: Person);
definition eligible(p: Person) exact`: LDC-E1201.

## Boundary

The compiler itself declares the definition symbol: a separate relation of the same name is rejected with E1201/E1338. The minimal working form above does not duplicate the declaration.

An issue with error severity forbids a COMPUTED document: CONSTRAINT_VIOLATED and KEY_CONFLICT make the whole document NON_EXECUTABLE. This does not erase the fact’s truth status and does not change the constraint verdict.

The necessary half yields a constraint finding, not a new young fact. Exceptions require classification defeasible or separate rules.