Hamblin sets closed under conjunction or disjunction

A wh-question over atomic answers a i denotes, under Dayal's sum-closed restrictor, the closure of the atoms under conjunction, infClosure (Set.range a), the conjunctions over nonempty groups of atoms; under Spector's higher-order quantification, pruned to disjunctions of atoms as in Fox, it denotes their closure under disjunction, supClosure (Set.range a). Both families are read off the atoms true at a world, Preorder.satisfied with the atoms as criteria, and both induce the same partition, the kernel of that map.

References

• [Day96]
• [Spe08]
• [Fox07]
• [Fox18]

@[simp]

theorem Question.mem_satisfied_iff {W : Type u_1} {ι : Type u_2} {a : ι → Set W} {w : W} {i : ι} : i ∈ Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ w ↔ w ∈ a i

An atom is among those true at a world iff it is true there.

theorem Question.mem_biInter_iff_subset {W : Type u_1} {ι : Type u_2} {a : ι → Set W} {S : Finset ι} {w : W} : w ∈ ⋂ i ∈ S, a i ↔ ↑S ⊆ Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ w

A world verifies the conjunction of a group iff the group's atoms are true there.

theorem Question.partition_infClosure_range {W : Type u_1} {ι : Type u_2} {a : ι → Set W} : partition (infClosure (Set.range a)) = Setoid.ker (Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ)

Under conjunctive closure, two worlds are in the same cell iff the same atoms are true at them.

theorem Question.partition_supClosure_range {W : Type u_1} {ι : Type u_2} {a : ι → Set W} : partition (supClosure (Set.range a)) = Setoid.ker (Preorder.satisfied (fun (v : W) (i : ι) => v ∈ a i) Set.univ)

Under disjunctive closure, two worlds are in the same cell iff the same atoms are true at them.

theorem Question.partition_infClosure_range_eq_supClosure_range {W : Type u_1} {ι : Type u_2} {a : ι → Set W} : partition (infClosure (Set.range a)) = partition (supClosure (Set.range a))

Both closures induce the same partition.