evalExpr
plain-language theorem explainer
Boolean truth of a Loom expression in a finite model under a name assignment. Separation witnesses and claim-distinctness results cite this as the decidable satisfaction predicate. Defined by recursion on negation-normal form: atoms via the model's relation (optionally denied), conjunction as Boolean and, and quantifiers as finite all/any over the shared universe Fin n.
Claim. Fix $n\in\mathbb{N}$, a model $M$ on universe $\mathrm{Fin}\,n$ (a map from relation indices to predicates on argument lists), and an assignment $\rho$ of bound names to elements of $\mathrm{Fin}\,n$. The value of an expression $e$ is a Boolean: an atom with predicate $p$, arguments $\vec{a}$, and denial flag $d$ evaluates to $M(p)(\rho(\vec{a}))$ or its negation according as $d$ is false or true; a conjunction is Boolean conjunction of the subvalues; a universal (resp. existential) quantifier binding name $x$ holds iff the body holds for every (resp. some) update of $\rho$ at $x$ ranging over $\mathrm{Fin}\,n$.
background
The Loom semantics module fixes what content means so that "different claims" is not syntactic taste. The separation theorem needs two utterances in different gauge orbits only when they really disagree as claims: two formula trees can differ and still agree in every model, which would embarrass a witness. Hence content is interpreted, and distinctness becomes: exhibit one finite model where one holds and the other fails.
A model on $\mathrm{Fin},n$ is a map sending each relation index to a Boolean predicate on lists of universe elements (arity is whatever the atom brings). An assignment sends bound names to elements of $\mathrm{Fin},n$; free names never reach evaluation because weaving rejects them. The load-bearing choice is a single shared finite universe for every binder (not a two-sorted reading by English sort). Expressions are already in negation normal form, so denial sits on the atom and there is no separate negation case.
proof idea
Not a proof: a structural recursive definition on the expression inductive type. Atom case: map the argument names through the assignment, query the model's holds predicate, then flip the bit if the denial flag is set. Conjunction case: Boolean and of the two recursive calls under the same model and environment. Quantifier case: branch on the universal flag; universal runs List.all over List.finRange n with the environment updated at the bound name, existential runs List.any the same way. Finiteness of the universe makes both quantifier clauses executable Booleans.
why it matters
This is the satisfaction engine the Loom separation story rests on. Downstream, SeparatedBy is literally inequality of the two Boolean values under a common model and environment, and that is the property a separation witness must establish (syntactic inequality is explicitly not enough). Concrete witnesses close by decide: witnessC_holds and witnessD_fails evaluate named content in a fixed witness model at the zero assignment to true and false respectively.
In framework terms this is infrastructure for the Loom domain rather than a T0–T8 forcing step: it makes "different content" a theorem about finite models so gauge-orbit separation is logically meaningful. The module's measured choice of the plainer single-sorted reading keeps most of the searched witness family intact while avoiding a stronger, weaker-witness assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.