Documentation

Studies.Blok2015

Blok (2015): The semantics and pragmatics of directional numeral modifiers #

This file formalizes the paper's account of directional numeral modifiers, the prepositions of direction used to modify a numeral, such as up to. They differ from the other modifiers that set an upper bound, such as at most: their lower bound cannot be cancelled and their upper bound can, they are odd with the lowest number of a scale, and they do not license negative polarity items. The paper derives the differences from two claims. A directional modifier asserts a lower bound and only implicates its upper bound, and every Class B modifier needs a range of values to quantify over.

The implementation follows the paper's, in unrestricted inquisitive semantics. A sentence denotes a set of possibilities. Up to n raises the possibilities that at least m hold, for m from the bottom s of the scale to n, so its informational content is that at least s hold (sUnion_upTo), with no upper bound. Exhaustifying each possibility against the question of how many leaves the possibilities of exactly m, and the upper bound n is an implicature (sUnion_exh_upTo). At most n, on Coppock and Brochhagen's analysis, raises the possibilities between m and n, so its content is the upper bound and is compatible with zero (sUnion_atMost). The range requirement is that the sentence raise more than one possibility, which fails for up to at the bottom of the scale and for at most 0 (nontrivial_upTo, nontrivial_atMost). The paper's judgments on the two kinds of modifier are checked against these predictions (judgment_rows).

Implementation notes #

Worlds are counts, as in the paper's simplified model with one world for each number. A proposition is a Set (Set ℕ) and not the library's Question, which is downward closed and identifies a proposition with its maximal possibilities, while the possibilities of up to are nested. At most is Coppock and Brochhagen's entry on the question of how many with one-sided answers (atMost_eq), and exhaustification is theirs too. The bottom of the scale is 1 in the rows, the whole numbers.

References #

The two denotations #

source
def Blok2015.upTo (s n : ℕ) :
Set (Set ℕ)

(45): up to n on a scale with bottom s raises the possibilities that at least m hold, for each m from s to n.

