NP Type-Shifting Principles #
@cite{partee-1987}
Three NP semantic types and six type-shifting operations (three inverse pairs):
lift / lower : e ↔ ⟨⟨e,t⟩,t⟩ (total / partial)
ident / iota : e ↔ ⟨e,t⟩ (formal; total / partial)
pred / nom : e ↔ ⟨e,t⟩ (substantive; Chierchia's ∪/∩)
A / BE : ⟨e,t⟩ ↔ ⟨⟨e,t⟩,t⟩ (total / total)
THE : ⟨e,t⟩ → ⟨⟨e,t⟩,t⟩ (partial; presuppositional)
In the finite extensional setting, pred = ident and nom = iota. The
conceptual difference: ident/iota are formal (pure combinatorics),
while pred/nom are substantive (depend on entity-property correspondence).
The intensional generalizations are Chierchia's ∪ (up) and ∩ (down) operators
in Semantics.Lexical.Noun.Kind.Chierchia1998.
Type-raising: lift(j) = λP. P(j)
Equations
Instances For
Singleton property: ident(j) = λx. [j = x].
Uses j = x order for definitional equality with BE(lift(j)).
Equations
- Semantics.Composition.TypeShifting.ident j x = decide (j = x)
Instances For
Predicative content of a GQ: BE(Q) = λx. Q(λy. y = x)
Equations
- Semantics.Composition.TypeShifting.BE Q x = Q fun (y : m.interpTy Semantics.Montague.Ty.e) => decide (y = x)
Instances For
Predicativize: extensional counterpart of Chierchia's ∪ (up) operator.
In the finite extensional setting, pred coincides with ident:
both map an entity to its singleton property λx. [j = x].
Conceptually distinct (@cite{partee-1987} Figure 1):
identis formal — pure combinatorics, always defined.predis substantive — applies to entity-correlates of properties and returns the corresponding property.
The intensional generalization is Semantics.Lexical.Noun.Kind.Chierchia1998.up.
Instances For
BE is a BoundedLatticeHom (Partee §3.3, Fact 1).
Equations
- Semantics.Composition.TypeShifting.BE_hom m = { toFun := Semantics.Composition.TypeShifting.BE, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }
Instances For
Fact 2 (@cite{partee-1987} §3.3): BE is the unique
BoundedLatticeHom from ⟨⟨e,t⟩,t⟩ to ⟨e,t⟩ that makes
Figure 3 commute (i.e., satisfies f(lift(j)) = ident(j)).
Proof (@cite{keenan-faltz-1985}): For each entity x, construct the
atom atom_x = ⨅_j literal(j) where literal(j) = lift(j) if j = x
and (lift(j))ᶜ otherwise. This atom is the indicator of {P_x} where
P_x = λy. [y = x]. Since f preserves ⊓ and complements, f maps
atom_x correctly. Then monotonicity determines f(Q)(x) for arbitrary
Q by cases on Q(P_x).
BE(Q₁ ∧ Q₂) = BE(Q₁) ∧ BE(Q₂)
BE(Q₁ ∨ Q₂) = BE(Q₁) ∨ BE(Q₂)
BE(¬Q) = ¬BE(Q)
Partial inverse of lift. Defined when Q is a principal ultrafilter.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Partial inverse of ident. Returns the unique satisfier of P.
Equations
- Semantics.Composition.TypeShifting.iota domain P = match List.filter (fun (x : m.interpTy Semantics.Montague.Ty.e) => P x) domain with | [j] => some j | x => none
Instances For
NOM: Nominalization (@cite{partee-1987} Figure 1, @cite{chierchia-1984}).
Maps a property to its individual correlate: ⟨e,t⟩ → e (partial).
In the finite extensional setting, NOM = iota (returns the unique
satisfier of P, if singleton). The intensional generalization is
Semantics.Lexical.Noun.Kind.Chierchia1998.down (Chierchia's ∩).
Equations
- Semantics.Composition.TypeShifting.NOM domain P = Semantics.Composition.TypeShifting.iota domain P
Instances For
Existential closure: A(P) = λQ. ∃x. P(x) ∧ Q(x)
Equations
- Semantics.Composition.TypeShifting.A domain P Q = domain.any fun (x : m.Entity) => P x && Q x
Instances For
THE: Presuppositional type-shifter for definites (@cite{partee-1987} Figure 1).
THE(P) = lift(iota(P)) when iota(P) is defined (P has a unique satisfier).
Maps ⟨e,t⟩ → ⟨⟨e,t⟩,t⟩ (partial). Unlike A (which is total), THE
presupposes existence and uniqueness. Connects to the semantics of "the"
in Semantics.Lexical.Determiner.Definite.
Equations
Instances For
lower ∘ lift = some on the domain (Partee's round-trip).
Requires j ∈ domain (j must be in the model) and domain.Nodup
(no duplicates, ensuring unique filter result).
iota ∘ ident = some on the domain (Partee's round-trip).
The ident predicate picks out exactly j, so iota returns j
when j is the unique satisfier (guaranteed by Nodup).
THE ∘ ident = some ∘ lift on the domain.
When ident(j) has a unique satisfier (always, given Nodup),
THE shifts it to the corresponding principal ultrafilter.
lift = Conjunction.typeRaise
Coherence of the three readings of "the king" (@cite{partee-1987} §3.2).
When iota succeeds, the e, ⟨e,t⟩, and ⟨⟨e,t⟩,t⟩ readings are
related by BE(lift(j)) = ident(j) (Figure 2 commutativity).
Truth-Conditional Transparency of Type-Shifts #
A type-shift is truth-conditionally transparent when the shifted meaning produces the same sentential truth value as the original. The precise condition:
Theorem: For a GQ Q : ⟨⟨α,t⟩,t⟩, the round-trip A(BE(Q)) preserves
truth conditions iff Q is a principal ultrafilter (i.e., Q = lift(j)
for some individual j).
For non-principal GQs (quantifiers, degree quantifiers like numerals),
A(BE(Q)) yields a strictly weaker meaning. This is precisely when
the RSA model should include both the original and shifted meanings as
alternative interpretations.
Applications:
- Proper names:
Q = lift(john)→A(BE(Q)) = Q→ no ambiguity - Numerals:
Q = ⟦three⟧→A(BE(Q)) = ∃d[d=3 ∧ D(d)]≠Q→ ambiguity - Universal quantifiers:
Q = ⟦every student⟧→A(BE(Q)) = ⟦some student⟧≠Q
A GQ is a principal ultrafilter iff it equals lift(j) for some entity.
Equations
- Semantics.Composition.TypeShifting.isPrincipalUltrafilter domain Q = ∃ j ∈ domain, Q = Semantics.Composition.TypeShifting.lift j
Instances For
Round-trip preservation for principal ultrafilters.
For Q = lift(j), A(BE(Q))(P) = Q(P) for all P.
This means type-shifting is truth-conditionally transparent for
proper names, pronouns, definites — any expression that denotes
a principal ultrafilter.
BE ∘ A = id on properties (@cite{partee-1987} §3.3).
For any property P, BE(A(P)) = P. This makes A a right inverse
of BE: existential closure followed by predicative content recovers
the original property.
This is the key result establishing A as a "natural" type-shifting
functor — it is an inverse of BE, and Partee argues it (together with
some) is the most natural DET-type functor.
Proof: BE(A(P))(x) = A(P)(λy. y=x) = ∃z∈dom. P(z) ∧ (z=x) = P(x).
The decide(z=x) selects exactly z = x, collapsing the existential.
For non-principal GQs, the round-trip changes truth conditions.
every(⊤) = true but A(BE(every))(⊤) = false — the round-trip
collapses universal quantification to ⊥ on multi-element domains.
(BE(every) asks "which entity equals all entities?" — none do.)
The Full Commutativity Diagram #
Partee's type-shifting triangle connects three NP semantic types via six operations (three inverse pairs). The triangle commutes: any two paths between the same pair of types yield the same result.
e
╱ ╲
ident╱ ╲lift
╱ ╲
↓ ↓
⟨e,t⟩ ⇄ ⟨⟨e,t⟩,t⟩
A →
← BE
Commutativity (two faces):
BE ∘ lift = ident(right face,BE_lift_eq_ident)A ∘ ident = lift(left face,A_ident_eq_lift)
Retraction: BE ∘ A = id on ⟨e,t⟩ (BE_A_id) — A is a section of BE.
Consequence: All composite paths agree. The triangle is a commutative
diagram in Set, with A and BE witnessing that the two embeddings
ident : e → ⟨e,t⟩ and lift : e → ⟨⟨e,t⟩,t⟩ are "the same map" up to
the A/BE retraction on their codomains.
Left face of the triangle: A ∘ ident = lift.
A(ident(j))(P) = ∃x∈dom. [j=x] ∧ P(x) = P(j) = lift(j)(P).
Together with BE_lift_eq_ident (right face), this establishes
full commutativity of the type-shifting triangle.
Full cycle e →lift ⟨⟨e,t⟩,t⟩ →BE ⟨e,t⟩ →A ⟨⟨e,t⟩,t⟩ = lift.
Going around the triangle through GQ-space returns to the same GQ.
Full cycle e →ident ⟨e,t⟩ →A ⟨⟨e,t⟩,t⟩ →BE ⟨e,t⟩ = ident.
Going around the triangle through predicate-space returns to the same predicate.
Partial path e →lift ⟨⟨e,t⟩,t⟩ →BE ⟨e,t⟩ →iota e = some.
The indirect route through GQ-space recovers the entity.
Partial path e →ident ⟨e,t⟩ →A ⟨⟨e,t⟩,t⟩ →lower e = some.
The indirect route through predicate-space recovers the entity.
THE respects the triangle: THE ∘ BE ∘ lift = some ∘ lift.
Recovering the definite description from a type-raised proper name via BE, then THE, yields the original type-raised individual.
BE is a left inverse of A: the section/retraction structure of the
type-shifting triangle, expressed using Function.LeftInverse.
This connects to Mathlib's function infrastructure, giving us
Surjective BE and Injective (A domain) for free.
BE is surjective: every predicate is the predicative content of some GQ.
Derived from Function.LeftInverse.surjective.
A is injective: distinct predicates yield distinct GQs under
existential closure. Linguistically: different common nouns mean
different things as indefinites.
Derived from Function.LeftInverse.injective.
The A/BE Adjunction on Monotone GQs #
@cite{barwise-cooper-1981} observed that natural language determiners
denote upward-closed (monotone) generalized quantifiers: if Q(P) and
P ⊆ P', then Q(P'). This constraint is exactly what makes A and BE
form a GaloisCoinsertion — an adjunction where the upper adjoint (BE)
retracts the lower adjoint (A).
On the full Boolean algebra of all GQs, A ⊣ BE fails: for non-monotone Q
(e.g., λR. ¬R(a)), A(BE(Q)) ≤ Q does not hold. But restricted to the
sublattice of monotone GQs, the key inequality A(BE(Q)) ≤ Q holds because
singleton predicates {x} ≤ R whenever R(x), and monotonicity of Q
lifts this to Q({x}) ≤ Q(R).
The GaloisCoinsertion gives us, via Mathlib:
GaloisConnection:A(P) ≤ Q ↔ P ≤ BE(Q)for monotone QBE_upis surjective onUpwardGQandA_upis injectiveA_upis strictly monotone
Upward-closed (monotone) generalized quantifiers — the @cite{barwise-cooper-1981} constraint on natural language determiners.
Q is upward-closed when Q(P) and P ≤ P' imply Q(P').
Equivalently, Monotone Q in the pointwise order on ⟨e,t⟩.
Equations
Instances For
A(P) is always upward-closed: if ∃x∈dom with P(x) ∧ R(x),
and R ≤ R', then ∃x∈dom with P(x) ∧ R'(x).
Lift A to the UpwardGQ subtype.
Equations
- Semantics.Composition.TypeShifting.A_up domain P = ⟨Semantics.Composition.TypeShifting.A domain P, ⋯⟩
Instances For
Project BE from the UpwardGQ subtype.
Instances For
A is monotone as a map from predicates to GQs.
Key inequality: A(BE(Q)) ≤ Q for upward-closed Q.
A(BE(Q))(R) = ∃x∈dom. Q({x}) ∧ R(x). When R(x) holds,
{x} ≤ R in the pointwise order. By monotonicity of Q,
Q({x}) ≤ Q(R), establishing the inequality.
This is precisely the condition that fails for non-monotone Q
(e.g., Q = λR. ¬R(a) where Q({a}) = false but Q(∅) = true).
Galois coinsertion: A (existential closure) and BE (predicative
content) form a GaloisCoinsertion on the sublattice of upward-closed GQs.
This is the order-theoretic content of Partee's type-shifting triangle:
Linguistically: @cite{barwise-cooper-1981}'s constraint that natural language determiners denote monotone GQs is exactly the condition under which the A/BE pair forms an adjunction.
Equations
- Semantics.Composition.TypeShifting.galoisCoinsertion domain hcomplete = GaloisCoinsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯
Instances For
The Galois connection: A(P) ≤ Q ↔ P ≤ BE(Q) for monotone Q.
CARD: number → cardinality predicate (@cite{snyder-2026}, (6a)). CARD = λn.λx. μ(x) = n. Turns a number into a predicate on entities that have exactly n atomic parts.
Equations
- Semantics.Composition.TypeShifting.CARD μ n x = decide (μ x = n)
Instances For
PM: Predicate Modification (@cite{heim-kratzer-1998}, (7a)). PM = λP.λQ.λx. P(x) ∧ Q(x). Intersective modifier.
Equations
- Semantics.Composition.TypeShifting.PM P Q x = (P x && Q x)
Instances For
NOM(pred(j)) = some j: nominalizing the predicativization of an entity
returns that entity. The extensional counterpart of Chierchia's ∩(∪k) = k
(Semantics.Lexical.Noun.Kind.Chierchia1998.down_up_id).