NP Type-Shifting Principles #
Three NP semantic types and six type-shifting operations (three inverse pairs):
individual / lower : e ↔ ⟨⟨e,t⟩,t⟩ (total / partial)
ident / iota : e ↔ ⟨e,t⟩ (formal; total / partial)
pred / nom : e ↔ ⟨e,t⟩ (substantive; Chierchia's ∪ and ∩)
A / BE : ⟨e,t⟩ ↔ ⟨⟨e,t⟩,t⟩ (total / total)
THE : ⟨e,t⟩ → ⟨⟨e,t⟩,t⟩ (partial; presuppositional)
The two quantifier-side operations A and BE, and the Montague lift
Quantification.individual, are the quantifier API and live in
Semantics.Quantification.Quantifier; this file holds the entity-side shifts
and the commuting triangle relating all three types.
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 [Chi84]'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.
Singleton property: ident(j) = λx. [j = x].
Uses j = x order for definitional equality with BE(individual 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 [EKSU17] (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
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 ([Par87] 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
BE ∘ individual = ident (Figure 3 commutativity).
Fact 2 ([Par87] §3.3): BE is the unique
BoundedLatticeHom from ⟨⟨e,t⟩,t⟩ to ⟨e,t⟩ that makes
Figure 3 commute (i.e., satisfies f(individual j) = ident(j)).
Proof ([KF85]): For each entity x, construct the
atom atom_x = ⨅_j literal(j) where literal(j) = individual j if j = x
and (individual 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).
Partial inverse of individual. Defined when Q is a principal
ultrafilter.
Equations
- Semantics.Composition.TypeShifting.lower domain Q = match List.filter (fun (j : E) => decide (Q fun (x : E) => x = j)) domain with | [j] => some j | x => none
Instances For
Partial inverse of ident. Returns the unique satisfier of P.
Equations
- Semantics.Composition.TypeShifting.iota domain P = match List.filter (fun (x : E) => decide (P x)) domain with | [j] => some j | x => none
Instances For
NOM: Nominalization ([Par87] Figure 1, [Chi84]).
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
THE: Presuppositional type-shifter for definites ([Par87] Figure 1).
THE(P) = individual(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 Quantification.individual (Semantics.Composition.TypeShifting.iota domain P)
Instances For
lower ∘ individual = 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 ∘ individual on the domain.
When ident(j) has a unique satisfier (always, given Nodup),
THE shifts it to the corresponding principal ultrafilter.
Coherence of the three readings of "the king" ([Par87] §3.2).
When iota succeeds, the e, ⟨e,t⟩, and ⟨⟨e,t⟩,t⟩ readings are
related by BE(individual j) = ident(j) (Figure 2 commutativity).
The type-shifting triangle ([Par87] Figure 3) #
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╱ ╲individual
╱ ╲
↓ ↓
⟨e,t⟩ ⇄ ⟨⟨e,t⟩,t⟩
A →
← BE
Commutativity (two faces):
BE ∘ individual = ident(right face,BE_individual_eq_ident)A ∘ ident = individual(left face,A_ident_eq_individual)
Retraction: A is a section of BE — BE ∘ A = id on ⟨e,t⟩
(Quantification.BE_A_id).
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 individual : e → ⟨⟨e,t⟩,t⟩ are "the same map" up to
the A/BE retraction on their codomains.
Left face of the triangle: A ∘ ident = individual.
A(ident(j))(P) = ∃x∈dom. [j=x] ∧ P(x) = P(j) = individual(j)(P).
Together with BE_individual_eq_ident (right face), this establishes
full commutativity of the type-shifting triangle.
Full cycle e →individual ⟨⟨e,t⟩,t⟩ →BE ⟨e,t⟩ →A ⟨⟨e,t⟩,t⟩ = individual.
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 →individual ⟨⟨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 ∘ individual = some ∘ individual.
Recovering the definite description from a type-raised proper name via BE, then THE, yields the original type-raised individual.
CARD: number → cardinality predicate ([Sny26], (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 ([HK98], (7a)).
PM = λP.λQ.λx. P(x) ∧ Q(x): Modifier.intersective at e ⇒ t.
Equations
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).
Complement denotation types ([Chi84]) #
[Chi84] 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
[Par87]'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 [Chi98] 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).
[Chi84] 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 [Chi98], and the Control Principle in
[Chi84] Ch IV all operate on the property layer.
- property : ComplementDenotation
- proposition : ComplementDenotation
Propositional layer: t (or ⟨s,t⟩ intensionally). Finite indicative and subjunctive complements.
Instances For
Equations
- Semantics.Composition.TypeShifting.instDecidableEqComplementDenotation 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
The semantic layer of a clausal complement type, derived from the two
Features observables: clausal and finite → proposition, clausal and
nonfinite → property ([Chi84]), none for non-clausal
complements.
Equations
- One or more equations did not get rendered due to their size.