Carlson (1977): A unified analysis of the English bare plural

[Car77a] argues that the English bare plural is unambiguous. Its existential use is not the plural of a: it takes only opaque readings (§1.2), only narrow scope with negation and other quantifiers (§1.3), and even narrower scope than a allows, as in (30) Dogs were everywhere against the bizarre (29) A dog was everywhere (differentiated scope, §1.4). Its existential and generic uses are in complementary distribution, fixed by the predicate (§2). The analysis of §4 treats the bare plural as the proper name of a kind, translated as [Mon73] translates a proper name, λP P{d} (Quantifier.NP.individual), and puts the existential in the predicate. Of the two classes of predicates that [Mil74] and [Sie76] isolate, Milsark's properties and states, a property is predicated of an individual and a state of one of its stages, a temporally and spatially bounded realization of it: Dogs are intelligent is I(d) and Dogs are sick is ∃y[R(y, d) ∧ sick'(y)], the image of the state under the realization relation R (SetRel.image).

Three consequences are derived. The scope facts force the analysis: by Quantifier.NP.exists_eq_individual_iff a noun-phrase denotation that commutes with negation and with universal quantification is a proper name, and an existential over a noun commutes with both exactly when the noun has one member (some_scopeless_iff). Differentiated scope follows from the ontology: a particular individual "can only be in one place at a time" (SpatiallyBounded), so neither Jake is everywhere nor Some dog is everywhere can be true, (135a, b) (not_everywhere, not_some_everywhere), while a kind whose stages are those of its instances is everywhere when its instances are spread over the places, (135c) (everywhere_iff). And states inherit along the instance relation where properties do not: Dogs are sitting on my lawn and All dogs are mammals give Mammals are sitting on my lawn, (119) (mem_image_of_mem_image), while Dogs are good pets does not give Mammals are good pets, (120), so a property of dogs that mammals lack is no state.

Implementation notes

• Stages and individuals are distinct types. The paper gives them one type, noting that they should be distinguished "at some level" and leaving the matter open (p. 450).
• Particular individuals and kinds are both individuals, and nothing records which is which: spatial boundedness, "the main difference between kinds and individuals" (p. 451), is a property an individual has or lacks in a model.
• The link between a kind and its instances inst is stated in two directions, as hypotheses. That every stage of a kind is a stage of one of its instances is stated on p. 452; that a stage of an instance is a stage of its kind is inferred from "If there are some of a kind present, then this counts as the presence of that kind" (p. 451). A stage of a kind is a stage of one instance, where p. 451 has "one or more of that kind".
• be everywhere is evaluated at a time, and Place is the relevant places, the restrictor Place' of the paper's formula (p. 454), so [Nontrivial Place] says there are two of them.
• The progressive, which "turns a 'property' into a 'state'" (p. 450), is the same image under R; its formula on p. 450 prints the arguments of R in the opposite order from p. 449 and is not transcribed. The habitual Dogs run, run'(d), is a property of the kind, and its relation to the state run' is left open, as in the paper.
• The negation of (134), the universal of (22) and (23), the conjunction of (58) and (59), and the belief of (132), read as universal quantification over doxastic alternatives, are all instances of the two clauses of Quantifier.NP.exists_eq_individual_iff. Montague's intension operator is not modelled.

TODO

• The anaphora facts of §1.5 and §2.2 need a dynamic layer.

References

• [Car77a]
• [Mil74]
• [Sie76]
• [Mon73]

Stages and individuals

structure Carlson1977.Model (Stage : Type u_5) (Ind : Type u_6) (Place : Type u_7) (Time : Type u_8) : Type (max (max (max u_5 u_6) u_7) u_8)

A model of the ontology of §4.2: stages, each at a place and a time, and the relation of a stage to the individuals it realizes.

• R : SetRel Stage Ind

  s ~[R] x: the stage s realizes the individual x, the paper's R(s, x).

• place : Stage → Place

  The place of a stage.

• time : Stage → Time

  The time of a stage.

def Carlson1977.Model.located {Stage : Type u_1} {Ind : Type u_2} {Place : Type u_3} {Time : Type u_4} (M : Model Stage Ind Place Time) (p : Place) (t : Time) : Set Stage

The stages at the place p at the time t, those of which the paper's At(z, p) holds.

Equations

• M.located p t = {s : Stage | M.place s = p ∧ M.time s = t}

def Carlson1977.Model.placesAt {Stage : Type u_1} {Ind : Type u_2} {Place : Type u_3} {Time : Type u_4} (M : Model Stage Ind Place Time) (x : Ind) (t : Time) : Set Place

The places an individual occupies at the time t, those of its stages then. Its stages are M.R.preimage {x}, the paper's λx R(x, j) (p. 449).

Equations

• M.placesAt x t = M.place '' (M.R.preimage {x} ∩ {s : Stage | M.time s = t})

