Documentation

Linglib.Theories.Semantics.Degree.ThanClause

Than-Clause Semantics #

@cite{bhatt-pancheva-2004} @cite{heim-2006} @cite{von-stechow-1984}

Compositional semantics for the than-clause in comparative constructions. The than-clause introduces the standard of comparison and determines the degree set against which the matrix predicate is evaluated.

Key Issues #

  1. Max operator: the than-clause denotes a degree set, and the comparative requires its maximum (max(than-clause)) to compare against the matrix degree.

  2. Phrasal vs. clausal: phrasal "than Bill" vs. clausal "than Bill is tall" — the clausal than-clause makes the degree abstraction explicit.

  3. Scope: the than-clause interacts with scope-taking elements (quantifiers, modals, negation).

source
def Semantics.Degree.ThanClause.thanClauseDenotation {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (standard : Entity) :
Set D

A than-clause denotes a degree predicate: the set of degrees that the standard entity has.

"than Bill is tall" → λd. height(Bill) ≥ d = {d | d ≤ height(Bill)}

This is a downward-closed set (initial segment) when the predicate is a positive adjective.

Equations
Instances For
    source
    def Semantics.Degree.ThanClause.thanClauseMax {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (standard : Entity) :
    D

    The maximum of a than-clause denotation is the degree of the standard entity: max({d | d ≤ μ(b)}) = μ(b).

    Only [Preorder D] is needed: the standard's measure is the greatest element of its own downward-closure regardless of linearity.

    Equations
    Instances For
      source
      theorem Semantics.Degree.ThanClause.thanClauseMax_isGreatest {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (b : Entity) :
      IsGreatest (thanClauseDenotation μ b) (thanClauseMax μ b)

      μ(b) is the greatest element of the than-clause denotation. This is isGreatest_Iic specialized to degree semantics: the maximum of {d | d ≤ μ(b)} is μ(b). Only [Preorder D] required.

      source
      inductive Semantics.Degree.ThanClause.ThanClauseType :
      Type

      The two syntactic forms of than-clauses.

      Instances For
        source
        @[implicit_reducible]
        instance Semantics.Degree.ThanClause.instDecidableEqThanClauseType :
        DecidableEq ThanClauseType
        Equations
        source
        def Semantics.Degree.ThanClause.instReprThanClauseType.repr :
        ThanClauseType → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          instance Semantics.Degree.ThanClause.instReprThanClauseType :
          Repr ThanClauseType
          Equations
          source
          theorem Semantics.Degree.ThanClause.phrasal_clausal_equivalence {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (b : Entity) :
          thanClauseMax μ b = μ b

          Phrasal and clausal than-clauses yield the same degree when the elided material is the same predicate. "taller than Bill" and "taller than Bill is tall" have the same truth conditions.

          source
          theorem Semantics.Degree.ThanClause.thanClause_eq_posExt {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (b : Entity) :
          thanClauseDenotation μ b = Core.Scale.posExt μ b

          The than-clause denotation is the positive extent of the standard entity — the same algebraic object that Kennedy calls "degree set" and Schwarzschild calls "positive interval".