Why this matters: the meaning layer tells you what a clause means; the semantic model tells you which worlds make it true. Confusing the two makes a generated language look broken when it is only under-specified.
Two different layers
| Layer | What it holds | What it answers |
|---|---|---|
## Meaning | Lambda denotations and composed truth conditions | What does this clause mean? |
## Model | A domain plus predicate extensions | Is it true in this interpretation? |
Every generated language has a ## Meaning section. Only a Spec with
semantics gives the ## Model section something to show;
otherwise it says “No model.”
Level 3, concretely
The rich Spec declared this interpretation:
Domain: ana, bo
lex:sun: ana
lex:moon: bo
lex:see: ana, boRead each line as an extension: lex:sun holds of ana,
lex:moon holds of bo, and lex:see holds of
the pair ana, bo. So:
| Formula | Truth value | Why |
|---|---|---|
lex:sun(ana) | true | ana is in the extension |
lex:sun(bo) | false | bo is not |
lex:moon(bo) | true | bo is in the extension |
forall x (lex:moon(x) -> lex:sun(x)) | false | bo is a moon but not a sun |
Retrieval check
Which formula is true?
Which function checks all finite models?
Which run declares a model?
Do it once
- Open
out/language-levels/level-3-rich.md. - Read the
## Modelsection. - Predict whether
lex:see(ana, bo)is true before checking. - Now ask what would change if the extension were empty.
Expected: it is true. An empty extension would make it false and
would make the universal moon–sun formula true vacuously over moon.
Primary source: the feature guide sections on meaning and the model, plus the glossary entries for Meaning, Semantic model, and Validity.
Ask your teacher: if a formula is true in the model but you expected otherwise, ask which extension makes it true.
Previous: Read the grammar sketch. Reference: Meaning and model cheat sheet.