Question entailment

[groenendijk-stokhof-1984] [roberts-2012]

The entailment order on question contents: P.Entails Q iff every alternative of P entails some alternative of Q ([roberts-2012] (8), after [groenendijk-stokhof-1984]). The order coincides with the inquisitive lattice order under finiteness (entails_iff_le); the two diverge only where alt is empty.

Fidelity notes

Entails matches [groenendijk-stokhof-1984] entailment only where alternatives are complete answers (partition and polar contents; not mention-some which) — [roberts-2012]'s own caveat. Polar-question goals reduce to Set inclusions via entails_polar_polar_iff and then decide, after activating Set.decidableSubsetOfFintype (Core/Data/Fintype/Sets.lean) as a local instance.

def Question.Entails {W : Type u_1} (P Q : Question W) : Prop

Every alternative of P entails some alternative of Q.

Equations

• P.Entails Q = ∀ p ∈ P.alt, ∃ q ∈ Q.alt, p ⊆ q

Reflexivity / transitivity

theorem Question.Entails.refl {W : Type u_1} (P : Question W) : P.Entails P

theorem Question.Entails.trans {W : Type u_1} {P Q R : Question W} (hPQ : P.Entails Q) (hQR : Q.Entails R) : P.Entails R

Lattice ↔ entailment

theorem Question.entails_of_le {W : Type u_1} {P Q : Question W} (h : P ≤ Q) (hQ : Q.props.Finite) : P.Entails Q

Inquisitive entailment P ≤ Q implies P.Entails Q; finiteness supplies maximal extensions.

theorem Question.le_of_entails {W : Type u_1} {P Q : Question W} (hP : P.props.Finite) (h : P.Entails Q) : P ≤ Q

Converse of entails_of_le, under finiteness of P.props.

theorem Question.entails_iff_le {W : Type u_1} {P Q : Question W} (hP : P.props.Finite) (hQ : Q.props.Finite) : P.Entails Q ↔ P ≤ Q

Question entailment coincides with the inquisitive lattice order under finiteness.

theorem Question.entails_of_le' {W : Type u_1} {P Q : Question W} [Finite W] (h : P ≤ Q) : P.Entails Q

Variant of entails_of_le for finite world types.

Polar reduction

theorem Question.entails_polar_polar_iff {W : Type u_1} {p q : Set W} (hne_p : p ≠ ∅) (hnu_p : p ≠ Set.univ) (hne_q : q ≠ ∅) (hnu_q : q ≠ Set.univ) : (polar p).Entails (polar q) ↔ (p ⊆ q ∨ p ⊆ qᶜ) ∧ (pᶜ ⊆ q ∨ pᶜ ⊆ qᶜ)