def Carlson1977.Model.SpatiallyBounded {Stage : Type u_1} {Ind : Type u_2} {Place : Type u_3} {Time : Type u_4} (M : Model Stage Ind Place Time) (x : Ind) : Prop

An individual is spatially bounded when it "can only be in one place at a time" (p. 451), as particular individuals are and kinds are not.

Equations

• M.SpatiallyBounded x = ∀ (t : Time), (M.placesAt x t).Subsingleton

def Carlson1977.Model.Everywhere {Stage : Type u_1} {Ind : Type u_2} {Place : Type u_3} {Time : Type u_4} (M : Model Stage Ind Place Time) (t : Time) (x : Ind) : Prop

be everywhere at the time t, λx ∀y[Place'(y) → ∃z[R(z, x) ∧ At(z, y)]] (p. 454): for every place, the state of being there holds of x.

Equations

• M.Everywhere t x = ∀ (p : Place), x ∈ M.R.image (M.located p t)

theorem Carlson1977.Model.everywhere_iff_placesAt_eq_univ {Stage : Type u_1} {Ind : Type u_2} {Place : Type u_3} {Time : Type u_4} {M : Model Stage Ind Place Time} {x : Ind} {t : Time} : M.Everywhere t x ↔ M.placesAt x t = Set.univ

theorem Carlson1977.Model.not_everywhere {Stage : Type u_1} {Ind : Type u_2} {Place : Type u_3} {Time : Type u_4} {M : Model Stage Ind Place Time} {x : Ind} [Nontrivial Place] (hx : M.SpatiallyBounded x) (t : Time) : ¬M.Everywhere t x

(135a) Jake is everywhere is false: an individual that can only be in one place at a time is not everywhere, given two places.

theorem Carlson1977.Model.not_some_everywhere {Stage : Type u_1} {Ind : Type u_2} {Place : Type u_3} {Time : Type u_4} {M : Model Stage Ind Place Time} [Nontrivial Place] {N : Ind → Prop} (hN : ∀ (x : Ind), N x → M.SpatiallyBounded x) (t : Time) : ¬Quantifier.GQ.some N (M.Everywhere t)

(135b) Some dog is everywhere is false when every dog is spatially bounded, since the existential over dogs scopes over the universal over places.

Kinds and their instances

theorem Carlson1977.Model.image_image_subset {Stage : Type u_1} {Ind : Type u_2} {Place : Type u_3} {Time : Type u_4} {M : Model Stage Ind Place Time} {inst : SetRel Ind Ind} (h : M.R.comp inst ⊆ M.R) (P : Set Stage) : inst.image (M.R.image P) ⊆ M.R.image P

A state that holds of an instance of a kind holds of the kind, when a stage of an instance is a stage of its kind.

theorem Carlson1977.Model.mem_image_iff {Stage : Type u_1} {Ind : Type u_2} {Place : Type u_3} {Time : Type u_4} {M : Model Stage Ind Place Time} {k : Ind} {inst : SetRel Ind Ind} (h : M.R.comp inst ⊆ M.R) (hk : ∀ ⦃s : Stage⦄, (s, k) ∈ M.R → (s, k) ∈ M.R.comp inst) (P : Set Stage) : k ∈ M.R.image P ↔ k ∈ inst.image (M.R.image P)

A state holds of a kind exactly when it holds of one of its instances, when the stages of the kind are those of its instances: Dogs are sick is true when some dog is sick.

theorem Carlson1977.Model.mem_image_of_mem_image {Stage : Type u_1} {Ind : Type u_2} {Place : Type u_3} {Time : Type u_4} {M : Model Stage Ind Place Time} {k k' : Ind} {inst : SetRel Ind Ind} (h : M.R.comp inst ⊆ M.R) (hk : ∀ ⦃s : Stage⦄, (s, k) ∈ M.R → (s, k) ∈ M.R.comp inst) (hsub : ∀ ⦃x : Ind⦄, (x, k) ∈ inst → (x, k') ∈ inst) {P : Set Stage} (hP : k ∈ M.R.image P) : k' ∈ M.R.image P

(119): a state inherits from a kind to a kind with all of its instances, so Dogs are sitting on my lawn and All dogs are mammals give Mammals are sitting on my lawn.

theorem Carlson1977.Model.everywhere_iff {Stage : Type u_1} {Ind : Type u_2} {Place : Type u_3} {Time : Type u_4} {M : Model Stage Ind Place Time} {k : Ind} {t : Time} {inst : SetRel Ind Ind} (h : M.R.comp inst ⊆ M.R) (hk : ∀ ⦃s : Stage⦄, (s, k) ∈ M.R → (s, k) ∈ M.R.comp inst) : M.Everywhere t k ↔ ∀ (p : Place), ∃ x ∈ M.R.image (M.located p t), (x, k) ∈ inst

(135c) Dogs are everywhere: a kind whose stages are those of its instances is everywhere exactly when at each place one of its instances is there, so different places may hold different dogs.

