Selection Functions

[Sta68]

A selection function in the sense of [Sta68]: given a world w and a non-empty proposition A ⊆ W, return a unique "selected" world s w A ∈ A — intuitively, the closest A-world to w.

Selection functions are characterized by two axioms:

• Inclusion: s w A ∈ A whenever A is non-empty (the selected world satisfies the input proposition).
• Centering: if w ∈ A, then s w A = w (when w itself is in A, the closest A-world is w itself).

These two axioms suffice for many semantic applications: [Sta68] conditionals, [CS18]'s selectional semantics for will, and Schulz's choice-function conditionals all rely on selection functions of this form.

Behavior on empty A is left unspecified: the axioms are vacuous there, and concrete instances may pick any default.

structure Semantics.Conditionals.SelectionFunction (W : Type u_1) : Type u_1

A selection function on W: maps a world and a proposition to a "selected" world, satisfying [Sta68]'s Inclusion and Centering axioms.

• sel : W → Set W → W

  The selection map.

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

  Inclusion: if A is non-empty, the selected world is in A.

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

  Centering: if w ∈ A, then sel w A = w.

theorem Semantics.Conditionals.SelectionFunction.sel_singleton {W : Type u_1} (s : SelectionFunction W) (w : W) : s.sel w {w} = w

Centering specialized to a singleton: sel w {w} = w.

theorem Semantics.Conditionals.SelectionFunction.sel_mem {W : Type u_1} (s : SelectionFunction W) (w : W) (A : Set W) (hA : A.Nonempty) : s.sel w A ∈ A

The selected world satisfies the input proposition (Inclusion).

theorem Semantics.Conditionals.SelectionFunction.sel_em {W : Type u_1} (s : SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) : A (s.sel w f) ∨ ¬A (s.sel w f)

Selection Excluded Middle — the structural origin of [Sta68]'s Conditional Excluded Middle and [CS18]'s Will Excluded Middle. Because sel w f is a single world, every predicate evaluated there satisfies excluded middle. The selection function reduces a quantificational question over a set to a propositional question at one point.

theorem Semantics.Conditionals.SelectionFunction.sel_neg_swap {W : Type u_1} (s : SelectionFunction W) (A : W → Prop) (f : Set W) (w : W) : (fun (w' : W) => ¬A w') (s.sel w f) ↔ ¬A (s.sel w f)

Selection Negation Swap — negation commutes through evaluation at the selected world: applying a pointwise-negated predicate to sel w f is the same as negating the application. This is the structural origin of [CS18]'s Negation Swap for will. The equivalence is Iff.rfl once the prejacent has been reduced to a propositional question at the selected point.

def Semantics.Conditionals.selectionConditional {W : Type u_1} (s : SelectionFunction W) (p q : W → Prop) : W → Prop

Selection conditional [Sta68]: "if p, q" is true at w iff q holds at the world s selects from the p-worlds. This is the bare selection-conditional clause of the selection-function framework. The indicative refinement ([Sta75], via a pragmatic constraint on s) and the counterfactual reading ([Sta81]/[Lew73b], via a similarity-induced s) share this single clause and differ only in which selection functions are admissible — so both Stalnaker.moodedConditional and Counterfactual.stalnakerCounterfactual specialize it here rather than re-stating the truth-condition.

Equations

• Semantics.Conditionals.selectionConditional s p q w = q (s.sel w {w' : W | p w'})

@[implicit_reducible]

instance Semantics.Conditionals.selectionConditional_decidable {W : Type u_1} (s : SelectionFunction W) (p q : W → Prop) [DecidablePred q] (w : W) : Decidable (selectionConditional s p q w)

selectionConditional is decidable when its consequent is. The single decidability instance the indicative and counterfactual readings inherit.

Equations

• Semantics.Conditionals.selectionConditional_decidable s p q w = Semantics.Conditionals.selectionConditional_decidable._aux_1 s p q w

def Semantics.Conditionals.selectionPrefers {W : Type u_1} (s : SelectionFunction W) (w₀ w₁ w₂ : W) : Prop

Pairwise preference induced by a selection function.

w₁ is preferred to w₂ from center w₀ iff when choosing between just the two of them, the selection function picks w₁.

Equations

• Semantics.Conditionals.selectionPrefers s w₀ w₁ w₂ = (s.sel w₀ {w₁, w₂} = w₁)

def Semantics.Conditionals.SelectionFunction.isCoherent {W : Type u_1} (s : SelectionFunction W) : Prop

A selection function is coherent iff its induced pairwise preference is transitive. This is the content of [Sta81]'s claim that selection functions determine a well-ordering of possible worlds.

Not all selection functions satisfying inclusion + centering are coherent — coherence is an additional rationality constraint.

Equations

• One or more equations did not get rendered due to their size.