Documentation

Linglib.Theories.Semantics.Lexical.Determiner.Definite

The Semantics of Definiteness #

@cite{donnellan-1966} @cite{heim-1982} @cite{kamp-1981} @cite{partee-1987} @cite{russell-1905} @cite{barwise-cooper-1981}

Denotations for definite descriptions using the type vocabulary from Core/Definiteness.lean. Two theories, formalized as determiner denotations with presuppositions:

Key Results #

source
def Semantics.Lexical.Determiner.Definite.the_uniq {E : Type} (domain : List E) [DecidableEq E] (restrictor scope : E → Bool) :
Core.Presupposition.PrProp Unit

⟦the⟧ under uniqueness (Russell/Strawson/@cite{heim-kratzer-1998}):

Presupposition: exactly one entity in the domain satisfies the restrictor. Assertion: the scope predicate holds of that entity.

Type: (e→t) → (e→t) → PrProp W (restrictor → scope → presuppositional proposition)

This corresponds to Schwarz's weak article (German contracted vom, Fering A-form, Lakhota kiŋ).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Semantics.Lexical.Determiner.Definite.the_uniq_w {W E : Type} (domain : List E) (restrictor scope : E → W → Bool) :
    Core.Presupposition.PrProp W

    ⟦the⟧ under uniqueness, world-indexed version.

    For intensional contexts where the restrictor extension varies by world. This is the standard @cite{heim-kratzer-1998} entry.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      structure Semantics.Lexical.Determiner.Definite.DiscourseContext (E : Type) :
      Type

      A discourse context tracking salient/familiar entities.

      @cite{heim-1982}: the context is a set of "file cards" — entities that have been introduced into the discourse and are available for anaphoric reference.

      • salient : List E

        Entities currently salient/familiar in discourse

      Instances For
        source
        def Semantics.Lexical.Determiner.Definite.the_fam {E : Type} [DecidableEq E] (dc : DiscourseContext E) (restrictor scope : E → Bool) :
        Core.Presupposition.PrProp Unit

        ⟦the⟧ under familiarity:

        Presupposition: there exists a salient entity in the discourse context matching the restrictor. Assertion: the scope predicate holds of that entity.

        This corresponds to Schwarz's strong article (German full von dem, Fering D-form, Lakhota k'uŋ, Akan nó).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Semantics.Lexical.Determiner.Definite.familiarity_weaker_existence {E : Type} [DecidableEq E] (dc : DiscourseContext E) (restrictor scope : E → Bool) (e : E) (h_sal : List.filter restrictor dc.salient = [e]) :
          (the_fam dc restrictor scope).presup () = true

          Familiarity presupposition requires discourse salience, not world-relative uniqueness. The same restrictor can succeed under familiarity but fail under uniqueness (if multiple entities satisfy the restrictor in the world but only one is discourse-salient).

          source
          theorem Semantics.Lexical.Determiner.Definite.the_uniq_eq_definitePrProp {W E : Type} (domain : List E) (restrictor scope : E → W → Bool) :
          the_uniq_w domain restrictor scope = Reference.Donnellan.definitePrProp domain restrictor scope

          The uniqueness-based definite IS Donnellan's attributive semantics.

          the_uniq_w and definitePrProp compute identical presuppositions and assertions. Both filter the domain for unique restrictor-satisfiers.

          source
          theorem Semantics.Lexical.Determiner.Definite.the_uniq_presup_iff_iota {m : Montague.Model} (domain : List m.Entity) (restrictor : m.interpTy Montague.Ty.et) :
          (match List.filter restrictor domain with | [head] => true | x => false) = (Composition.TypeShifting.iota domain restrictor).isSome

          The uniqueness presupposition holds iff Partee's ι succeeds.

          iota domain P = some e exactly when the uniqueness presupposition of the_uniq is satisfied. The ι-operator is the presupposition-free core of the uniqueness-based definite.

          source
          theorem Semantics.Lexical.Determiner.Definite.the_is_every_on_singletons (m : Montague.Model) [Fintype m.Entity] (restrictor scope : m.Entity → Bool) (e : m.Entity) (h_restr : restrictor e = true) (h_unique : ∀ (x : m.Entity), restrictor x = true → x = e) :
          Quantifier.every_sem m restrictor scope = scope e

          ⟦the⟧ agrees with ⟦every⟧ when the restrictor is a singleton.

          When exactly one entity satisfies the restrictor, "the φ is ψ" and "every φ is ψ" have the same truth value. This is the classical observation that the definite article is a universal quantifier restricted to singletons.

          source
          def Semantics.Lexical.Determiner.Definite.qforceToPresupType :
          Fragments.English.Determiners.QForce → Option Core.Definiteness.DefPresupType

          English "the" is QForce.definite — our semantics provides its denotation.

          The lexical entry in Fragments/English/Determiners.lean records the as QForce.definite. Our the_uniq provides the compositional semantics that was previously missing: the denotes a presuppositional determiner that presupposes existence+uniqueness and asserts the scope.

          Since English has only one article form (ArticleType.weakOnly), the default semantics is uniqueness-based. The familiarity reading arises pragmatically (accommodation) rather than structurally.

          Equations
          Instances For
            source
            theorem Semantics.Lexical.Determiner.Definite.definite_is_uniqueness :
            qforceToPresupType Fragments.English.Determiners.QForce.definite = some Core.Definiteness.DefPresupType.uniqueness

            QForce.definite maps to uniqueness by default.

            source
            def Semantics.Lexical.Determiner.Definite.qforceToDefiniteness :
            Fragments.English.Determiners.QForce → Core.Definiteness.Definiteness

            Map QForce to Definiteness.

            Equations
            Instances For
              source
              def Semantics.Lexical.Determiner.Definite.modifierNecessary {E : Type} (domain : List E) (restrictor modifier : E → Bool) :
              Bool

              A modifier is referentially necessary in a domain when the bare restrictor fails to uniquely identify a referent but the modified (intersected) restrictor succeeds.

              This captures the shared mechanism underlying:

              • Contrastive inference (@cite{sedivy-etal-1999}): a scalar adjective is informative when a same-category competitor is present
              • Context-sensitive attachment (@cite{paape-vasishth-2026}): an RC modifier is pragmatically licensed when multiple potential referents make the bare definite ambiguous

              In both cases, the modifier rescues a failed uniqueness presupposition.

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