Documentation

Linglib.Semantics.Conditionals.Counterfactual.Alternatives

Counterfactuals over sets of antecedent propositions #

A conditional whose antecedent denotes a set of propositions S rather than a single one — the disjuncts of a disjunctive antecedent ([AO09]) or the antecedent's truthmakers ([San18b]) — can be read distributively or collectively. Distributive requires the counterfactual of each proposition in S ([AO09]'s universal quantification over alternatives, the assertion of [San18b]'s DIST_π) and so validates Simplification of Disjunctive Antecedents by construction; would lets the modal extract the disjunctive closure ⋁S ([San18b]), which is [Lew73b]'s counterfactual on the disjunction and does not. homogeneity is the all-or-nothing verdict — .true when every proposition's counterfactual holds, .false when none does, .indet otherwise — the presupposition of DIST_π and the trivalent conditional of [CG20].

source
def Semantics.Conditionals.Counterfactual.disjunctiveClosure {W : Type u_1} [DecidableEq W] (S : List (Finset W)) :
Finset W

The disjunctive closure ⋁S.

Equations
Instances For
    source
    @[simp]
    theorem Semantics.Conditionals.Counterfactual.mem_disjunctiveClosure {W : Type u_1} [DecidableEq W] (S : List (Finset W)) {x : W} :
    x ∈ disjunctiveClosure S ↔ ∃ A ∈ S, x ∈ A
    source
    def Semantics.Conditionals.Counterfactual.would {W : Type u_1} [DecidableEq W] [Fintype W] (sim : SimilarityOrdering W) (S : List (Finset W)) (C : W → Prop) [DecidablePred C] (w : W) :
    Prop

    The modal over S quantifies over the closest worlds of its disjunctive closure.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Semantics.Conditionals.Counterfactual.Distributive {W : Type u_1} [DecidableEq W] [Fintype W] (sim : SimilarityOrdering W) (S : List (Finset W)) (C : W → Prop) [DecidablePred C] (w : W) :
      Prop

      The distributive reading: the counterfactual holds of each proposition in S.

      Equations
      Instances For
        source
        def Semantics.Conditionals.Counterfactual.homogeneity {W : Type u_1} [DecidableEq W] [Fintype W] (sim : SimilarityOrdering W) (S : List (Finset W)) (C : W → Prop) [DecidablePred C] (w : W) :
        Trivalent

        The all-or-nothing verdict over S.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[instance_reducible]
          instance Semantics.Conditionals.Counterfactual.instDecidableWould {W : Type u_1} [DecidableEq W] [Fintype W] (sim : SimilarityOrdering W) (S : List (Finset W)) (C : W → Prop) [DecidablePred C] (w : W) :
          Decidable (would sim S C w)
          Equations
          source
          @[instance_reducible]
          instance Semantics.Conditionals.Counterfactual.instDecidableDistributive {W : Type u_1} [DecidableEq W] [Fintype W] (sim : SimilarityOrdering W) (S : List (Finset W)) (C : W → Prop) [DecidablePred C] (w : W) :
          Decidable (Distributive sim S C w)
          Equations
          source
          theorem Semantics.Conditionals.Counterfactual.distributive_iff_homogeneity_eq_true {W : Type u_1} [DecidableEq W] [Fintype W] (sim : SimilarityOrdering W) (S : List (Finset W)) (C : W → Prop) [DecidablePred C] (w : W) :
          Distributive sim S C w ↔ homogeneity sim S C w = Trivalent.true
          source
          theorem Semantics.Conditionals.Counterfactual.would_singleton {W : Type u_1} [DecidableEq W] [Fintype W] (sim : SimilarityOrdering W) (C : W → Prop) [DecidablePred C] (w : W) (A : Finset W) :
          would sim [A] C w ↔ universalCounterfactual sim (fun (x : W) => x ∈ A) C w

          On a singleton the modal quantifies over the closest worlds of its one proposition.

          source
          theorem Semantics.Conditionals.Counterfactual.universalCounterfactual_mem_filter {W : Type u_1} [DecidableEq W] [Fintype W] (sim : SimilarityOrdering W) (C : W → Prop) [DecidablePred C] (w : W) (A : W → Prop) [DecidablePred A] :
          universalCounterfactual sim (fun (x : W) => x ∈ Finset.filter A Finset.univ) C w ↔ universalCounterfactual sim A C w

          A proposition given as a predicate and as the finset of its worlds yield the same counterfactual.