Selection functions

This file defines selection functions and the selection conditional. A selection function takes a world and a possible proposition to a world at which the proposition holds, the world itself when it holds there: intuitively the closest world at which the proposition holds. The selection conditional if p, q is true when q holds at the world selected for p, and vacuously true when p is impossible. A similarity ordering with ties corresponds to the class of selection functions its completions determine, and for a single conditional the supervaluation over them is the conditional of the closest worlds.

Main definitions

• SelectionFunction: a selection function.
• selectionConditional: the selection conditional.
• SelectionFunction.IsCSO: Stalnaker's condition (4), that antecedents each true at the world selected for the other select the same world.
• SelectionFunction.restrict: a selection function restricted to a set of worlds.
• SelectionFunction.along, SelectionFunction.modal: selection along an accessibility relation and the selectional modal it defines.
• Completion: a linear extension of a family of preorders at each center.
• SelectionFunction.Compatible: selection by a completion of a family of preorders.

Main results

• SelectionFunction.exists_sel_eq: outside a proposition any of its worlds can be selected.
• SelectionFunction.modal_eq_core, SelectionFunction.modal_inter_refl, SelectionFunction.modal_eq_id: the selectional modal along a relation is necessity along a function, idle where the relation is reflexive and the identity along a reflexive relation.
• SelectionFunction.Compatible.isCSO: selection by a completion satisfies condition (4).
• mem_closestImp_iff_forall_compatible: the conditional of the closest worlds is the supervaluation over completions.

References

• R. C. Stalnaker, A Theory of Conditionals (1968)
• R. C. Stalnaker, Indicative conditionals (1975)
• R. C. Stalnaker, A Defense of Conditional Excluded Middle (1981)

structure Conditional.SelectionFunction (W : Type u_1) : Type u_1

A selection function ([Sta68]) takes a world and a proposition to a selected world, one at which the proposition holds when it is possible, and the world itself when the proposition holds there.

• sel : W → Set W → W

  The selection map.

• inclusion (w : W) (A : Set W) : A.Nonempty → self.sel w A ∈ A

  The world selected for a possible proposition is one at which it holds.

• centering (w : W) (A : Set W) : w ∈ A → self.sel w A = w

  A world at which the proposition holds selects itself.

theorem Conditional.SelectionFunction.exists_sel_eq {W : Type u_1} {w v : W} {A : Set W} (hv : v ∈ A) (hw : w ∉ A) : ∃ (s : SelectionFunction W), s.sel w A = v

Inclusion and centering are the only constraints on a selection function, so at a world outside a proposition any world of the proposition is selected by some selection function.

def Conditional.SelectionFunction.domain {W : Type u_1} (s : SelectionFunction W) (w : W) (p : Set W) : Set W

The domain of the selection conditional, the world selected for p when p is possible and nothing otherwise. [Sta68] selects the absurd world, at which every sentence is true, exactly for an impossible antecedent (conditions (1) and (2)), so the conditional is vacuously true there. With every world possible relative to every other, an antecedent is impossible when it is empty.

Equations

• s.domain w p = {s.sel w p} ∩ p

theorem Conditional.SelectionFunction.domain_eq_singleton {W : Type u_1} (s : SelectionFunction W) {p : Set W} {w : W} (hp : p.Nonempty) : s.domain w p = {s.sel w p}

theorem Conditional.SelectionFunction.subsingleton_domain {W : Type u_1} (s : SelectionFunction W) {p : Set W} {w : W} : (s.domain w p).Subsingleton

theorem Conditional.SelectionFunction.domain_of_mem {W : Type u_1} (s : SelectionFunction W) {p : Set W} {w : W} (hw : w ∈ p) : s.domain w p = {w}

def Conditional.selectionConditional {W : Type u_1} (s : SelectionFunction W) (p q : Set W) : Set W

The selection conditional of [Sta68], true at w when q holds at the world s selects for p and vacuously true when p is impossible. The indicative reading of [Sta75] and the counterfactual reading of [Sta81] share this clause and differ in which selection functions are admissible.

Equations

• Conditional.selectionConditional s p q = Conditional.ofDomain s.domain p q

theorem Conditional.mem_selectionConditional {W : Type u_1} (s : SelectionFunction W) {p q : Set W} {w : W} : w ∈ selectionConditional s p q ↔ p.Nonempty → s.sel w p ∈ q

theorem Conditional.mem_selectionConditional_of_nonempty {W : Type u_1} (s : SelectionFunction W) {p q : Set W} {w : W} (hp : p.Nonempty) : w ∈ selectionConditional s p q ↔ s.sel w p ∈ q

theorem Conditional.mem_selectionConditional_of_mem {W : Type u_1} (s : SelectionFunction W) {p q : Set W} {w : W} (hw : w ∈ p) : w ∈ selectionConditional s p q ↔ w ∈ q

At an antecedent-world the selection conditional reduces to its consequent, by centering.

