Docs / Semantics / Composition / Extensional

Extensional operators

import Linglib.Semantics.Composition.Extensional · namespace Montague

An operator on intensions is extensional at an index when its value there depends only on its argument's extension there: negation is extensional, necessity is not, and among adjectives gray is and skillful is not. An operator is extensional exactly when it is a function on extensions applied index by index, and at an index where it is extensional it cannot tell a variable it binds from one fixed there. Necessity is extensional only at a world that accesses no world but itself.

Main definitions

Montague.IsExtensionalAt O w: the value of O at w depends only on the extension of its argument at w.
Montague.IsExtensional O: O is extensional at every index.

Implementation notes

Extensionality at w is the statement that O · w factors through evaluation at w, and that it depends, in the sense of mathlib's DependsOn, on the coordinate w alone. Kamp's condition for an extensional adjective takes a single function on extensions for every index; the function here may vary with the index, as in his gloss of the condition and as his claim that every predicative adjective is extensional requires.

References

Kamp 1975, Two theories about adjectives formalized
Zimmermann 2026, African Lambdas I: Formal Semantics of African Languages—The Nominal Domain formalized

Declarations

O is extensional at w when its value at w depends on its argument only through the argument's extension at w.

def IsExtensionalAt L46–49

{W : Type u_1} {α : Type u_2} {β : Type u_3} (O : (W → α) → W → β) (w : W) :

Prop

IsExtensionalAt O w = ∀ ⦃p q : W → α⦄, p w = q w → O p w = O q w

Used by IsExtensional, isExtensionalAt_iff_factorsThrough, isExtensionalAt_iff_dependsOn, not_isExtensionalAt_iff, isExtensionalAt_iff_forall_const, isExtensionalAt_iff_exists, isExtensionalAt_iff_forall_diag, isExtensionalAt_box_iff, isExtensionalAt_id, isExtensionalAt_const, isExtensionalAt_not, IsExtensionalAt.comp, IsExtensionalAt.comp_left, IsExtensionalAt.comp₂, IsExtensionalAt.not, IsExtensionalAt.and, IsExtensionalAt.or

Used in Semantics/Composition/Mode, Semantics/Reference/Rigidity, HeimKratzer1998, Zimmermann2026

O is extensional when it is extensional at every index.

def IsExtensional L51–53

{W : Type u_1} {α : Type u_2} {β : Type u_3} (O : (W → α) → W → β) :

Prop

IsExtensional O = ∀ (w : W), IsExtensionalAt O w

Built from

Used by isExtensional_iff_exists_eq_piMap, isExtensional_piMap

Used in Semantics/Modification/Classification, Kamp1975

An operator is extensional exactly when it applies a function on extensions at each index.

theorem isExtensional_iff_exists_eq_piMap L76–79

{W : Type u_1} {α : Type u_2} {β : Type u_3} {O : (W → α) → W → β} :

IsExtensional O ↔ ∃ (f : W → α → β), O = Pi.map f

Built from

L81–82

An operator is extensional at w exactly when it does not distinguish an argument whose index it binds, fun v ↦ g v v, from the same argument with the index fixed at w, g w.

theorem isExtensionalAt_iff_forall_diag L84–88