Why this matters: a language can look logically tidy in its
own model while the inference is not valid in general. If you mix up
entails and valid_entails, you will overclaim what a
grammar proves.
Two questions
| Call | Question | Scope |
|---|---|---|
entails | Do the premises imply the conclusion here? | The one declared model |
valid_entails | Do they imply it in every model up to size N? | All non-empty finite models |
The same inference, two verdicts
In the level 3 model, only ana is a sun. So this holds:
entails(model, ["exists x (lex:sun(x))"], "lex:sun(ana)")
-> Entailment(holds=True, ...)
But the inference is not valid in general. Another model can put the only sun on a different individual. Bounded search finds it:
conlang valid \
--premise "exists x (lex:sun(x))" \
--conclusion "lex:sun(ana)" \
--max-domain 2
invalid: countermodel at domain size 2
domain: d0, d1
constants: ana=d0
lex:sun: [['d1']]
premises: [True]
The countermodel makes the premise true and the conclusion false. That is why declared-model entailment and validity are different claims.
Watch the vacuous case
entails holds when a premise is false. That is material
implication, not evidence that the conclusion is true:
entails(model, ["lex:moon(ana)"], "lex:sun(ana)")
-> holds=True because moon(ana) is false
Retrieval check
Which call uses only the declared model?
Which verdict can be “unknown”?
Which evidence shows an inference is not valid?
Do it once
- Run the
conlang validcommand above. - Read the countermodel: which individual is
ana, and which is the sun? - Now evaluate the same inference in the level 3 model with
entails. - Ask: why can both answers be correct?
Expected: the declared model has one sun at ana, so the
inference holds there. The countermodel moves the sun away, so the inference is not
valid across all models.
Primary source: the feature guide sections on model entailment and validity, plus the glossary entries for Entailment, Validity, and Countermodel.
Ask your teacher: if a formula feels obvious, ask whether it is obvious in the model or valid in every model.
Previous: Meaning is not the model. Reference: Entailment vs validity cheat sheet.