Documentation

Linglib.Theories.Semantics.Degree.Frameworks.Rett

Rett's Order-Sensitive MAX Framework #

@cite{rett-2026} @cite{rullmann-1995} @cite{schwarzschild-2008} @cite{krifka-2010b}

@cite{rett-2026} "Semantic Ambivalence and Expletive Negation": the comparative morpheme is an order-sensitive maximality operator MAX_R that picks the R-maximal element of a degree set.

This framework absorbs and extends the content previously in Theories/Semantics/Lexical/Adjective/Comparative.lean, providing a unified analysis of comparatives, temporal connectives, and expletive negation licensing.

Key Ideas #

  1. MAX_R: A domain-general maximality operator parameterized by a relation R. MAX_R(X) = {x ∈ X | ∀x' ∈ X, x' ≠ x → R x x'}. For <, this gives the minimum; for >, the maximum.

  2. Ambidirectionality: A construction f is ambidirectional for B iff f(B) ↔ f(Bᶜ). This holds when MAX picks the same boundary from both B and its complement.

  3. Expletive negation licensing: EN is licensed exactly in ambidirectional constructions, because negating the argument is truth-conditionally vacuous.

  4. Manner implicature: EN triggers evaluativity — the marked form signals that the comparison/temporal relation is noteworthy.

Connections #

source
@[reducible, inline]
abbrev Semantics.Degree.Frameworks.Rett.ScaleDirection :
Type

Comparative direction reuses scale polarity from Core. positive: "taller" — MAX picks the highest degrees. negative: "shorter" — MAX picks the lowest degrees.

Equations
Instances For
    source
    def Semantics.Degree.Frameworks.Rett.rettComparative {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) (dir : ScaleDirection) :
    Prop

    Rett/Schwarzschild comparative morpheme (eq. 47): "A is taller than B" iff MAX of A's degrees >_dir MAX of B's degrees.

    For singleton degree sets {μ(a)} and {μ(b)}, MAX is trivial (maxOnScale_singleton), so this reduces to direct comparison.

    Equations
    Instances For
      source
      theorem Semantics.Degree.Frameworks.Rett.rettComparative_eq_MAX {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) :
      rettComparative μ a b Core.Scale.ScalePolarity.positive ↔ ∃ m ∈ Core.Scale.maxOnScale (fun (x1 x2 : α) => x1 > x2) {μ b}, μ a > m

      MAX–direct bridge: the direct comparison μ(a) > μ(b) is equivalent to the MAX-based formulation. This makes explicit that rettComparative is a simplification of the general MAX-comparison, justified by maxOnScale_singleton.

      source
      theorem Semantics.Degree.Frameworks.Rett.comparative_boundary {α : Type u_1} [LinearOrder α] (μ_a μ_b : α) :
      (∃ m ∈ Core.Scale.maxOnScale (fun (x1 x2 : α) => x1 ≥ x2) {d : α | d ≤ μ_b}, μ_a > m) ↔ μ_a > μ_b

      The comparative depends only on the boundary μ_b, not on whether the standard is B = {d | d ≤ μ_b} or any other set sharing that supremum. This captures Rett's ambidirectionality insight: since MAX₍≥₎({d | d ≤ μ_b}) = {μ_b}, the existential reduces to a direct comparison.

      source
      theorem Semantics.Degree.Frameworks.Rett.equative_boundary {α : Type u_1} [LinearOrder α] (μ_a μ_b : α) :
      (∃ m ∈ Core.Scale.maxOnScale (fun (x1 x2 : α) => x1 ≥ x2) {d : α | d ≤ μ_b}, μ_a ≥ m) ↔ μ_a ≥ μ_b

      Equative boundary reduction: the equative also depends only on the boundary μ_b.

      source
      structure Semantics.Degree.Frameworks.Rett.MannerEffect :
      Type

      Manner implicature triggered by EN in an ambidirectional construction. evaluative: the relation is noteworthy (large gap / early timing). atypical: the EN form is pragmatically marked (optional, stylistic).

      • evaluative : Bool

        Does EN trigger an evaluative reading?

      • atypical : Bool

        Is the EN form pragmatically marked (optional, stylistic)?

      Instances For
        source
        instance Semantics.Degree.Frameworks.Rett.instDecidableEqMannerEffect :
        DecidableEq MannerEffect
        Equations
        source
        def Semantics.Degree.Frameworks.Rett.instDecidableEqMannerEffect.decEq (x✝ x✝¹ : MannerEffect) :
        Decidable (x✝ = x✝¹)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Semantics.Degree.Frameworks.Rett.instBEqMannerEffect.beq :
          MannerEffect → MannerEffect → Bool
          Equations
          Instances For
            source
            instance Semantics.Degree.Frameworks.Rett.instBEqMannerEffect :
            BEq MannerEffect
            Equations
            source
            instance Semantics.Degree.Frameworks.Rett.instReprMannerEffect :
            Repr MannerEffect
            Equations
            source
            def Semantics.Degree.Frameworks.Rett.instReprMannerEffect.repr :
            MannerEffect → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Semantics.Degree.Frameworks.Rett.enEvaluativeEffect :
              MannerEffect

              EN in ambidirectional constructions (comparatives, before-clauses) triggers evaluativity but is not atypical — it's a productive pattern cross-linguistically.

              Equations
              Instances For