Similarity orderings

@cite{lewis-1973} @cite{stalnaker-1968}

A SimilarityOrdering W equips a type of worlds with a centered ternary relation closer w₀ w₁ w₂ ("w₁ is at least as close to w₀ as w₂ is") that is reflexive and transitive in the second/third arguments at every center. This is the order-theoretic substrate of variably-strict counterfactuals (@cite{lewis-1973} / @cite{stalnaker-1968}) and of any "closest-world" semantics — selectional, supervaluation, homogeneity, etc.

The structure lives in Core.Order (not Conditionals) because it is a general-purpose primitive: it is used directly by counterfactual operators in Theories/Semantics/Conditionals/, by alternative-sensitive operators (@cite{santorio-2018}), by causal psycholinguistic models in Theories/Semantics/Causation/, and by any future "closest match" theory.

Key operations

• closer w₀ w₁ w₂ — the relation itself (reflexive, transitive)
• closestWorlds w₀ A — minimal elements of a Finset under closer
• atCenter w₀ — coerce to a Core.Order.NormalityOrder centered at w₀
• isCentered — strong centering: w is the unique closest world to itself
• candidateSelections — the set of selection-function candidates induced by the ordering (bridge to Stalnaker selection)
• ≤[sim, w₀] notation: w₁ ≤[sim, w₀] w₂ reads "w₁ is at least as similar to w₀ as w₂ is" (@cite{lewis-1973}-style notation)

Connection to selection functions

Semantics.Conditionals.SelectionFunction and SimilarityOrdering are dual presentations of the same intuition. A coherent selection function induces a similarity ordering via the coherentSelectionToSimilarity constructor (which lives in Theories/Semantics/Conditionals/Basic.lean because it depends on selection-function machinery from Semantics.Conditionals.SelectionFunction).

Structure

structure Core.Order.SimilarityOrdering (W : Type u_1) : Type u_1

A similarity ordering on worlds: a centered ternary relation closer w₀ w₁ w₂ saying that w₁ is at least as close to w₀ as w₂ is, reflexive and transitive in w₁/w₂/w₃ at each center w₀.

• closer : W → W → W → Prop

  closer w₀ w₁ w₂ means w₁ is at least as close to w₀ as w₂ is.

• closer_refl (w₀ w : W) : w ≤[self,w₀] w

  Every world is at least as close to any center as itself.

• closer_trans (w₀ w₁ w₂ w₃ : W) : (w₁ ≤[self,w₀] w₂) → (w₂ ≤[self,w₀] w₃) → w₁ ≤[self,w₀] w₃

  Transitivity in the candidate arguments at a fixed center.

• closerDec (w₀ w₁ w₂ : W) : Decidable (w₁ ≤[self,w₀] w₂)

  The relation is decidable.

@[implicit_reducible]

instance Core.Order.instDecidableCloser {W : Type u_1} (sim : SimilarityOrdering W) (w₀ w₁ w₂ : W) : Decidable (w₁ ≤[sim,w₀] w₂)

Equations

• Core.Order.instDecidableCloser sim w₀ w₁ w₂ = sim.closerDec w₀ w₁ w₂

Constructors

def Core.Order.SimilarityOrdering.ofBool {W : Type u_1} (f : W → W → W → Bool) (hrefl : ∀ (w₀ w : W), f w₀ w w = true) (htrans : ∀ (w₀ w₁ w₂ w₃ : W), f w₀ w₁ w₂ = true → f w₀ w₂ w₃ = true → f w₀ w₁ w₃ = true) : SimilarityOrdering W

Construct a SimilarityOrdering from a Bool-valued function. Reflexivity and transitivity proofs can typically be discharged by decide on finite types.

Equations

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

def Core.Order.SimilarityOrdering.atCenter {W : Type u_1} (sim : SimilarityOrdering W) (w₀ : W) : NormalityOrder W

The NormalityOrder centered at world w₀: le w₁ w₂ iff w₁ is at least as close to w₀ as w₂ is. Bridges variably-strict semantics to the default-reasoning infrastructure (optimal, refine, respects, CR1–CR4) in Core.Order.Normality.

Equations

• sim.atCenter w₀ = { le := sim.closer w₀, le_refl := ⋯, le_trans := ⋯ }

Centering

def Core.Order.SimilarityOrdering.isCentered {W : Type u_1} (sim : SimilarityOrdering W) : Prop

A strongly centered similarity ordering: every world is strictly closest to itself. This is the centering axiom of @cite{lewis-1973} that licenses the inference from variably-strict to material truth.

Equations

