Similarity orderings

A SimilarityOrdering W is a family of comparative-similarity preorders on worlds, one for each center: closer w₀ w₁ w₂ says that w₁ is at least as similar to w₀ as w₂ is ([Lew73b], [Sta68]). Each closer w₀ is reflexive and transitive (Std.Refl, IsTrans instances) and decidable. closest w₀ s is the set of s-worlds maximally similar to w₀ — the minimal elements of s under closer w₀ — with closestWorlds its Finset form; the Limit Assumption (closest_nonempty, closestWorlds_nonempty) is Set.Finite.exists_minimal. isCentered is strong centering, and w₁ ≤[sim, w₀] w₂ is notation for sim.closer w₀ w₁ w₂.

Structure

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

A family of comparative-similarity preorders, one for each center w₀: closer w₀ w₁ w₂ says that w₁ is at least as similar to w₀ as w₂ is.

• closer : W → W → W → Prop

  w₁ is at least as similar to w₀ as w₂ is.

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

  Closeness is decidable at each center.

@[instance_reducible]

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

Equations

• sim.instDecidableCloser w₀ w₁ w₂ = sim.decClose w₀ w₁ w₂

instance Semantics.Conditionals.SimilarityOrdering.instReflCloser {W : Type u_1} (sim : SimilarityOrdering W) (w₀ : W) : Std.Refl (sim.closer w₀)

instance Semantics.Conditionals.SimilarityOrdering.instIsTransCloser {W : Type u_1} (sim : SimilarityOrdering W) (w₀ : W) : IsTrans W (sim.closer w₀)

@[reducible]

def Semantics.Conditionals.SimilarityOrdering.atCenter {W : Type u_1} (sim : SimilarityOrdering W) (w₀ : W) : Preorder W

The preorder centered at w₀, for local use in proofs.

Equations

• sim.atCenter w₀ = Preorder.ofLE (sim.closer w₀) ⋯ ⋯

Constructors

def Semantics.Conditionals.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 can typically be discharged by decide.

Equations

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

Centering

def Semantics.Conditionals.SimilarityOrdering.isCentered {W : Type u_1} (sim : SimilarityOrdering W) : Prop

A strongly centered similarity ordering: every world is strictly closest to itself ([Lew73b]'s centering axiom).

Equations

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

Closest worlds

def Semantics.Conditionals.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₀.

Equations

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

@[simp]

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

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

theorem Semantics.Conditionals.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 Semantics.Conditionals.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.

theorem Semantics.Conditionals.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 ([Lew73b]): every non-empty Finset has a closest world. Routes through Set.Finite.exists_minimal on the preorder centered at w₀.

Closest worlds of a set

def Semantics.Conditionals.SimilarityOrdering.closest {W : Type u_1} (sim : SimilarityOrdering W) (w₀ : W) (s : Set W) : Set W

The closest s-worlds to w₀: the minimal elements of s under the similarity preorder centered at w₀. closestWorlds is the Finset form.

Equations

• sim.closest w₀ s = {w : W | w ∈ s ∧ ∀ w' ∈ s, (w ≤[sim,w₀] w') ∨ ¬w' ≤[sim,w₀] w}

theorem Semantics.Conditionals.SimilarityOrdering.closest_subset {W : Type u_1} (sim : SimilarityOrdering W) (w₀ : W) (s : Set W) : sim.closest w₀ s ⊆ s

@[simp]

theorem Semantics.Conditionals.SimilarityOrdering.coe_closestWorlds {W : Type u_1} [DecidableEq W] (sim : SimilarityOrdering W) (w₀ : W) (A : Finset W) : ↑(sim.closestWorlds w₀ A) = sim.closest w₀ ↑A

theorem Semantics.Conditionals.SimilarityOrdering.closest_nonempty {W : Type u_1} (sim : SimilarityOrdering W) (w₀ : W) {s : Set W} (hs : s.Finite) (hne : s.Nonempty) : (sim.closest w₀ s).Nonempty

The Limit Assumption for finite sets.

@[instance_reducible]

instance Semantics.Conditionals.SimilarityOrdering.instDecidablePredMemSetClosestOfFintype {W : Type u_1} [Fintype W] (sim : SimilarityOrdering W) (w₀ : W) (s : Set W) [DecidablePred fun (x : W) => x ∈ s] : DecidablePred fun (x : W) => x ∈ sim.closest w₀ s

Equations

• sim.instDecidablePredMemSetClosestOfFintype w₀ s w = Semantics.Conditionals.SimilarityOrdering.instDecidablePredMemSetClosestOfFintype._aux_1 sim w₀ s w

Selection-function bridge primitives

def Semantics.Conditionals.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.

Equations

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

def Semantics.Conditionals.«term_≤[_,_]_» : Lean.TrailingParserDescr

Comparative-closeness notation ([Lew73b]): w₁ ≤[sim, w₀] w₂ reads "w₁ is at least as similar to w₀ as w₂ is".

Equations

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