theorem Conditional.selectionConditional_inter_self {W : Type u_1} (s : SelectionFunction W) {p q : Set W} : selectionConditional s p q ∩ p = q ∩ p

theorem Conditional.selectionConditional_cem {W : Type u_1} (s : SelectionFunction W) {p q : Set W} {w : W} : w ∈ selectionConditional s p q ∨ w ∈ selectionConditional s p qᶜ

The selection conditional satisfies Conditional Excluded Middle, since a single selected world settles every consequent.

theorem Conditional.selectionConditional_or {W : Type u_1} (s : SelectionFunction W) {p q r : Set W} {w : W} (h : w ∈ selectionConditional s p (q ∪ r)) : w ∈ selectionConditional s p q ∨ w ∈ selectionConditional s p r

The selection conditional distributes over a disjunctive consequent.

theorem Conditional.selectionConditional_subset_materialImp {W : Type u_1} (s : SelectionFunction W) {p q : Set W} : selectionConditional s p q ⊆ materialImp p q

The selection conditional entails the material conditional, since by centering an antecedent-world selects itself.

Selection along a relation

A selection function selects along an accessibility relation by selecting from the successors of a world, and the selectional modal along the relation is necessity along the graph of this selection: the preimage of a function, so a complete lattice homomorphism. Selection is idle at the worlds that access themselves.

def Conditional.SelectionFunction.along {W : Type u_1} (s : SelectionFunction W) (R : SetRel W W) (w : W) : W

The world selected along R at w, from the R-successors of w.

Equations

• s.along R w = s.sel w {v : W | (w, v) ∈ R}

def Conditional.SelectionFunction.modal {W : Type u_1} (s : SelectionFunction W) (R : SetRel W W) : CompleteLatticeHom (Set W) (Set W)

The selectional modal along R, sending A to the worlds whose selection along R is an A-world.

Equations

• s.modal R = CompleteLatticeHom.setPreimage (s.along R)

@[simp]

theorem Conditional.SelectionFunction.mem_modal {W : Type u_1} {s : SelectionFunction W} {R : SetRel W W} {A : Set W} {w : W} : w ∈ (s.modal R) A ↔ s.along R w ∈ A

theorem Conditional.SelectionFunction.modal_eq_core {W : Type u_1} {s : SelectionFunction W} {R : SetRel W W} (A : Set W) : (s.modal R) A = (Function.graph (s.along R)).core A

The selectional modal is necessity along the graph of the selection.

theorem Conditional.SelectionFunction.along_eq_self {W : Type u_1} {s : SelectionFunction W} {R : SetRel W W} {w : W} (h : (w, w) ∈ R) : s.along R w = w

A world that accesses itself selects itself.

theorem Conditional.SelectionFunction.rel_along {W : Type u_1} {s : SelectionFunction W} {R : SetRel W W} {w : W} (h : ∃ (v : W), (w, v) ∈ R) : (w, s.along R w) ∈ R

A world with a successor selects one of its successors.

theorem Conditional.SelectionFunction.modal_inter_refl {W : Type u_1} {s : SelectionFunction W} {R : SetRel W W} (A : Set W) : (s.modal R) A ∩ {w : W | (w, w) ∈ R} = A ∩ {w : W | (w, w) ∈ R}

At the worlds that access themselves, the selectional modal of A holds where A does.

theorem Conditional.SelectionFunction.modal_eq_id {W : Type u_1} {s : SelectionFunction W} {R : SetRel W W} [R.IsRefl] : s.modal R = CompleteLatticeHom.id (Set W)

Along a reflexive relation selection is idle, so the selectional modal is the identity.

theorem Conditional.selectionConditional_eq_modal {W : Type u_1} {s : SelectionFunction W} {p : Set W} (hp : p.Nonempty) (q : Set W) : selectionConditional s p q = (s.modal (SetRel.ofSuccessors fun (x : W) => p)) q

On a possible antecedent, the selection conditional is the selectional modal along the constant relation to the antecedent-worlds.

Condition (4) and restriction

def Conditional.SelectionFunction.IsCSO {W : Type u_1} (s : SelectionFunction W) : Prop

A selection function satisfies [Sta68]'s condition (4) when two possible antecedents each true at the world selected for the other select the same world.

Equations

