# Set difference is not commutative

KL-FCS-063 · Relational algebra · version 1.0.0

## Problem

Decide the proposed set identity over every triple of finite-universe relations.

## Context

Check query identities over explicit finite set semantics, and retain counterexamples to invalid rewrites.

## Definitions

- **Set semantics**: Each value occurs at most once; duplicates and NULLs are absent.
- **Relational identity**: Two query expressions with the same output on every admitted relation.
- **Counterexample**: A concrete set assignment making the outputs differ.

## Checked result

Equivalent on the stated domain: no.

The finite universe makes every relation assignment enumerable. The sample output illustrates the identity or supplies a direct refutation.

## Checker reasoning

1. Enumerate every subset of the universe.
2. Evaluate both expressions on every triple of sets.
3. Compare the complete finite-domain outputs.
4. Replay a concrete sample, including a differing output for a false identity.

## Dataset construction

{
  "family": "relational-algebra",
  "task": "Decide the proposed set identity over every triple of finite-universe relations.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Complete relation assignments · 64 triples",
  "acceptance": [
    "Enumerate every subset of the universe.",
    "Evaluate both expressions on every triple of sets.",
    "Compare the complete finite-domain outputs.",
    "Replay a concrete sample, including a differing output for a false identity."
  ],
  "generation": "Deterministic finite fixture; full enumeration or witness replay as stated.",
  "split_policy": "Reference corpus for exposition and reproduction; no train/test evaluation split is claimed."
}

## Formal payload

```json
{
  "specification": {
    "universe_size": 2,
    "law": "difference-commutativity",
    "semantics": "Mathematical sets; unique values; no NULL or tuple multiplicity."
  },
  "claim": {
    "equivalent_on_domain": false
  },
  "witness": {
    "sample": {
      "A": [
        0
      ],
      "B": [],
      "C": [],
      "left": [
        0
      ],
      "right": []
    }
  }
}
```

## Complexity

A universe of n values has 2ⁿ subsets; three relation inputs create 2³ⁿ assignments.

## Limits

Finite enumeration is bounded to this universe; these artifacts do not certify an SQL optimizer or measured execution speed.

## Common error and further work

SQL bag semantics, NULL values, and outer joins can invalidate a rewrite valid for mathematical sets.

Add equijoin trees, bag multiplicities, NULL handling, and an explicit query-cost model.

## Verification

Complete relation assignments · 64 triples. 64 checker units.
Replay with `python3 tools/verify.py`. Mechanical status: checked; human review
has not yet been recorded. Custom Python verification, not a proof-assistant
claim. Checker 1.0.0 and exact source hashes are in `verification.json`.

## Provenance and references

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11.
No external dataset or model-generation experiment. Reuse-license selection
remains pending.

- [Conceptual reference](https://www.postgresql.org/docs/current/explicit-joins.html)