SeparatedBy
plain-language theorem explainer
Two Loom expressions count as different claims when a finite model and name-assignment make one true and the other false. Separation witnesses cite this predicate; bare syntactic inequality is not enough. The body is Boolean inequality of the shared finite-universe evaluator, with a decidable instance by unfolding.
Claim. Fix a universe size $n$, a model $M$ on $\mathrm{Fin}\,n$ (a predicate saying which relation tuples hold), and an assignment of bound names to elements. Expressions $a$ and $b$ are separated by $M$ and that assignment when their truth values under the finite-model evaluator differ.
background
The Loom semantics module gives content a meaning so that "different claims" is not a matter of taste. The separation theorem needs two utterances in different gauge orbits only when they really disagree as claims: two formulas can differ as trees yet agree under every reading, and that pair would embarrass the language rather than witness a distinction.
A model on universe size $n$ is a map from predicate indices and argument lists in $\mathrm{Fin},n$ to Booleans; arity is whatever the atom brings. An assignment sends bound names to elements of that finite universe. Evaluation is the plain reading: atoms look up the model's holds-predicate (with optional denial), conjunction is Boolean and, and quantifiers range over the shared finite carrier. Expressions are already in negation-normal form, so denial lives on the atom.
The load-bearing choice is one shared sort for every bound name. A two-sorted reading would separate more pairs but would be a stronger assumption and a weaker witness; a probe showed most of the searched family already separates on this plainer reading.
proof idea
Definitional: the predicate is exactly inequality of the two Boolean values returned by the finite-model evaluator on the given model, assignment, and pair of expressions. The accompanying decidable instance unfolds the definition and reuses the existing decidable equality on Bool.
why it matters
This is the semantic distinctness property a Loom separation witness must discharge. Downstream, witnessC_and_D_are_different_claims proves the concrete witness pair is separated under a fixed finite model and constant assignment, by decide. Without it, the separation theorem would only show syntactic or gauge-orbit difference, which the module doc flags as potentially empty. It sits in the Loom layer that turns Recognition-style content into checkable claims before any physics constants or forcing-chain steps are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.