Reference: Entailment vs validity

Call	Scope	Result
`entails(model, premises, conclusion)`	One declared interpretation	`Entailment(holds, premise_values, conclusion)`
`valid_entails(premises, conclusion, max_domain=3)`	Every non-empty model, sizes 1..N	`Validity(status, max_domain, models_checked, countermodel)`
`evaluate(model, formula)`	One formula in one declared interpretation	`bool`
`valid(formula, max_domain=3)`	Every non-empty model, sizes 1..N	`Validity`

Declared model (level 3)

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

Same inference, two answers

# Declared model: holds, because ana is the only sun.
entails(model, ["exists x (lex:sun(x))"], "lex:sun(ana)")
-> holds=True

# All models up to size 2: invalid, because the sun can be elsewhere.
valid_entails(["exists x (lex:sun(x))"], "lex:sun(ana)", max_domain=2)
-> countermodel: domain d0,d1; ana=d0; lex:sun={d1}

Vacuous truth: entails returns holds=True when a premise is false, because material implication is true. That is not evidence for the conclusion. Check premise_values before reading a verdict.

What the verdicts mean

Status	Meaning
`valid`	No countermodel exists up to the domain bound and the budget was not exhausted.
`invalid`	A countermodel exists; the `Countermodel` records domain, extensions, constants, and premise values.
`unknown`	The model budget ran out before the search finished. Never read this as valid.

CLI

conlang valid --premise "exists x (lex:sun(x))" \
  --conclusion "lex:sun(ana)" --max-domain 2

Exit codes: 0 valid, 1 invalid or unknown, 2 usage or parse error.

Primary source: feature guide and glossary.

Lesson: Entailment is not validity.