Equations
Instances For
    source
    def Blok2015.atMost (n : ℕ) :
    Set (Set ℕ)

    At most n (43c) is [CB13]'s entry on the question of how many, with an answer Ici m for each lower bound m.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Blok2015.atMost_eq (n : ℕ) :
      atMost n = (fun (x : ℕ) => Set.Icc x n) '' Set.Iic n

      At most n raises the possibilities that between m and n hold, for each m up to n.

      source
      theorem Blok2015.sUnion_upTo {s n : ℕ} (h : s ≤ n) :
      ⋃₀ upTo s n = Set.Ici s

      The informational content of up to n is its lower bound. At least the bottom of the scale hold, and nothing bounds the count from above.

      source
      theorem Blok2015.sUnion_atMost {n : ℕ} :
      ⋃₀ atMost n = Set.Iic n

      The informational content of at most n is its upper bound.

      The implicated upper bound #

      source
      def Blok2015.howMany :
      Set (Set ℕ)

      (51): the question of how many, with a possibility for each lower bound.

      Equations
      Instances For
        source
        theorem Blok2015.Ici_diff_sUnion_howMany {m : ℕ} :
        Set.Ici m \ ⋃₀ {q : Set ℕ | q ∈ howMany ∧ ¬Set.Ici m ⊆ q} = {m}

        Exhaustified against the question of how many, at least m is exactly m.

        source
        theorem Blok2015.exh_upTo_howMany {s n : ℕ} :
        Inquisitive.Unrestricted.exh (upTo s n) howMany = (fun (m : ℕ) => {m}) '' Set.Icc s n

        Exhaustification turns the possibilities of up to n into those of exactly m, for m from the bottom of the scale to n (50), (51).

        source
        theorem Blok2015.sUnion_exh_upTo {s n : ℕ} :
        ⋃₀ Inquisitive.Unrestricted.exh (upTo s n) howMany = Set.Icc s n

        The upper bound of up to n is an implicature. The exhaustified content is bounded by n, where the asserted content sUnion_upTo is not.

        The range requirement #

        source
        theorem Blok2015.nontrivial_upTo {s n : ℕ} :
        (upTo s n).Nontrivial ↔ s < n

        Up to n raises more than one possibility just in case n is above the bottom of the scale, which is the bottom-of-the-scale effect.

        source
        theorem Blok2015.nontrivial_atMost {n : ℕ} :
        (atMost n).Nontrivial ↔ 0 < n

        At most n raises more than one possibility just in case n is not zero.

        Monotonicity #

        The asserted content of up to is closed upward and that of at most downward, so only at most is downward monotone and licenses negative polarity items.

        source
        theorem Blok2015.isUpperSet_sUnion_upTo {s n : ℕ} :
        IsUpperSet (⋃₀ upTo s n)
        source
        theorem Blok2015.isLowerSet_sUnion_atMost {n : ℕ} :
        IsLowerSet (⋃₀ atMost n)
        source
        theorem Blok2015.not_isLowerSet_sUnion_upTo {s n : ℕ} (hs : 0 < s) (h : s ≤ n) :
        ¬IsLowerSet (⋃₀ upTo s n)

        The judgments #

        source
        inductive Blok2015.Test :
        Type

        The diagnostics of the paper's examples are a continuation if any, a contrast with no-one, a continuation that cancels or reinforces the upper bound, a bare sentence testing the range requirement, and a negative polarity item.

        Instances For
          source
          @[instance_reducible]
          instance Blok2015.instDecidableEqTest :
          DecidableEq Test
          Equations
          source
          @[instance_reducible]
          instance Blok2015.instReprTest :
          Repr Test
          Equations
          source
          def Blok2015.instReprTest.repr :
          Test → ℕ → Std.Format
          Equations
          Instances For
            source
            def Blok2015.testOf :
            String → Option Test

            The diagnostic a row's feature names.

            Equations
            Instances For
              source
              def Blok2015.proposition (directional : Bool) (n : ℕ) :
              Set (Set ℕ)

              The possibilities a modifier raises with the number n on the scale of the whole numbers, by whether the modifier is directional.

              Equations
              Instances For
                source
                def Blok2015.Predicted (P : Set (Set ℕ)) (n : ℕ) :
                Test → Prop

                What the account predicts acceptable. If any needs content compatible with zero and the contrast with no-one content that excludes it. Cancelling or reinforcing the upper bound needs a bound that is not asserted. A bare sentence needs more than one possibility, and a negative polarity item downward monotone content.

                Equations
                Instances For
                  source
                  theorem Blok2015.predicted_upTo_iff {n : ℕ} (t : Test) :
                  Predicted (upTo 1 n) n t ↔ t = Test.butNone ∨ t = Test.upperBound ∧ 1 ≤ n ∨ t = Test.range ∧ 1 < n ∨ t = Test.npi ∧ n = 0
                  source
                  theorem Blok2015.predicted_atMost_iff {n : ℕ} (t : Test) :
                  Predicted (atMost n) n t ↔ t = Test.ifAny ∨ t = Test.range ∧ 0 < n ∨ t = Test.npi
                  source
                  @[instance_reducible]
                  instance Blok2015.instDecidablePredictedProposition {n : ℕ} (d : Bool) (t : Test) :
                  Decidable (Predicted (proposition d n) n t)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  theorem Blok2015.judgment_rows (row : Datum) :
                  row ∈ Examples.all → ∃ (t : Test), (row.feature? "test").bind testOf = some t ∧ ∃ (n : ℕ), row.nat? "numeral" = some n ∧ (row.judgment = Judgment.acceptable ↔ Predicted (proposition (decide (row.feature? "directional" = some "+")) n) n t)

                  Every judgment of the paper's rows is the account's prediction. A row is acceptable just in case its modifier, with its number, passes its diagnostic.