Documentation

Linglib.Theories.Semantics.Conditionals.Counterfactual.QuantifierEmbedding

Quantified counterfactuals — projection-duality machinery #

@cite{ramotowska-marty-romoli-santorio-2025}

Extracted from Theories/Semantics/Conditionals/Counterfactual.lean (was lines 217–492). Provides the projection-duality apparatus that the @cite{ramotowska-marty-romoli-santorio-2025} study file uses to predict the strength × CF embedding pattern.

Projection Duality: Why Strength Matters #

Quantifier strength corresponds to a fundamental duality in how semantic values project through operators:

Universal-like operators (every, no, □, ∧):

Existential-like operators (some, not-every, ◇, ∨):

This duality manifests across natural-language semantics:

DomainUniversal-likeExistential-like
Quantified counterfactualsReject on mixedAccept on mixed
Presupposition projectionFiltering (universal)Existential accomm.
Homogeneity"The Xs P" needs all"Some Xs P" needs one
Free Choice□(A∨B) → □A∧□B◇(A∨B) → ◇A∧◇B
MonotonicityDownward entailingUpward entailing

The selectional theory captures this because three-valued logic with supervaluation naturally implements this projection duality.

Quantifier Embedding #

The three counterfactual theories make different predictions when counterfactuals are embedded under quantifiers in mixed scenarios (some individuals satisfy the consequent, others don't):

SentenceUniversalSelectionalHomogeneity
Every d □→FALSEFALSEPRESUP FAIL
Some d □→FALSETRUEPRESUP FAIL
No d □→TRUEFALSEPRESUP FAIL
Not every d □→TRUETRUEPRESUP FAIL

The universal and selectional theories agree on "every" and "not every" but DISAGREE on "some" and "no" — the discriminating contrast tested in @cite{ramotowska-marty-romoli-santorio-2025}.

source
@[reducible, inline]
abbrev Semantics.Conditionals.Counterfactual.QStrength :
Type

Quantifier strength IS projection type. Strong quantifiers (every, no) use conjunctive projection; weak quantifiers (some, not-every) use disjunctive.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Semantics.Conditionals.Counterfactual.QStrength.strong :
    QStrength

    Strong quantifiers use conjunctive projection.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Semantics.Conditionals.Counterfactual.QStrength.weak :
      QStrength

      Weak quantifiers use disjunctive projection.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Semantics.Conditionals.Counterfactual.QStrength.toProjection (s : QStrength) :
        Core.Duality.ProjectionType

        Identity: projection type is already itself.

        Equations
        Instances For
          source
          def Semantics.Conditionals.Counterfactual.projectTruthValues (proj : Core.Duality.ProjectionType) (results : List Core.Duality.Truth3) :
          Core.Duality.Truth3

          The Projection Duality Theorem.

          For a list of three-valued results:

          • Conjunctive projection: TRUE iff all TRUE, FALSE iff any FALSE
          • Disjunctive projection: TRUE iff any TRUE, FALSE iff all FALSE

          Implementation delegates to Core.Duality.aggregate, which computes the meet (⋀) or join (⋁) in the Truth3 lattice via foldl.

          Equations
          Instances For
            source
            theorem Semantics.Conditionals.Counterfactual.conjunctive_fragile (results : List Core.Duality.Truth3) (h : (results.any fun (x : Core.Duality.Truth3) => x == Core.Duality.Truth3.false) = true) :
            projectTruthValues Core.Duality.ProjectionType.conjunctive results ≠ Core.Duality.Truth3.true

            Conjunctive projection is fragile: one false element yields false.

            source
            theorem Semantics.Conditionals.Counterfactual.disjunctive_robust (results : List Core.Duality.Truth3) (h : (results.any fun (x : Core.Duality.Truth3) => x == Core.Duality.Truth3.true) = true) :
            projectTruthValues Core.Duality.ProjectionType.disjunctive results = Core.Duality.Truth3.true

            Disjunctive projection is robust: one true element yields true.

            source
            theorem Semantics.Conditionals.Counterfactual.projectTruthValues_eq_aggregate (proj : Core.Duality.ProjectionType) (l : List Core.Duality.Truth3) :
            projectTruthValues proj l = Core.Duality.aggregate proj l

            projectTruthValues and aggregate are the same operation.

            The four embedded-quantifier operators #

            source
            def Semantics.Conditionals.Counterfactual.embeddedSelectional (s : QStrength) (results : List Core.Duality.Truth3) :
            Core.Duality.Truth3

            Evaluate embedded counterfactual under a quantifier via projection. Strong quantifiers (every, no) use conjunctive projection; weak quantifiers (some, not every) use disjunctive projection.

            Equations
            Instances For
              source
              def Semantics.Conditionals.Counterfactual.noSelectional (results : List Core.Duality.Truth3) :
              Core.Duality.Truth3

              "No" quantifier: conjunctive projection over NEGATED individual results. "No X would V" = "Every X would NOT V".

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Semantics.Conditionals.Counterfactual.notEverySelectional (results : List Core.Duality.Truth3) :
                Core.Duality.Truth3

                "Not every" quantifier: disjunctive projection over NEGATED individual results. "Not every X would V" = "∃X. ¬(X would V)".

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

                  Selectional Theory: Embedded Determinacy #

                  @cite{ramotowska-marty-romoli-santorio-2025} §2.2.2: embedded selectional counterfactuals are DETERMINATE even though unembedded ones can be indeterminate. This is because the quantifier operates INSIDE the scope of the selection function — within each selected world, individual results are Bool (true/false), not Truth3.

                  source
                  theorem Semantics.Conditionals.Counterfactual.embeddedSelectional_determinate (s : QStrength) (bs : List Bool) :
                  embeddedSelectional s (List.map Core.Duality.Truth3.ofBool bs) ≠ Core.Duality.Truth3.indet

                  Embedded selectional determinacy: when individual results are all determinate (Bool), the projected result is always determinate.

                  source
                  theorem Semantics.Conditionals.Counterfactual.strength_determines_pattern (bs : List Bool) (h_some_true : bs.any id = true) (h_some_false : (bs.any fun (x : Bool) => !x) = true) :
                  embeddedSelectional QStrength.strong (List.map Core.Duality.Truth3.ofBool bs) = Core.Duality.Truth3.false ∧ embeddedSelectional QStrength.weak (List.map Core.Duality.Truth3.ofBool bs) = Core.Duality.Truth3.true

                  Strength determines pattern: under selectional semantics with mixed Bool individual results (some true, some false):

                  • Conjunctive projection (strong quantifiers) yields .false
                  • Disjunctive projection (weak quantifiers) yields .true
                  source
                  theorem Semantics.Conditionals.Counterfactual.no_mixed (bs : List Bool) (h_some_true : bs.any id = true) (h_some_false : (bs.any fun (x : Bool) => !x) = true) :
                  noSelectional (List.map Core.Duality.Truth3.ofBool bs) = Core.Duality.Truth3.false

                  "No" in mixed scenario gives FALSE under selectional semantics.

                  source
                  theorem Semantics.Conditionals.Counterfactual.notEvery_mixed (bs : List Bool) (h_some_true : bs.any id = true) (h_some_false : (bs.any fun (x : Bool) => !x) = true) :
                  notEverySelectional (List.map Core.Duality.Truth3.ofBool bs) = Core.Duality.Truth3.true

                  "Not every" in mixed scenario gives TRUE under selectional semantics.

                  source
                  theorem Semantics.Conditionals.Counterfactual.all_four_quantifiers_mixed (bs : List Bool) (h_some_true : bs.any id = true) (h_some_false : (bs.any fun (x : Bool) => !x) = true) :
                  embeddedSelectional QStrength.strong (List.map Core.Duality.Truth3.ofBool bs) = Core.Duality.Truth3.false ∧ embeddedSelectional QStrength.weak (List.map Core.Duality.Truth3.ofBool bs) = Core.Duality.Truth3.true ∧ noSelectional (List.map Core.Duality.Truth3.ofBool bs) = Core.Duality.Truth3.false ∧ notEverySelectional (List.map Core.Duality.Truth3.ofBool bs) = Core.Duality.Truth3.true

                  All four quantifiers in mixed scenarios: under selectional semantics with mixed Bool individual results, strong quantifiers (every, no) yield .false and weak quantifiers (some, not every) yield .true.

                  Universal Theory: All Individual Counterfactuals False #

                  Under the universal theory in a mixed scenario, EVERY individual counterfactual is false. The quantifier operates over a list of all-false values, giving DIFFERENT predictions from the selectional theory:

                  The theories agree on "every" and "not every" but DISAGREE on "some" and "no" — the empirical discriminators tested in @cite{ramotowska-marty-romoli-santorio-2025}.

                  source
                  theorem Semantics.Conditionals.Counterfactual.universal_all_false (n : ℕ) (hn : n > 0) :
                  projectTruthValues Core.Duality.ProjectionType.conjunctive (List.replicate n Core.Duality.Truth3.false) = Core.Duality.Truth3.false ∧ projectTruthValues Core.Duality.ProjectionType.disjunctive (List.replicate n Core.Duality.Truth3.false) = Core.Duality.Truth3.false

                  Universal theory embedded predictions: all individual CFs false.