• s.IsCSO = ∀ (w : W) (p p' : Set W), p.Nonempty → p'.Nonempty → s.sel w p' ∈ p → s.sel w p ∈ p' → s.sel w p = s.sel w p'

theorem Conditional.SelectionFunction.IsCSO.sel_mem_iff {W : Type u_1} {s : SelectionFunction W} {w : W} {p q : Set W} (hs : s.IsCSO) (h : (p ∩ q).Nonempty) : s.sel w p ∈ q ↔ s.sel w p = s.sel w (p ∩ q)

Under condition (4), the world selected for p lies in q iff it is the world selected for p ∩ q.

noncomputable def Conditional.SelectionFunction.restrict {W : Type u_1} (s : SelectionFunction W) (C : Set W) : SelectionFunction W

The restriction of a selection function to a set C, which at a world of C selects among the antecedent-worlds in C when there are any and otherwise selects as before.

Equations

• s.restrict C = { sel := fun (w : W) (A : Set W) => if w ∈ C ∧ (A ∩ C).Nonempty then s.sel w (A ∩ C) else s.sel w A, inclusion := ⋯, centering := ⋯ }

theorem Conditional.SelectionFunction.restrict_sel_of_mem {W : Type u_1} {w : W} (s : SelectionFunction W) (C : Set W) {A : Set W} (hw : w ∈ C) (hA : (A ∩ C).Nonempty) : (s.restrict C).sel w A = s.sel w (A ∩ C)

theorem Conditional.SelectionFunction.restrict_sel_of_not_nonempty {W : Type u_1} {w : W} (s : SelectionFunction W) (C : Set W) {A : Set W} (hA : ¬(A ∩ C).Nonempty) : (s.restrict C).sel w A = s.sel w A

Selection functions compatible with a similarity ordering

[Sta81] reads a similarity ordering with ties and incomparabilities as the class of its completions, the well orderings of the worlds that extend it, and a conditional as true when it is true on every completion.

structure Conditional.Completion {W : Type u_1} (ord : W → Preorder W) : Type u_1

A completion of a family of preorders assigns to each center a linear order of the worlds extending its strict order.

• order : W → LinearOrder W

  The completed order at each center.

• le_of_lt (w x y : W) : x < y → x ≤ y

def Conditional.SelectionFunction.SelectedBy {W : Type u_1} {ord : W → Preorder W} (s : SelectionFunction W) (c : Completion ord) : Prop

A selection function is selected by a completion when it selects, for each center, the least possible antecedent-world in the completion's order.

Equations

• s.SelectedBy c = ∀ (w : W) (p : Set W), p.Nonempty → ∀ u ∈ p, s.sel w p ≤ u

def Conditional.SelectionFunction.Compatible {W : Type u_1} (s : SelectionFunction W) (ord : W → Preorder W) : Prop

A selection function is compatible with a family of preorders when some completion of the family selects it.

Equations

• s.Compatible ord = ∃ (c : Conditional.Completion ord), s.SelectedBy c

theorem Conditional.SelectionFunction.Compatible.isCSO {W : Type u_1} {ord : W → Preorder W} {s : SelectionFunction W} (hs : s.Compatible ord) : s.IsCSO

A selection function selected by a completion satisfies [Sta68]'s condition (4).

theorem Conditional.SelectionFunction.Compatible.sel_mem_minimals {W : Type u_1} {ord : W → Preorder W} {s : SelectionFunction W} {p : Set W} {w : W} (hs : s.Compatible ord) (hp : p.Nonempty) : s.sel w p ∈ (ord w).minimals p

A compatible selection function selects a closest antecedent-world.

theorem Conditional.SelectionFunction.Compatible.domain_subset {W : Type u_1} {ord : W → Preorder W} {s : SelectionFunction W} {p : Set W} {w : W} (hs : s.Compatible ord) : s.domain w p ⊆ (ord w).minimals p

theorem Conditional.SelectionFunction.Compatible.closestImp_subset {W : Type u_1} {ord : W → Preorder W} {s : SelectionFunction W} {p q : Set W} (hs : s.Compatible ord) : closestImp ord p q ⊆ selectionConditional s p q

Every compatible selection function makes true what the closest worlds make true.

theorem Conditional.exists_completion {W : Type u_1} {ord : W → Preorder W} {p : Set W} {w v : W} (hv : v ∈ (ord w).minimals p) : ∃ (c : Completion ord), ∀ u ∈ p, v ≤ u

Any closest antecedent-world comes first among the antecedent-worlds in some completion. At its center the completion orders the worlds strictly closer than it, then it, then the rest, and within each group as a linear extension of the strict order; elsewhere it is a linear extension of the strict order.

theorem Conditional.SelectionFunction.exists_compatible {W : Type u_1} {ord : W → Preorder W} {p : Set W} {w v : W} [Finite W] (hc : IsCentered ord) (hv : v ∈ (ord w).minimals p) : ∃ (s : SelectionFunction W), s.Compatible ord ∧ s.sel w p = v

On a finite, strongly centered family of preorders, any closest antecedent-world is selected by some compatible selection function.

theorem Conditional.mem_closestImp_iff_forall_compatible {W : Type u_1} {ord : W → Preorder W} {p q : Set W} {w : W} [Finite W] (hc : IsCentered ord) : w ∈ closestImp ord p q ↔ ∀ (s : SelectionFunction W), s.Compatible ord → w ∈ selectionConditional s p q

On a finite, strongly centered family of preorders, the conditional of the closest worlds holds iff the selection conditional is true on every completion, [Sta81]'s supervaluation for a single conditional.