Partee (1987): Noun Phrase Interpretation and Type-shifting Principles #

This file formalizes the type-shifting principles of [Par87]. A noun phrase may denote an entity, a predicate, or a generalized quantifier as its environment demands, and the mappings between the three types come in inverse pairs, the paper's Figure 1: lift, the substrate's Quantifier.NP.individual, and lower, the total injection of an entity into its principal ultrafilter and its partial inverse; ident and iota, the singleton property of an entity and the unique member of a property; and nom and pred, the correlates of properties and entities after [Chi84] (lower_lift, Reference.iota_ident). The definite article has a partial entity meaning, iota, and a total quantifier meaning, THE, which is the determiner GQ.the. Whenever iota(king') is defined THE(king') is its lift, and otherwise the empty set of properties, so lower(THE(king')) = iota(king') either way. The predicative reading of the king is BE(THE(king')), the singleton of the unique king, which is ident(iota(king')) when the latter is defined and coincides with the common noun when there is at most one king; this is why the article can be dropped in John is (the) president (the_eq_individual, lower_the, BE_the_eq_ident, BE_the_eq_self).

The functor BE, Montague's translation of be reconceived as a type shifter, is a homomorphism of the Boolean structures, Fact 1, which the substrate builds into NP.BE, and the unique homomorphism making Figure 3 commute, BE(lift(j)) = ident(j), Fact 2 (BE_natural). The indefinite article A is GQ.some, natural as an inverse of BE (NP.BE_some), so be a man comes out as man, and be no man as the complement of be a man (BE_no), while be every man holds only of the only man (BE_every_apply). English be itself is then predicate application, the predicative reading having moved into the noun phrase.

Implementation notes #

The setting is extensional, so pred is ident and nom and iota are both the Russellian Reference.iota.
Fact 2 is read with complete homomorphisms, the homomorphisms of [KF85]'s result that the individuals generate the quantifiers, which the paper invokes for it; on an infinite domain a merely Boolean homomorphism need not preserve the infinite meets the argument uses.
The mappings to and from kinds of §3.4 onward and the analysis of the Williams counterexample are not formalized.

References #

source

noncomputable def Partee1987.lower {E : Type u_1} (Q : Quantifier.NP E) :

Option E

lower Q is the entity whose Montague lift is Q, when Q is a principal ultrafilter.

Equations

Partee1987.lower Q = Reference.iota fun (j : E) => Q = Quantifier.NP.individual j

Instances For

Figure 1: three inverse pairs #

source

theorem Partee1987.lower_lift {E : Type u_1} (j : E) :

lower (Quantifier.NP.individual j) = some j

lower inverts the total injection lift, lower(lift(j)) = j.

source

theorem Partee1987.iota_BE_lift {E : Type u_1} (j : E) :

Reference.iota (Quantifier.NP.BE (Quantifier.NP.individual j)) = some j

Lowering a lifted entity through BE and iota returns it.

Figure 2: the king in three types (§3.2) #

source

theorem Partee1987.the_eq_individual {E : Type u_1} (j : E) (P : E → Prop) (h : Reference.iota P = some j) :

Quantifier.GQ.the P = Quantifier.NP.individual j

Whenever iota is defined, THE(king') = lift(iota(king')).

source

theorem Partee1987.the_eq_bot {E : Type u_1} (P : E → Prop) (h : Reference.iota P = none) :

Quantifier.GQ.the P = ⊥

Whenever iota is undefined, THE(king') is the empty set of properties.

source

theorem Partee1987.lower_the {E : Type u_1} (P : E → Prop) :

lower (Quantifier.GQ.the P) = Reference.iota P

lower(THE(king')) = iota(king'), whether or not iota(king') is defined.

source

theorem Partee1987.BE_the_apply {E : Type u_1} (P : E → Prop) (x : E) :

Quantifier.NP.BE (Quantifier.GQ.the P) x ↔ ∀ (y : E), P y ↔ y = x

BE(THE(king')) holds of x when x is the only king.

source

theorem Partee1987.BE_the_eq_ident {E : Type u_1} (j : E) (P : E → Prop) (h : Reference.iota P = some j) :

Quantifier.NP.BE (Quantifier.GQ.the P) = Quantifier.NP.ident j

When iota(king') is defined, BE(THE(king')) = ident(iota(king')): the diagram commutes.

source

theorem Partee1987.BE_the_eq_self {E : Type u_1} (P : E → Prop) (hP : {x : E | P x}.Subsingleton) :

Quantifier.NP.BE (Quantifier.GQ.the P) = P

With at most one king the predicative the king is the common noun king, the equivalence that lets the article drop in John is (the) president (12).