Documentation

Linglib.Theories.Semantics.Degree.Equative

Equative Semantics #

@cite{kennedy-2007} @cite{rett-2020} @cite{schwarzschild-2008} @cite{thomas-deo-2020}

Compositional semantics for equative constructions ("as tall as").

At-Least vs. Exactly #

The literal semantics of the equative is "at least as tall as" (≥). The "exactly as tall as" reading arises via scalar implicature: the speaker chose "as tall as" over the stronger "taller than", implicating that "taller than" is false, yielding equality.

This parallels numeral strengthening: "three" literally means "at least three" and is strengthened to "exactly three" by implicature.

Alternative: Granularity-Based Account #

Degree.Granularity offers a different explanation: the "exactly" reading arises because just signals finest granularity, and the finest equative is already the strongest (so just's negative component is vacuous). See just_vacuous_iff in Degree.Granularity.

source
def Semantics.Degree.Equative.equativeLiteral {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (a b : Entity) :
Prop

Equative literal semantics: "A is as tall as B" iff μ(A) ≥ μ(B). This is the "at least as" reading.

Equations
Instances For
    source
    def Semantics.Degree.Equative.equativeStrengthened {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (a b : Entity) :
    Prop

    Equative strengthened semantics: "A is as tall as B" iff μ(A) = μ(B). This is the "exactly as" reading, derived by implicature.

    Equations
    Instances For
      source
      theorem Semantics.Degree.Equative.strengthened_entails_literal {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (a b : Entity) :
      equativeStrengthened μ a b → equativeLiteral μ a b

      The strengthened reading entails the literal reading.

      source
      def Semantics.Degree.Equative.negatedEquative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) :
      Prop

      Negated equative: "A is not as tall as B" iff μ(A) < μ(B). Negation of the at-least semantics yields strict less-than.

      Equations
      Instances For
        source
        theorem Semantics.Degree.Equative.negated_iff_not_literal {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) :
        negatedEquative μ a b ↔ ¬equativeLiteral μ a b

        Negated equative is the negation of the literal equative.