Sauerland (2003): a new semantics for number

Sauerland locates the interpreted number feature in a φ-head above DP and interprets agreement features as presuppositions: [Sg] is the identity function presupposing an atom (his entry admits an atom or a mass; Number.dom keeps the atomic case), [Pl] the identity with no presupposition, and Heim's Maximize Presupposition has the speaker use the most specific feature whose presupposition holds, (7). In competition with the singular the plural is therefore unblocked only at non-atoms (unblocked_plural), which the coordination Kai and Lina shows (coordination_plural), and at atoms too once the singular is blocked by an independent factor, singular they (13) or polite address (14) (unblocked_plural_of_singular_blocked). The two domains are nested (sg_domain_ssubset_pl), an instance of his Feature-Subset Principle (46), and since the features are domain restrictions the competition is presuppositional rather than scalar. The person features (44) compete the same way: the second person is used outside the first person's domain and the third outside the participants', the non-participant presupposition of (47) (unblocked_second, unblocked_third), except in a context whose speaker is part of the addressee, where the first and second person domains coincide and competition cannot separate them (unblocked_second_of_degenerate).

Every decomposes into a definite DER, taking the maximal element of a cumulative restrictor (der_unique; his cover-based * is Mereology.algClosure_iff_exists_sup'), and JE, a universal over the atomic parts of a group individual that projects its scope's presupposition universally (JE), whose truth on a bivalent scope is Link's distributivity operator (je_eq_one_iff_D, je_eq_one_iff_forall). The indefinite projects existentially (aSem), so every boy invited his sister requires every boy to have a sister while a boy invited his sister requires one (projection_asymmetry), and the weak plural makes Lina didn't harvest tomatoes entail Lina didn't harvest a tomato (negated_pl_entails_negated_sg). The same mechanism runs Czech gender agreement on coordinations, masculine vacuous, feminine presupposing non-masculinity and neuter presupposing genderlessness (czech_gender), and predicts that polite address recruits the unmarked values, plural and third person (politeness_unmarked).

References

• [Sau03]
• [Hei91], [Lin87b]

Number features and Maximize Presupposition

theorem Sauerland2003.coordination_plural {E : Type u_1} [SemilatticeSup E] {a b : E} (ha : Mereology.Atom a) (hb : Mereology.Atom b) (hne : a ≠ b) : a ⊔ b ∉ Number.dom (some Number.singular)

The φ-head above a coordination of two distinct atoms cannot carry [Sg].

theorem Sauerland2003.sg_domain_ssubset_pl {E : Type u_1} [SemilatticeSup E] {a b : E} (ha : Mereology.Atom a) (hb : Mereology.Atom b) (hne : a ≠ b) : Number.dom (some Number.singular) ⊂ Number.dom (some Number.plural)

The Feature-Subset Principle for number makes the domain of [Sg] a proper subset of the domain of [Pl].

theorem Sauerland2003.der_unique {E : Type u_1} [SemilatticeSup E] {R : E → Prop} {m₁ m₂ : E} (h₁ : Maximal (Mereology.AlgClosure R) m₁) (h₂ : Maximal (Mereology.AlgClosure R) m₂) : m₁ = m₂

DER is well defined on a cumulative restrictor, since *R has at most one maximal element.

def Sauerland2003.numberAlts : Option Number → Set (Option Number)

The two number features that can head a φP are each other's alternatives.

Equations

• Sauerland2003.numberAlts x✝ = {some Number.singular, some Number.plural}

theorem Sauerland2003.unblocked_singular {E : Type u_1} [SemilatticeSup E] : Competition.unblocked numberAlts Number.dom (some Number.singular) = {x : E | Mereology.Atom x}

[Sg] is used exactly at the atoms.

theorem Sauerland2003.unblocked_plural {E : Type u_1} [SemilatticeSup E] {a b : E} (ha : Mereology.Atom a) (hb : Mereology.Atom b) (hne : a ≠ b) : Competition.unblocked numberAlts Number.dom (some Number.plural) = {x : E | ¬Mereology.Atom x}

[Pl] is used exactly at the non-atoms, the non-atomicity derived from Maximize Presupposition.

theorem Sauerland2003.unblocked_plural_of_singular_blocked {E : Type u_1} [SemilatticeSup E] : Competition.unblocked (fun (x : Option Number) => {some Number.plural}) Number.dom (some Number.plural) = Set.univ

With [Sg] blocked by an independent factor, [Pl] is used of atoms too, (13)–(14).

theorem Sauerland2003.atom_mem_unblocked_iff {E : Type u_1} [SemilatticeSup E] {a b : E} (ha : Mereology.Atom a) (hb : Mereology.Atom b) (hne : a ≠ b) : a ∉ Competition.unblocked numberAlts Number.dom (some Number.plural) ∧ a ∈ Competition.unblocked (fun (x : Option Number) => {some Number.plural}) Number.dom (some Number.plural)

At an atom [Pl] is unusable while [Sg] competes and usable once it is blocked.

Person

def Sauerland2003.personAlts : Option Person → Set (Option Person)

The three person features that can head a φP are each other's alternatives, (44).

Equations

• Sauerland2003.personAlts x✝ = {some Person.first, some Person.second, some Person.third}

theorem Sauerland2003.dom_first_ssubset_dom_second {E : Type u_1} {W : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) (h : ¬c.agent ≤ c.addressee) : Person.dom c (some Person.first) ⊂ Person.dom c (some Person.second)

theorem Sauerland2003.unblocked_first {E : Type u_1} {W : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) : Competition.unblocked personAlts (Person.dom c) (some Person.first) = Person.dom c (some Person.first)

The first person is used on its whole domain.

theorem Sauerland2003.unblocked_second {E : Type u_1} {W : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) (h : ¬c.agent ≤ c.addressee) : Competition.unblocked personAlts (Person.dom c) (some Person.second) = Person.dom c (some Person.second) \ Person.dom c (some Person.first)

Unless the speaker is part of the addressee, the second person is used in its domain outside the first person's.

theorem Sauerland2003.unblocked_second_of_degenerate {E : Type u_1} {W : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) (h : c.agent ≤ c.addressee) : Competition.unblocked personAlts (Person.dom c) (some Person.second) = Person.dom c (some Person.second)

When the speaker is part of the addressee, the first and second person domains coincide and competition leaves the second person usable on its whole domain.

theorem Sauerland2003.unblocked_third {E : Type u_1} {W : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) (h : ∃ (x : E), x ∉ Person.dom c (some Person.second)) : Competition.unblocked personAlts (Person.dom c) (some Person.third) = (Person.dom c (some Person.second))ᶜ

The third person is used outside the participants' domain, the non-participant presupposition of (47), when some referent lies outside it.

Every as JE ∘ DER, and the indefinite

noncomputable def Sauerland2003.aSem {E : Type u_1} (R : E → Prop) (S : E → SignType) : SignType

The indefinite projects its scope's presupposition existentially, defined when the scope is defined of some individual of the restrictor and true when it is true of one.

Equations

• Sauerland2003.aSem R S = Trivalent.existsHaug fun (x : { x : E // R x }) => S ↑x

noncomputable def Sauerland2003.JE {E : Type u_1} [PartialOrder E] (X : E) (P : E → SignType) : SignType

JE, the quantificational part of every, ranges over the atomic parts of a group individual X, presupposing the scope predicate is defined at each and asserting it holds at each.

Equations

• Sauerland2003.JE X P = Trivalent.forallWeak fun (a : { a : E // Mereology.Atom a ∧ a ≤ X }) => P ↑a

theorem Sauerland2003.je_eq_one_iff_forall {E : Type u_1} [PartialOrder E] {R Q : E → Prop} [DecidablePred Q] {maxR : E} (hR : ∀ (x : E), R x ↔ Mereology.Atom x ∧ x ≤ maxR) : (JE maxR fun (x : E) => SignType.ofProp (Q x)) = 1 ↔ ∀ (x : E), R x → Q x

When the atoms below maxR are exactly the R-elements, JE with a bivalent scope asserts the ordinary universal.

theorem Sauerland2003.projection_asymmetry {E : Type u_1} [PartialOrder E] {boys a₁ a₂ : E} {R : E → Prop} {S : E → SignType} (ha₂ : Mereology.Atom a₂) (h₂ : a₂ ≤ boys) (hR₁ : R a₁) (hdom₁ : S a₁ ≠ 0) (hdom₂ : S a₂ = 0) : aSem R S ≠ 0 ∧ JE boys S = 0

JE projects its scope's presupposition universally and the indefinite existentially. With a restrictor atom a₂ ≤ boys outside the scope's domain and some R-individual inside it, a boy invited his sister is defined and every boy invited his sister is not.

theorem Sauerland2003.negated_pl_entails_negated_sg {E : Type u_1} [PartialOrder E] {starR harvest : E → Prop} [DecidablePred harvest] (h : (aSem starR fun (x : E) => SignType.ofProp (harvest x)) = -1) (hsg : (aSem (fun (x : E) => Mereology.Atom x ∧ starR x) fun (x : E) => SignType.ofProp (harvest x)) ≠ 0) : (aSem (fun (x : E) => Mereology.Atom x ∧ starR x) fun (x : E) => SignType.ofProp (harvest x)) = -1

Under the weak plural Lina didn't harvest tomatoes entails Lina didn't harvest a tomato wherever the latter is defined, the singular indefinite restricting the plural's assertion to atoms.

theorem Sauerland2003.je_eq_one_iff_D {E : Type u_1} [SemilatticeSup E] (X : E) (P : E → Prop) [DecidablePred P] : (JE X fun (x : E) => SignType.ofProp (P x)) = 1 ↔ Mereology.D P X

On a bivalent scope JE is [Lin87b]'s distributivity operator.

Gender agreement in Czech coordinations

inductive Sauerland2003.Conjunct : Type

A conjunct of one of Sauerland's Czech coordinations is a man, a woman or a child.

• man : Conjunct
• woman : Conjunct
• child : Conjunct

@[instance_reducible]

instance Sauerland2003.instDecidableEqConjunct : DecidableEq Conjunct

Equations

• Sauerland2003.instDecidableEqConjunct x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Sauerland2003.instReprConjunct.repr : Conjunct → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Sauerland2003.instReprConjunct : Repr Conjunct

Equations

• Sauerland2003.instReprConjunct = { reprPrec := Sauerland2003.instReprConjunct.repr }

@[instance_reducible]

instance Sauerland2003.gendered : Gendered (Finset Conjunct)

A coordination is gendered masculine when a conjunct is a man, and feminine when a conjunct is a woman and none is a man; a coordination of children is gendered neither way.

Equations

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

def Sauerland2003.janVera : Finset Conjunct

Jan a Věra, Matka a její dítě and Otec a jeho dítě, as the sums of their conjuncts.

Equations

• Sauerland2003.janVera = {Sauerland2003.Conjunct.man, Sauerland2003.Conjunct.woman}

def Sauerland2003.matkaDite : Finset Conjunct

Equations

• Sauerland2003.matkaDite = {Sauerland2003.Conjunct.woman, Sauerland2003.Conjunct.child}

def Sauerland2003.otecDite : Finset Conjunct

Equations

• Sauerland2003.otecDite = {Sauerland2003.Conjunct.man, Sauerland2003.Conjunct.child}

theorem Sauerland2003.czech_gender : janVera ∉ Gender.dom (some Gender.feminine) ∧ matkaDite ∈ Gender.dom (some Gender.feminine) ∧ matkaDite ∉ Gender.dom (some Gender.neuter) ∧ otecDite ∉ Gender.dom (some Gender.feminine) ∧ otecDite ∈ Gender.dom (some Gender.masculine)

Of Sauerland's Czech coordinations, Jan a Věra excludes feminine, Matka a její dítě takes feminine but not neuter, and Otec a jeho dítě takes only the vacuous masculine.

Politeness

theorem Sauerland2003.politeness_unmarked {E : Type u_1} {W : Type u_2} {P : Type u_3} {T : Type u_4} [PartialOrder E] (c : Reference.Context W E P T) : Number.dom (some Number.plural) = Set.univ ∧ Person.dom c (some Person.third) = Set.univ

Polite address recruits the semantically unmarked values, plural and third person, whose vacuous presuppositions hold of any addressee (German Sie).