Question entailment

[GS84] [Rob12]

The entailment order on question contents: P.Entails Q iff every alternative of P entails some alternative of Q ([Rob12] (8), after [GS84]); IsSubquestion is its inverse reading. 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 [GS84] entailment only where alternatives are complete answers (partition and polar contents; not mention-some which) — [Rob12]'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

def Question.IsSubquestion {W : Type u_1} (q parent : Question W) : Prop

q is a subquestion of parent if answering parent settles q.

Equations

• q.IsSubquestion parent = parent.Entails 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

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

theorem Question.IsSubquestion.trans {W : Type u_1} {P Q R : Question W} (hPQ : P.IsSubquestion Q) (hQR : Q.IsSubquestion R) : P.IsSubquestion 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ᶜ)