Reference: Meaning, model, validity

Layer	Question	Tool
Meaning	What does this clause mean?	`lexeme_meaning`, `build_meaning`, relative/complement builders
Model	Is it true in this interpretation?	`evaluate`, `entails`
Validity	Is it true in every model up to size N?	`valid`, `valid_entails`

Declared model (level 3)

Domain: ana, bo

lex:sun:  ana
lex:moon: bo
lex:see:  ana, bo

Formula	Value	Reason
`lex:sun(ana)`	true	`ana` is in `lex:sun`
`lex:sun(bo)`	false	`bo` is not
`lex:moon(bo)`	true	`bo` is in `lex:moon`
`lex:see(ana, bo)`	true	the pair is in `lex:see`
`forall x (lex:moon(x) -> lex:sun(x))`	false	`moon(bo)` is true, `sun(bo)` is false

Entailment vs validity

Call	Scope	Can return
`entails(model, premises, conclusion)`	The one declared model	`Entailment`
`valid(formula, max_domain=3)`	All non-empty models up to size 3	`valid`, `invalid`, `unknown`
`valid_entails(premises, conclusion, max_domain=3)`	All non-empty models up to size 3	`valid`, `invalid`, `unknown`

Do not confuse them. evaluate and entails never search other models. valid and valid_entails ignore the declared model and can return unknown when the model budget runs out.

Where the sections come from

## Meaning is derived from lexemes, place structure, and composition — every language has one.
## Model is derived from Language.semantic_model; with no domain it says “No model.”
## Model truth values and entailment are derived at render time, never stored.

Primary source: feature guide, Spec reference, and the glossary.

Lessons: Meaning is not the model · Entailment is not validity.