IndisputableMonolith.Loom.Semantics
Semantic layer for the Loom: interpretations of relational atoms over a finite universe Fin n, plus assignment and expression evaluation. Relations are predicates on argument lists, so arity is free. Separation and kernel checks import this module to compare models of two surface-identical formulas. Structure is definitional: Model, Assign, evalExpr, and SeparatedBy, with no deep proofs here.
claimA model over universe $\mathrm{Fin}\, n$ assigns to each relation symbol a predicate on finite argument tuples (arity unconstrained). An assignment maps roles to elements of the universe. Expression evaluation interprets grammar terms under a model and assignment; two contents are separated when some model makes one true and the other false.
background
The Loom grammar (upstream) treats content as an inductive Expr and maps it by weave to configurations of closed walks. Five production rules are forced by matching algebraic operations on configurations to content operators: ordered product of letters for a relation on roles, and dual constructions for the remaining connectives.
Semantics sits under that grammar. A model is an interpretation on $\mathrm{Fin}, n$: each relation is a predicate on the argument list the atom actually carries, so no global arity table is required. Assignments send role variables into the universe; evaluation walks the expression tree under those data.
The local setting is model-theoretic separation for woven content: same surface relations, different quantifier/skolem shape, distinguished by existence of a finite model.
proof idea
This is a definition module, not a proof development. It introduces the carrier types and the recursive evaluators: Model as relation-interpretation over Fin n, Assign as role-to-element maps, evalExpr as the standard inductive interpretation of grammar expressions, and SeparatedBy as the existence of a model (and assignments) witnessing truth of one content and falsity of the other. Downstream modules import these definitions; no nontrivial lemmas are discharged here.
why it matters in Recognition Science
Feeds Loom.Separation, which checks a kernel-level separation witness for two contents that assert the same two relations on doors and keys but differ in quantifier pattern: (A) every door has some key that opens it, and one master key locks every door, versus (B) every door has some key that locks it, and one master key opens every door. B is the security hole; A is not. Without a finite-model semantics and an evaluation function, that distinction cannot be stated inside the kernel.
In the broader Recognition stack the Loom is the linguistic front end that turns structured content into walk configurations. Semantics is the bridge that lets separation (and later soundness) talk about truth in a model rather than only about syntactic weave shape.
scope and limits
- Does not prove soundness or completeness of weave relative to models.
- Does not construct the door/key separation witness; that lives in Loom.Separation.
- Does not fix a signature or bound arities in advance.
- Does not address infinite universes or continuous domains.
- Does not define the five grammar production rules; those are in Loom.Grammar.