Partition questions

This file defines the basic vocabulary of partition questions. A question in the sense of [GS84] is a Setoid W, its answers the cells; the same object is a subject matter in the sense of [Lew88], and a proposition is entirely about it when the question decides it, that is, when it is constant on the cells. The polar question whether p is the kernel of the indicator of p, a question decides p exactly when it refines the polar question, Q ≤ polar p, and the question raised by a family of propositions is the meet of their polar questions, so a finer question decides more (le_trans), the finest question decides everything (bot_le), and a family's question decides each member (iInf₂_le). A question settles the value of a function exactly when it decides each of its fibres (le_ker_iff_forall_decides). Every question is the meet of the polar questions of its cells (iInf_polar_cell), and the nontrivial polar questions are the coatoms of the lattice of questions (isCoatom_iff). A proposition a question decides is [Car13]'s visible, [PB25]'s considered, and an issue in a subject matter for [vFG10]; the converse relation, a proposition settling a question, is Question.Resolves.

Main definitions

• Setoid.cell Q w — the cell of w, an element of Q.classes.
• Setoid.polar p — the polar question whether p.
• Setoid.Decides Q p — Q decides p: p is a union of cells.
• Setoid.ofProps ps — the question raised by a finite family of propositions.

References

• [GS84]
• [Lew88]
• [vFG10]
• [Car13]
• [PB25]

Cells

def Setoid.cell {W : Type u_1} (Q : Setoid W) (w : W) : Set W

The cell of w is the set of worlds equivalent to it.

Equations

• Q.cell w = {v : W | Q v w}

@[simp]

theorem Setoid.mem_cell {W : Type u_1} {Q : Setoid W} {w v : W} : v ∈ Q.cell w ↔ Q v w

theorem Setoid.cell_mem_classes {W : Type u_1} {Q : Setoid W} (w : W) : Q.cell w ∈ Q.classes

theorem Setoid.mem_cell_self {W : Type u_1} {Q : Setoid W} (w : W) : w ∈ Q.cell w

theorem Setoid.cell_nonempty {W : Type u_1} {Q : Setoid W} (w : W) : (Q.cell w).Nonempty

theorem Setoid.cell_eq_of_rel {W : Type u_1} {Q : Setoid W} {w v : W} (h : Q w v) : Q.cell w = Q.cell v

theorem Setoid.cell_eq_or_disjoint {W : Type u_1} (Q : Setoid W) (w v : W) : Q.cell w = Q.cell v ∨ Disjoint (Q.cell w) (Q.cell v)

Two cells are equal or disjoint.

@[simp]

theorem Setoid.cell_bot {W : Type u_1} (w : W) : ⊥.cell w = {w}

theorem Setoid.cell_inf {W : Type u_1} {Q : Setoid W} (Q' : Setoid W) (w : W) : (Q ⊓ Q').cell w = Q.cell w ∩ Q'.cell w

@[instance_reducible]

instance Setoid.instDecidableRelROfDecidableEq_linglib {W : Type u_1} [DecidableEq W] : DecidableRel ⇑⊥

Equations

• Setoid.instDecidableRelROfDecidableEq_linglib v w = decidable_of_iff (v = w) ⋯

@[instance_reducible]

instance Setoid.instDecidableRelR_linglib {W : Type u_1} : DecidableRel ⇑⊤

Equations

• Setoid.instDecidableRelR_linglib x✝¹ x✝ = isTrue trivial

@[instance_reducible]

instance Setoid.instDecidableMemSetCellOfDecidableRelR {W : Type u_1} {Q : Setoid W} {w v : W} [DecidableRel ⇑Q] : Decidable (v ∈ Q.cell w)

Equations

• Setoid.instDecidableMemSetCellOfDecidableRelR = Setoid.instDecidableMemSetCellOfDecidableRelR._aux_1

@[instance_reducible]

instance Setoid.instDecidableLeSetCellOfFintypeOfDecidableRelROfDecidablePredMem {W : Type u_1} {Q : Setoid W} {p : Set W} {w : W} [Fintype W] [DecidableRel ⇑Q] [DecidablePred fun (x : W) => x ∈ p] : Decidable (Q.cell w ⊆ p)

