Documentation

Linglib.Theories.Semantics.Tense.MaximalInformativity

Maximal Informativity and Temporal in-Adverbials #

@cite{beck-rullmann-1999} @cite{fox-hackl-2006} @cite{kennedy-2007} @cite{krifka-1989} @cite{krifka-1998} @cite{rouillard-2026}

@cite{rouillard-2026} "Maximal informativity accounts for the distribution of temporal in-adverbials" (Linguistics and Philosophy 49:1–56).

Core Contribution #

Temporal in-adverbials (TIAs) lead a double life:

Both distributional restrictions derive from a single principle:

Maximal Informativity Principle (MIP): for some constituent of the LF in which a TIA appears, the numeral in the TIA's measure phrase must be capable of being maximally informative. If no number can be maximally informative (information collapse), the TIA is blocked.

Architecture #

Mereology (CUM, DIV, QUA) ──▷ scalar properties of derived TIA meanings
         │ │
     telicity informativity
         │ │
         ▼ ▼
E-TIA licensing ◁───── MIP ─────▷ G-TIA polarity sensitivity
                                         │
                              open PTS + closed runtime
                                 (from Time.lean)

Sections #

  1. Maximal informativity (max⊨)
  2. Measure functions and pts (prior time spans)
  3. E-TIA semantics: in as event-level map function
  4. G-TIA semantics: in as perfect-level identity map
  5. The MIP as a licensing condition
  6. Information collapse theorems
  7. Bridge: Kennedy open/closed scales ↔ TIA licensing
@[reducible, inline]

Upward scalarity for ℕ-indexed families. Specialization of Core.Scale.IsUpwardMonotone to ℕ. @cite{rouillard-2026} p. 24: outputs of (77) are totally ordered by entailment, smaller values entail larger ones. @cite{beck-rullmann-1999}: the maximally informative number is the smallest value returning a true proposition.

