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 pred/nom pair originates in @cite{chierchia-1984}'s nominalization
operator ^ from HST* (Cocchiarella's property theory), applied to infinitival
and gerundive complements. The intensional generalizations are Chierchia's
∪ (up) and ∩ (down) operators in Semantics.Kinds.NMP,
which extend the same type-shift to kinds and bare plurals.
Type-raising: lift(j) = λP. P(j)
Equations
- Semantics.Composition.TypeShifting.lift j P = P j
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 = (j = x)
Instances For
Propositional analogue of ident: propIdent(p) = λq. [p = q],
i.e. the singleton question {p} from a proposition p.
This is ID of @cite{elliott-etal-2017} (their eq. 10), used to coerce a
proposition into a question denotation when an embedding predicate (e.g.
a Predicate of Relevance like care) selects only for questions. The shape
mirrors ident one type-theoretic level up: entities ↦ singleton properties
becomes propositions ↦ singleton questions.
Equations
- Semantics.Composition.TypeShifting.propIdent p q = (p = q)
Instances For
Predicative content of a GQ: BE(Q) = λx. Q(λy. y = x)
Equations
- Semantics.Composition.TypeShifting.BE Q x = Q fun (y : F.Denot Core.Logic.Intensional.Ty.e) => 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.Kinds.NMP.up.
Instances For
Equations
- Semantics.Composition.TypeShifting.instBooleanAlgebraDenotT F = inferInstance
Equations
- Semantics.Composition.TypeShifting.instBooleanAlgebraDenotEt F = inferInstance
Equations
- Semantics.Composition.TypeShifting.instBooleanAlgebraDenotEtt F = inferInstance
BE is a BoundedLatticeHom (Partee §3.3, Fact 1).
Equations
- Semantics.Composition.TypeShifting.BE_hom F = { 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 : F.Denot Core.Logic.Intensional.Ty.e) => decide (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.Kinds.NMP.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 = ∃ x ∈ domain, 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.Definiteness.
Equations
- Semantics.Composition.TypeShifting.THE domain P = Option.map Semantics.Composition.TypeShifting.lift (Semantics.Composition.TypeShifting.iota domain P)
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:
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
- Semantics.Composition.TypeShifting.UpwardGQ F = { Q : F.Denot Core.Logic.Intensional.Ty.ett // Monotone Q }
Instances For
Equations
- Semantics.Composition.TypeShifting.instPartialOrderUpwardGQ = Subtype.partialOrder fun (Q : F.Denot Core.Logic.Intensional.Ty.ett) => Monotone Q
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 = (μ 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.Kinds.NMP.down_up_id).
Property vs. Proposition: Complement Denotation Types #
@cite{chierchia-1984} argues that infinitival and gerundive complements
denote properties (type ⟨e,t⟩), not propositions (type ⟨s,t⟩). This
is the original linguistic motivation for the pred/nom operators in
@cite{partee-1987}'s type-shifting triangle.
The key insight: pred and nom mediate between the individual
correlate of a property (an entity of type e that "is" the property)
and the property itself (type ⟨e,t⟩). This is exactly what infinitival
complements need: "to run" denotes a property, but it can be nominalized
("running is fun") to denote the individual correlate of that property.
The intensional generalization of this idea appears in @cite{chierchia-1998} as ∩ (down) and ∪ (up), applied to kinds rather than infinitives. Both applications share the same underlying type-shift: there is a systematic correspondence between properties and their individual correlates in the domain.
Complement denotation layer: whether a complement denotes a property (⟨e,t⟩, open predicate) or a proposition (t / ⟨s,t⟩, closed).
@cite{chierchia-1984} Ch I: the infinitive/gerund vs. finite clause
distinction corresponds to this type distinction. Nominalization
(NOM/nom) and control both require the property layer — control
needs an unsaturated individual argument to bind, and nominalization
maps ⟨e,t⟩ → e. Propositions must go through existential closure
(A) to reach the GQ layer.
The extensional pred/nom pair, their intensional generalization
as ∩/∪ in @cite{chierchia-1998}, and the Control Principle in
@cite{chierchia-1984} Ch IV all operate on the property layer.
- property : ComplSemLayer
- proposition : ComplSemLayer
Propositional layer: t (or ⟨s,t⟩ intensionally). Finite indicative and subjunctive complements.
Instances For
Equations
- Semantics.Composition.TypeShifting.instDecidableEqComplSemLayer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Property-type complements support nominalization (⟨e,t⟩ → e via NOM)
and control (the unsaturated argument position can be bound).
This unifies @cite{chierchia-1984}'s two central claims: control and nominalization are both consequences of the property/proposition type distinction.