Equations

• Setoid.instDecidableLeSetCellOfFintypeOfDecidableRelROfDecidablePredMem = { decide := decide (∀ a ∈ Finset.univ, (fun (v : W) => Q v w → v ∈ p) a), reflects_decide := ⋯ }

Polar questions and decided propositions

def Setoid.polar {W : Type u_1} (p : Set W) : Setoid W

The polar question whether p is the kernel of its indicator.

Equations

• Setoid.polar p = Setoid.ker fun (x : W) => x ∈ p

theorem Setoid.polar_iff {W : Type u_1} {p : Set W} {w v : W} : (polar p) w v ↔ (w ∈ p ↔ v ∈ p)

theorem Setoid.polar_cell_of_mem {W : Type u_1} {p : Set W} {w : W} (hw : w ∈ p) : (polar p).cell w = p

theorem Setoid.polar_cell_of_notMem {W : Type u_1} {p : Set W} {w : W} (hw : w ∉ p) : (polar p).cell w = pᶜ

@[simp]

theorem Setoid.polar_compl {W : Type u_1} {p : Set W} : polar pᶜ = polar p

@[instance_reducible]

instance Setoid.instDecidableRelROfDecidablePredMemSet_linglib {W : Type u_1} {p : Set W} [DecidablePred fun (x : W) => x ∈ p] : DecidableRel ⇑(polar p)

Equations

• Setoid.instDecidableRelROfDecidablePredMemSet_linglib x✝¹ x✝ = decidable_of_iff (x✝¹ ∈ p ↔ x✝ ∈ p) ⋯

def Setoid.Decides {W : Type u_1} (Q : Setoid W) (p : Set W) : Prop

A question decides p when it refines the polar question whether p, so that p is constant on its cells and a union of them.

Equations

• Q.Decides p = (Q ≤ Setoid.polar p)

theorem Setoid.decides_iff {W : Type u_1} {Q : Setoid W} {p : Set W} : Q.Decides p ↔ ∀ (w v : W), Q w v → (w ∈ p ↔ v ∈ p)

theorem Setoid.Decides.iff {W : Type u_1} {Q : Setoid W} {p : Set W} {w v : W} (h : Q.Decides p) (hwv : Q w v) : w ∈ p ↔ v ∈ p

Equivalent worlds agree on a decided proposition.

theorem Setoid.decides_iff_forall_cell {W : Type u_1} {Q : Setoid W} {p : Set W} : Q.Decides p ↔ ∀ (w : W), Q.cell w ⊆ p ∨ ∀ v ∈ Q.cell w, v ∉ p

Q decides p iff each cell entails p or entails its negation.

@[instance_reducible]

instance Setoid.instDecidableDecidesOfFintypeOfDecidableRelROfDecidablePredMemSet {W : Type u_1} {Q : Setoid W} {p : Set W} [Fintype W] [DecidableRel ⇑Q] [DecidablePred fun (x : W) => x ∈ p] : Decidable (Q.Decides p)

Equations

• Setoid.instDecidableDecidesOfFintypeOfDecidableRelROfDecidablePredMemSet = decidable_of_iff (∀ (w v : W), Q w v → (w ∈ p ↔ v ∈ p)) ⋯

theorem Setoid.Decides.mono {W : Type u_1} {Q : Setoid W} {p : Set W} {Q' : Setoid W} (hQ : Q' ≤ Q) (h : Q.Decides p) : Q'.Decides p

A finer question decides whatever a coarser one does.

theorem Setoid.bot_decides {W : Type u_1} {p : Set W} : ⊥.Decides p

The finest question decides every proposition.

theorem Setoid.polar_decides {W : Type u_1} {p : Set W} : (polar p).Decides p

The polar question whether p decides p.

theorem Setoid.top_decides_iff {W : Type u_1} {p : Set W} : ⊤.Decides p ↔ ∀ (w v : W), w ∈ p ↔ v ∈ p

The coarsest question decides only the trivial propositions.

