Documentation

Linglib.Phenomena.Copulas.Studies.Elbourne2026

Elbourne (2026): Adjectives without syntactic categories #

@cite{elbourne-2026}

Published online: 12 March 2026, Natural Language & Linguistic Theory 44:17.

Adjectives are uniformly type ⟨et,et⟩ — functions from noun denotations to noun denotations. This eliminates Predicate Modification for adjective-noun combination (FA suffices) and supports the program of eliminating syntactic categories in favor of semantic types ("Meaning-Dependent Grammar", building on @cite{elbourne-2024}).

Key result #

Classification.lean already defines AdjMeaning W E = Property W E → Property W E, which IS the ⟨et,et⟩ type. The Kamp hierarchy there (intersective, subsective, privative) classifies adjectives by meaning postulates within that type — not by assigning different types to different classes. The present file makes this explicit and adds Elbourne's copula semantics.

Copula BE #

Elbourne's copula takes a tense relation R and an ⟨et,et⟩ adjective G, applies G to the trivially true noun λt.λx. ⊤, and existentially quantifies over a time satisfying R. This contrasts with @cite{partee-1987}'s BE (a type-shifting operation ⟨⟨e,t⟩,t⟩ → ⟨e,t⟩ for nominal predication) — a different function for a different construction.

Sections #

  1. ⟨et,et⟩ adjective meanings (intersective)
  2. Copula BE
  3. FA-sufficiency: FA on ⟨et,et⟩ = PM on ⟨e,t⟩; PM limitation
  4. "Fido was cute" derivation
  5. Connection to Classification hierarchy
  6. Former: non-subsective AdjMeaning + PM failure + end-to-end chain
  7. Compulsory E_R: attributive-only adjectives

The trivially true noun meaning: λt.λx. ⊤. The copula applies an ⟨et,et⟩ adjective to this to extract the adjective's inherent content.