• sim.isCentered = ∀ (w w' : W), w ≠ w' → (w ≤[sim,w] w') ∧ ¬w' ≤[sim,w] w

Closest worlds

def Core.Order.SimilarityOrdering.closestWorlds {W : Type u_1} [DecidableEq W] (sim : SimilarityOrdering W) (w₀ : W) (A : Finset W) : Finset W

The closest A-worlds to w₀: the minimal elements of A under the similarity preorder centered at w₀. In @cite{lewis-1973}'s notation, min_{≤_w}(A) = {w' ∈ A : ¬∃ w'' ∈ A. w'' <_w w'}.

Equations

• sim.closestWorlds w₀ A = {w' ∈ A | ∀ w'' ∈ A, (w' ≤[sim,w₀] w'') ∨ ¬w'' ≤[sim,w₀] w'}

@[simp]

theorem Core.Order.SimilarityOrdering.closestWorlds_empty {W : Type u_1} [DecidableEq W] (sim : SimilarityOrdering W) (w₀ : W) : sim.closestWorlds w₀ ∅ = ∅

theorem Core.Order.SimilarityOrdering.closestWorlds_subset {W : Type u_1} [DecidableEq W] (sim : SimilarityOrdering W) (w₀ : W) (A : Finset W) : sim.closestWorlds w₀ A ⊆ A

theorem Core.Order.SimilarityOrdering.mem_closestWorlds {W : Type u_1} [DecidableEq W] (sim : SimilarityOrdering W) (w₀ : W) (A : Finset W) (w' : W) : w' ∈ sim.closestWorlds w₀ A ↔ w' ∈ A ∧ ∀ w'' ∈ A, (w' ≤[sim,w₀] w'') ∨ ¬w'' ≤[sim,w₀] w'

theorem Core.Order.SimilarityOrdering.mem_closestWorlds_of_subset {W : Type u_1} [DecidableEq W] (sim : SimilarityOrdering W) {w₀ w : W} {A B : Finset W} (hBA : B ⊆ A) (hw : w ∈ sim.closestWorlds w₀ A) (hwB : w ∈ B) : w ∈ sim.closestWorlds w₀ B

Closest-world membership is preserved when restricting to a subset. If B ⊆ A and w is a closest A-world that lies in B, then w is also a closest B-world. (Restricting to fewer competitors can only preserve, never lose, "closest" status.)

This is the structural lemma underlying the @cite{ciardelli-zhang-champollion-2018} §1.2 argument that any minimal-change semantics inherits the switches falsification: at the actual world, the closest worlds in A̅ ∪ B̅ decompose into closest worlds in A̅ or B̅ individually.

theorem Core.Order.SimilarityOrdering.closestWorlds_nonempty {W : Type u_1} [DecidableEq W] (sim : SimilarityOrdering W) (w₀ : W) {A : Finset W} (hne : A.Nonempty) : (sim.closestWorlds w₀ A).Nonempty

Limit Assumption (closest-world existence): every non-empty Finset has a closest world under the centered preorder. Discharges the @cite{lewis-1973} "Limit Assumption" automatically on finite types — corresponds to mathlib's Finite.exists_minimal once the centered relation is exposed as a Preorder.

The proof routes through Set.Finite.exists_minimal, which gives a Minimal (· ∈ A) m. Membership in closestWorlds w₀ A is equivalent (the filter condition closer w₀ m w'' ∨ ¬ closer w₀ w'' m matches Minimal's ∀ y, y ≤ m → m ≤ y by case-splitting on closer w₀ w'' m).

Selection-function bridge primitives

These derive selection-function-flavoured notions from a similarity ordering without depending on Semantics.Conditionals.SelectionFunction itself, so they can sit in Core.Order. The full selection-function ↔ similarity duality (coherentSelectionToSimilarity) lives in Theories/Semantics/Conditionals/Basic.lean where both sides of the bridge are imported.

def Core.Order.candidateSelections {W : Type u_1} (sim : SimilarityOrdering W) (domain : Set W) (w : W) (A : Set W) : Set W

Candidate selection set: the worlds in A ∩ domain that are minimal at w under the similarity ordering. Any selection function s with s(w, A) ∈ candidateSelections sim domain w A is "legitimate" with respect to sim.

Equations

• Core.Order.candidateSelections sim domain w A = {w' : W | w' ∈ A ∩ domain ∧ ∀ w'' ∈ A ∩ domain, w' ≤[sim,w] w''}

def Core.Order.«term_≤[_,_]_» : Lean.TrailingParserDescr

Comparative-closeness notation (@cite{lewis-1973}): w₁ ≤[sim, w₀] w₂ reads "w₁ is at least as similar to w₀ as w₂ is". A direct @cite{lewis-1973}-style alias for sim.closer w₀ w₁ w₂.

Equations

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