theorem Setoid.decides_compl_iff {W : Type u_1} {Q : Setoid W} {p : Set W} : Q.Decides pᶜ ↔ Q.Decides p

theorem Setoid.Decides.compl {W : Type u_1} {Q : Setoid W} {p : Set W} (h : Q.Decides p) : Q.Decides pᶜ

theorem Setoid.Decides.inter {W : Type u_1} {Q : Setoid W} {p q : Set W} (hp : Q.Decides p) (hq : Q.Decides q) : Q.Decides (p ∩ q)

theorem Setoid.Decides.union {W : Type u_1} {Q : Setoid W} {p q : Set W} (hp : Q.Decides p) (hq : Q.Decides q) : Q.Decides (p ∪ q)

theorem Setoid.decides_cell {W : Type u_1} {Q : Setoid W} (w : W) : Q.Decides (Q.cell w)

A question decides each of its cells.

theorem Setoid.Decides.cell_subset {W : Type u_1} {Q : Setoid W} {p : Set W} {w : W} (h : Q.Decides p) (hw : w ∈ p) : Q.cell w ⊆ p

A cell of a question deciding p that meets p entails it.

theorem Setoid.le_ker_iff_forall_decides {W : Type u_1} {Q : Setoid W} {β : Type u_2} {f : W → β} : Q ≤ ker f ↔ ∀ (b : β), Q.Decides (f ⁻¹' {b})

A question settles the value of f, refining its kernel, exactly when it decides each fibre of f.

Polar questions as coatoms

theorem Setoid.iInf_polar_cell {W : Type u_1} (Q : Setoid W) : ⨅ (w : W), polar (Q.cell w) = Q

A question is the meet of the polar questions of its cells.

theorem Setoid.polar_ne_top {W : Type u_1} {p : Set W} (hp : p.Nonempty) (hp' : p ≠ Set.univ) : polar p ≠ ⊤

theorem Setoid.isCoatom_polar {W : Type u_1} {p : Set W} (hp : p.Nonempty) (hp' : p ≠ Set.univ) : IsCoatom (polar p)

A polar question whether p, for p neither empty nor everything, is a coatom, since a coarser question relates a p-world a to a world outside p, and so relates every world to a.

theorem Setoid.isCoatom_iff {W : Type u_1} {Q : Setoid W} : IsCoatom Q ↔ ∃ (p : Set W), p.Nonempty ∧ p ≠ Set.univ ∧ Q = polar p

The coatoms of the lattice of questions are exactly the polar questions whether p, for p neither empty nor everything.

The question raised by a family of propositions

def Setoid.ofProps {W : Type u_1} (ps : Finset (Finset W)) : Setoid W

The question raised by a family of propositions is the meet of their polar questions, the coarsest question deciding each of them.

Equations

• Setoid.ofProps ps = ⨅ p ∈ ps, Setoid.polar ↑p

theorem Setoid.ofProps_iff {W : Type u_1} {w v : W} (ps : Finset (Finset W)) : (ofProps ps) w v ↔ ∀ p ∈ ps, w ∈ p ↔ v ∈ p

@[instance_reducible]

instance Setoid.instDecidableRelROfDecidableEq_linglib_1 {W : Type u_1} (ps : Finset (Finset W)) [DecidableEq W] : DecidableRel ⇑(ofProps ps)

Equations

• Setoid.instDecidableRelROfDecidableEq_linglib_1 ps x✝¹ x✝ = decidable_of_iff (∀ p ∈ ps, x✝¹ ∈ p ↔ x✝ ∈ p) ⋯

theorem Setoid.ofProps_decides {W : Type u_1} (ps : Finset (Finset W)) {p : Finset W} (hp : p ∈ ps) : (ofProps ps).Decides ↑p

The question raised by a family decides each of its members.

theorem Setoid.le_ofProps_iff {W : Type u_1} {Q : Setoid W} (ps : Finset (Finset W)) : Q ≤ ofProps ps ↔ ∀ p ∈ ps, Q.Decides ↑p

The question raised by a family is the coarsest question deciding all of its members.