Scope

A proper name commutes with negation and with universal quantification, and by Quantifier.NP.exists_eq_individual_iff nothing else does. Cats are here and cats are not here, (134), is a contradiction because λx ¬∃y[R(y, x) ∧ Here'(y)](c) is ¬∃y[R(y, c) ∧ Here'(y)] (p. 453), the name commuting with the negation; Everyone read books on caterpillars, (23), has one reading because the name commutes with the universal. Buildings will collapse in Berlin tomorrow, and will burn in Boston the day after, (59), means (58) because the name commutes with the conjunction of two states, each with its own existential over stages: the predicate is R.image P ∩ R.image Q, which only contains R.image (P ∩ Q).

theorem Carlson1977.some_scopeless_iff {E : Type u_5} {N : E → Prop} : ((∀ (P : E → Prop), Quantifier.GQ.some N Pᶜ ↔ ¬Quantifier.GQ.some N P) ∧ ∀ (S : Set (E → Prop)), Quantifier.GQ.some N (sInf S) ↔ ∀ P ∈ S, Quantifier.GQ.some N P) ↔ ∃ (a : E), N = Quantifier.NP.ident a

The scope diagnostics separate the bare plural from an existential: λP ∃x[N(x) ∧ P(x)] commutes with negation and with universal quantification exactly when N has one member, as a proper name does.

A model

Two dogs, each with one stage at its own place, and the kinds dogs and mammals, both realized by the stages of their instances. Dogs are everywhere while neither dog is, and a property that dogs have and mammals lack is no state.

inductive Carlson1977.Dog : Type

The dogs of the model.

• rex : Dog
• fido : Dog

@[instance_reducible]

instance Carlson1977.instDecidableEqDog : DecidableEq Dog

Equations

• Carlson1977.instDecidableEqDog x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Carlson1977.instNontrivialDog : Nontrivial Dog

inductive Carlson1977.Individual : Type

The individuals of the model: two kinds and two dogs.

• dogs : Individual
• mammals : Individual
• dog (d : Dog) : Individual

def Carlson1977.instDecidableEqIndividual.decEq (x✝ x✝¹ : Individual) : Decidable (x✝ = x✝¹)

Equations

• Carlson1977.instDecidableEqIndividual.decEq Carlson1977.Individual.dogs Carlson1977.Individual.dogs = isTrue ⋯
• Carlson1977.instDecidableEqIndividual.decEq Carlson1977.Individual.dogs Carlson1977.Individual.mammals = isFalse Carlson1977.instDecidableEqIndividual.decEq._proof_3
• Carlson1977.instDecidableEqIndividual.decEq Carlson1977.Individual.dogs (Carlson1977.Individual.dog d) = isFalse ⋯
• Carlson1977.instDecidableEqIndividual.decEq Carlson1977.Individual.mammals Carlson1977.Individual.dogs = isFalse Carlson1977.instDecidableEqIndividual.decEq._proof_5
• Carlson1977.instDecidableEqIndividual.decEq Carlson1977.Individual.mammals Carlson1977.Individual.mammals = isTrue ⋯
• Carlson1977.instDecidableEqIndividual.decEq Carlson1977.Individual.mammals (Carlson1977.Individual.dog d) = isFalse ⋯
• Carlson1977.instDecidableEqIndividual.decEq (Carlson1977.Individual.dog d) Carlson1977.Individual.dogs = isFalse ⋯
• Carlson1977.instDecidableEqIndividual.decEq (Carlson1977.Individual.dog d) Carlson1977.Individual.mammals = isFalse ⋯
• Carlson1977.instDecidableEqIndividual.decEq (Carlson1977.Individual.dog a) (Carlson1977.Individual.dog b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Carlson1977.instDecidableEqIndividual : DecidableEq Individual

Equations

• Carlson1977.instDecidableEqIndividual = Carlson1977.instDecidableEqIndividual.decEq

def Carlson1977.ofKind : SetRel Individual Individual

x ~[ofKind] k: each dog is of both kinds.

Equations

• One or more equations did not get rendered due to their size.

def Carlson1977.model : Model Dog Individual Dog Unit

The model: each dog's one stage is at that dog's place, and it realizes the dog and both kinds.

Equations

• One or more equations did not get rendered due to their size.

theorem Carlson1977.model_comp_subset : model.R.comp ofKind ⊆ model.R

theorem Carlson1977.model_stages_of_kind {k : Individual} (hk : k = Individual.dogs ∨ k = Individual.mammals) ⦃s : Dog⦄ : (s, k) ∈ model.R → (s, k) ∈ model.R.comp ofKind

theorem Carlson1977.model_everywhere_dogs : model.Everywhere () Individual.dogs

(135c) in the model: dogs are everywhere.

theorem Carlson1977.model_spatiallyBounded (d : Dog) : model.SpatiallyBounded (Individual.dog d)