Equations
Instances For

    Intersective ⟨et,et⟩ adjective: λN.λt.λx. N(t)(x) ∧ Q(t)(x).

    @cite{elbourne-2026} (24b)/(59): /cute/ :: λf⟨e,it⟩.λx.λt. f(x)(t) & cute(x)(t)

    Equations
    Instances For

      Applying an intersective adjective to the trivial noun recovers the underlying property Q. This is what the copula exploits.

      Elbourne's copula BE.

      Takes a tense relation R and an ⟨et,et⟩ adjective G, applies G to the trivial noun, and existentially quantifies over a time satisfying R.

      @cite{elbourne-2026} (8)/(27c): BE :: λR⟨i,it⟩.λG⟨eit,eit⟩.λx.λt. ∃t'(R(t')(t) & G(λy.λt''.⊤)(x)(t'))

      Equations
      Instances For
        theorem Phenomena.Copulas.Studies.Elbourne2026.copulaBE_intersective {I : Type u_1} {E : Type u_2} (Q : Semantics.Lexical.Adjective.Classification.Property I E) (R : IIProp) (x : E) (t : I) :
        copulaBE R (intersective Q) x t (t' : I), R t' t Q t' x = true

        BE applied to an intersective adjective produces the expected truth conditions: ∃t'. R(t',t) ∧ Q(t')(x).

        theorem Phenomena.Copulas.Studies.Elbourne2026.fa_eq_pm {I : Type u_1} {E : Type u_2} (Q N : Semantics.Lexical.Adjective.Classification.Property I E) :
        intersective Q N = fun (t : I) (x : E) => Q t x && N t x

        Core theorem: FA on ⟨et,et⟩ adjective = PM on ⟨e,t⟩ property.

        The LHS is the FA attributive derivation: an intersective ⟨et,et⟩ adjective applied to a noun via function application. The RHS is Predicate Modification: conjunction of the underlying adjective property with the noun. Since FA reproduces PM for intersective adjectives, PM is unnecessary for adjective-noun combination.

        @cite{elbourne-2026} (25)–(26): ⟦cute donkey⟧ = λx.λt. donkey(x)(t) & cute(x)(t)

        PM always produces intersective results: the composition λN.λt.λx. A(t)(x) ∧ N(t)(x) satisfies Classification.isIntersective with witness A. This means PM is too restrictive even for merely subsective adjectives like skillful — not just non-subsective ones.

        @cite{elbourne-2026} (p. 13): under ⟨e,t⟩, "a rule like Predicate Modification is presumably necessary; but this would impose the intersective semantics that we have just seen is inappropriate for merely subsective adjectives."

        theorem Phenomena.Copulas.Studies.Elbourne2026.pm_always_subsective {I : Type u_1} {E : Type u_2} (A N : Semantics.Lexical.Adjective.Classification.Property I E) (t : I) (x : E) (h : (A t x && N t x) = true) :
        N t x = true

        Corollary: PM always yields subsective results (A ∧ N entails N). Follows from pm_always_intersective via the hierarchy (intersective → subsective), but also provable directly.

        theorem Phenomena.Copulas.Studies.Elbourne2026.fido_was_cute {I : Type u_1} {E : Type u_2} (Q : Semantics.Lexical.Adjective.Classification.Property I E) (lt : IIProp) (fido : E) (t : I) :
        copulaBE lt (intersective Q) fido t (t' : I), lt t' t Q t' fido = true

        Truth conditions for "Fido was cute": ∃t'(t' < t ∧ cute(Fido)(t')).

        Step-by-step derivation (@cite{elbourne-2026} (28)–(30)):

        1. ⟦BE PAST⟧ = λG.λx.λt. ∃t'(t' < t ∧ G(⊤)(x)(t'))
        2. ⟦[BE PAST] cute⟧ = λx.λt. ∃t'(t' < t ∧ cute(x)(t'))
        3. ⟦Fido [[BE PAST] cute]⟧ = λt. ∃t'(t' < t ∧ cute(Fido)(t'))

        Intersective ⟨et,et⟩ adjectives satisfy Classification.isIntersective. The witness is the underlying property Q.

        theorem Phenomena.Copulas.Studies.Elbourne2026.attributive_predicative_same_denotation {I : Type u_1} {E : Type u_2} (Q noun : Semantics.Lexical.Adjective.Classification.Property I E) :
        have attr := intersective Q noun; have pred := intersective Q trivialNoun; pred = Q attr = fun (t : I) (x : E) => noun t x && Q t x

        Attributive combination (FA on ⟨et,et⟩ adj + noun) and predicative extraction (copula applies adj to trivial noun) use the SAME adjective denotation. The copula adds tense; FA does not.

        "cute donkey" (attributive) = intersective Q donkey "Fido was cute" (predicative) uses intersective Q applied to

        The adjective meaning intersective Q is identical in both.

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

        Non-subsective ⟨et,et⟩ adjective: former. Computable over a finite list of time points via List.any.

        formerAdj times ltb N t x = true iff some earlier time t' satisfies ltb t' t ∧ N t' x and N t x = false.

        @cite{elbourne-2026} (44)/(60): λf⟨e,it⟩.λx.λt. ∃t'(< (t')(t) & f(x)(t') & ¬f(x)(t))

        Equations
        Instances For

          formerAdj is not subsective — connecting directly to Classification.isSubsective. This is a genuine AdjMeaning, so it integrates with the full Classification hierarchy.

          End-to-end chain: the ⟨et,et⟩ theory strictly subsumes ⟨e,t⟩ + PM for adjective-noun composition.

          1. For intersective adjectives, FA on ⟨et,et⟩ reproduces PM (fa_eq_pm).
          2. For non-subsective adjectives, ⟨et,et⟩ succeeds (former_adj_holdsjudge .now .joe = false).
          3. For non-subsective adjectives, ⟨e,t⟩ + PM fails (pm_cannot_produce_former).
          theorem Phenomena.Copulas.Studies.Elbourne2026.formerAdj_trivialNoun {I : Type u_1} {E : Type u_2} (times : List I) (ltb : IIBool) (t : I) (x : E) :

          Applying formerAdj to the trivial noun gives false everywhere: can never "formerly" hold (it always holds). The copula applies adjectives to , so former in predicative position would be vacuously false — a semantic reason for the attributive-only restriction (complementing compulsory E_R in § 7).

          Whether an adjective requires a noun argument (E_R feature status).

          Under the ⟨et,et⟩ theory ALL adjectives are the same type; the attributive/predicative distinction is syntactic, not semantic.

          • Optional E_R (cute, tall): attributive or predicative.
          • Compulsory E_R (former, mere, alleged): attributive only.

          @cite{elbourne-2026} § 3.2: the copula derivation requires the adjective to appear WITHOUT an E_R feature; adjectives bearing compulsory E_R cannot be taken as argument by [BE PAST].

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