Equations
Instances For
    @[reducible, inline]

    Downward scalarity for ℕ-indexed families. Specialization of Core.Scale.IsDownwardMonotone to ℕ.

    Equations
    Instances For
      theorem Semantics.Montague.Sentence.MaximalInformativity.upwardScalar_hasMaxInf {W : Type u_1} (P : WProp) (hUS : UpwardScalar P) (w : W) (n : ) (hn : P n w) (hMin : m < n, ¬P m w) :

      Upward scalar properties have maximally informative elements: the smallest true value is max⊨ (it entails all others). This is the abstract version of Rouillard's argument for why E-TIAs with telic VPs are acceptable.

      theorem Semantics.Montague.Sentence.MaximalInformativity.biscalar_constant_collapse {W : Type u_1} (P : WProp) (hDS : DownwardScalar P) (hUS : UpwardScalar P) (w : W) (n : ) (hn : P n w) (m : ) :
      P m w

      Bimonotone ℕ-families (both upward and downward scalar) make every value true at every world where any value is true. @cite{rouillard-2026} p. 25: the property in (80) is both upward and downward scalar — equivalently, it is a constant function. This is information collapse. Derived from Core.Scale.bimonotone_constant.

      A temporal measure function: assigns positive durations to intervals. @cite{rouillard-2026} §2.2.2, eq. (5)–(7): μ is additive over non-overlapping times and positive.

      • μ : Core.Time.Interval Time

        The measure of an interval in some unit φ

      • extensible (i : Core.Time.Interval Time) (m : ) : self.μ i m∃ (j : Core.Time.Interval Time), i.subinterval j self.μ j = m

        Any interval can be extended to a superinterval with a given larger measure. @cite{rouillard-2026}: temporal measure units (days, hours) are additive, so any interval can be padded to achieve any target measure ≥ current.

      • subdivisible (i : Core.Time.Interval Time) (m : ) : m self.μ i∃ (j : Core.Time.Interval Time), j.subinterval i self.μ j = m

        Any interval can be subdivided to a subinterval with a given smaller measure. @cite{rouillard-2026}: temporal measure units are additive, so any interval can be trimmed to achieve any target measure ≤ current.

      Instances For
        def Semantics.Montague.Sentence.MaximalInformativity.pts {Time : Type u_2} [LinearOrder Time] (n : ) (μ : MeasureFun Time) (s : Time) (interval : Core.Time.Interval Time) :

        Prior time span: the maximal interval right-bounded by t with measure n. @cite{rouillard-2026} eq. (50): pts(n, φ, t¹) := max⊑ᵢ(λt².t² ∈ S ∧ ∃t³[μ_φ(t³) = n ∧ rb(t¹, t²) ∧ t² ⊑ᵢ t³]) Simplified: pts(n, μ, s) is the interval consisting of every moment inclusively ordered between s and the moment n φ-units prior to s.

        Equations
        Instances For

          The preposition in as an event-level adverbial (E-TIA reading). @cite{rouillard-2026} eq. (62): ⟦in⟧ := λM_σi λt λx_σ. M(x) ⊑ᵢ t. For E-TIAs, M = τ (runtime function): the event's runtime is included in the time denoted by the measure phrase.

          Type: (e → Interval Time) → Time → (e → Prop) Instantiation for E-TIA: M = Eventuality.τ

          Equations
          Instances For

            E-TIA derived property: for each number n, the property that at world w there exists a P-event whose runtime is included in an n-unit time ending at g(1). @cite{rouillard-2026} eq. (77): λnλw.∃t[μ_d(t) = n ∧ ∃e[P(e)(w) ∧ τ_w(e) ⊑ᵢ g(1) ∧ τ_w(e) ⊑ᵢ t]]

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Semantics.Montague.Sentence.MaximalInformativity.gTIAProperty {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Tense.Aspect.Core.EventPred W Time) (μ : MeasureFun Time) (s : Time) :
              WProp

              G-TIA derived property: for each number n, the property that at world w an event's runtime is included in the prior time span pts(n, d, s). @cite{rouillard-2026} eq. (94), revised with open PTS (101): λnλw.∃e[P(e)(w) ∧ τ_w(e) ⊑ᵢ o(pts(n, d, s))]

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

                Maximal Informativity Principle (MIP). @cite{rouillard-2026} eq. (92): Given a numeral N, a measure word M, an index j, and a map function F, a constituent of the form [ [ N M] j … [ in F] tⱼ] is licensed only if it is contained in a constituent γ such that, for some w¹, max⊨(w¹, λnλw². ⟦γ[N ↦ proₖ]⟧) = ⟦N⟧.

                The TIA is licensed iff the numeral can be maximally informative in some constituent γ containing it.

                Equations
                Instances For

                  E-TIA is MIP-licensed iff the derived E-TIA property has a maximally informative numeral at some world.

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

                    G-TIA is MIP-licensed (in positive environment) iff the derived G-TIA property has a maximally informative numeral at some world.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def Semantics.Montague.Sentence.MaximalInformativity.gTIAPropertyNeg {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Tense.Aspect.Core.EventPred W Time) (μ : MeasureFun Time) (s : Time) :
                      WProp

                      G-TIA under negation: the negated G-TIA property.

                      Equations
                      Instances For

                        G-TIA is MIP-licensed under negation.

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

                          E-TIA Information Collapse for Atelic VPs. When a VP predicate has the subinterval property (is atelic/DIV), the E-TIA property is both upward and downward monotone (constant), so no numeral is maximally informative → the E-TIA is blocked. @cite{rouillard-2026} §4.1.1: the interaction of the subinterval property with E-TIAs results in information collapse.

                          Proof: For any world w where eTIAProperty holds at n, we show it holds at m for arbitrary m. Given P-event e at w:

                          • If m ≤ μ(τ(e)): subdivide τ(e) to get j ⊆ τ(e) with μ(j) = m. By SUB, ⟨j⟩ is a P-event. Since j ⊆ τ(e) ⊆ g1, j ⊆ g1.
                          • If m ≥ μ(τ(e)): extend τ(e) to get j ⊇ τ(e) with μ(j) = m. Same event e works.

                          Quantized predicates yield upward scalar E-TIA properties. @cite{rouillard-2026} §4.1.1: when P is QUA (telic), the E-TIA property in (77) is upward scalar — propositions from smaller n entail those from larger n. The maximally informative number is the smallest n returning a true proposition (= the actual duration of the event).

                          This is the structural explanation for why E-TIAs are acceptable with telic VPs: there exists a unique maximally informative number. Proof: The same event e works. Extend the containing time t (with μ(t) = n) to j ⊇ t with μ(j) = m ≥ n via MeasureFun.extensible. Since τ(e) ⊆ t ⊆ j, the witness transfers.

                          theorem Semantics.Montague.Sentence.MaximalInformativity.no_smallest_open_including_closed {Time : Type u_2} [LinearOrder Time] [DenselyOrdered Time] (runtime : Core.Time.Interval Time) (pts_open : Core.Time.Interval.GInterval Time) (_h_open : pts_open.isOpen) (h_contains : runtime.subinterval pts_open.toInterval) (h_nontrivial : pts_open.left < runtime.start) :
                          ∃ (pts' : Core.Time.Interval.GInterval Time), pts'.isOpen runtime.subinterval pts'.toInterval pts'.toInterval.subinterval pts_open.toInterval pts'.left pts_open.left

                          No smallest open PTS can include a closed runtime. @cite{rouillard-2026} §4.2.2, key insight: given dense time, if event runtimes are closed and PTSs are open, there can never be a smallest open interval to include a closed time — because by density, there is always a moment between the open boundary and the closed boundary, giving a smaller PTS.

                          This is the structural reason why G-TIAs in positive environments suffer information collapse: the G-TIA property is downward scalar with no minimum.

                          Proof: By density (DenselyOrdered), find m with pts_open.left < m < runtime.start. The open interval]m, pts_open.right[ still contains runtime (m < runtime.start and runtime.finish ≤ pts_open.right) and is strictly contained in pts_open (pts_open.left < m).

                          The analogy between @cite{kennedy-2007}'s scale typology for gradable adjectives and @cite{rouillard-2026}'s TIA licensing is structural — both use Core.Scale.Boundedness to classify their scales, and Boundedness.isLicensed derives the same licensing prediction from the classification:

                          | Kennedy (Adjectives)              | Rouillard (TIAs)                     |
                          |------------------------------------|--------------------------------------|
                          | Open scale (tall, expensive)       | Atelic VP / DIV predicate            |
                          | → context-dependent threshold      | → information collapse, no max⊨     |
                          | → RGA: "??completely tall"         | → E-TIA blocked: "*was sick in 3d"  |
                          |                                    |                                      |
                          | Closed scale (full, empty)         | Telic VP / QUA predicate             |
                          | → scale-structure standard (max/min)| → upward scalar, max⊨ exists       |
                          | → AGA: "completely full" ✓         | → E-TIA licensed: "wrote in 3d" ✓  |
                          |                                    |                                      |
                          | Interpretive Economy               | Maximal Informativity Principle       |
                          | → maximize conventional meaning    | → maximize numeral contribution      |
                          
                          Kennedy's `Boundedness.open_` (= Krifka's DIV),
                          and Kennedy's `Boundedness.closed` (= Krifka's QUA).
                          
                          For G-TIAs, the relevant "scale" is the PTS: open PTSs behave like
                          open scales (no inherent bound → no maximum standard), while closed
                          runtimes behave like closed scales (inherent bound → standard exists). 
                          
                          @[reducible, inline]

                          Vendler class determines scale boundedness via the Kennedy–Rouillard isomorphism (Core.Scale), derived through a compositional chain: VendlerClass →.telicity Telicity →.toMereoTag MereoTag →.toBoundedness Boundedness. Telic VPs → QUA → closed/bounded (max⊨ exists). Atelic VPs → CUM → open/unbounded (information collapse).

                          Equations
                          Instances For

                            Revised PERFECT: the perfect's domain of quantification is restricted to open intervals (S ∩ O in Rouillard's notation). @cite{rouillard-2026} eq. (107): ⟦PERF⟧ := λI_it λt¹.∃t² ∈ S ∩ O[rb(t¹, t²) ∧ I(t²)]

                            This revision is the key to deriving G-TIA polarity sensitivity:

                            • In positive environments, the smallest open PTS to include a closed runtime cannot exist (by density), so no number is maximally informative.
                            • In negative environments, the largest open PTS to exclude a closed runtime always exists (the one abutting the runtime's boundary), so a maximally informative number exists.
                            Equations
                            Instances For

                              E-TIA expressions are upward monotone in the numeral (@cite{rouillard-2026} §3): "wrote a paper in three days" entails "wrote a paper in four days" because τ(e) ⊑ t with |t| = 3 implies τ(e) ⊑ t' with |t'| = 4.

                              This upward monotonicity is a property of the *expression* "in n days"
                              (due to the containment semantics of *in*), NOT of the numeral itself.
                              The numeral "three" can be exact (@cite{kennedy-2015} de-Fregean type-shift:
                              closed scale → Class B → exact meaning), and the expression is still
                              upward monotone because containment is monotone in the interval size.
                              
                              Indeed, exact numerals are arguably REQUIRED: with LB numerals (|t| ≥ n),
                              ∃t. |t| ≥ n ∧ τ(e) ⊑ t is trivially true for any event (pick a large
                              enough interval). Only exact numerals (|t| = n) make "in n days"
                              informative: it then asserts |τ(e)| ≤ n.
                              
                              The exact reading of the DURATION ("took exactly 3 days, not 2") arises
                              via scalar implicature over the upward-monotone expression, parallel to
                              Kennedy's analysis of "the glass is full" (endpoint standard + exactness). 
                              
                              theorem Semantics.Montague.Sentence.MaximalInformativity.eTIA_expression_upward_monotone {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Tense.Aspect.Core.EventPred W Time) (μ : MeasureFun Time) (g1 : Core.Time.Interval Time) (n m : ) (hnm : n m) (w : W) (h : eTIAProperty P μ g1 n w) :
                              eTIAProperty P μ g1 m w

                              E-TIA expressions are upward monotone in the numeral: if the event fits in an n-unit time, it fits in an m-unit time for m ≥ n. This follows from the containment semantics of in (τ(e) ⊑ t), not from the numeral being lower-bounded. Compatible with @cite{kennedy-2015} exact numerals on closed scales.

                              Rouillard's closed subinterval property (CSUB, eq. 111) is the temporal analog of Krifka/Champollion's DIV (divisive reference). DIV says every part of a P-entity is itself P; CSUB says the closed counterpart of every subinterval of a P-event's runtime is itself a P-event's runtime.

                              The bridge: if an event predicate is DIV (in the mereological sense from
                              `Mereology.lean`), then it has the closed subinterval property (in the
                              temporal sense needed for G-TIA polarity). 
                              

                              DIV event predicates have the (plain) subinterval property. If P is downward-closed under the part-of relation on events, then any subinterval of a P-event's runtime that is itself some event's runtime is a P-event's runtime.