Mitrović and Sauerland (2016): Two Conjunctions Are Better Than One

Mitrović and Sauerland decompose the conjunction of two noun phrases into a junctor J, which intersects two generalized quantifiers, and a head μ on each conjunct, which denotes the subset relation and so is the quantifier every. Languages differ in which of the three heads they pronounce: English and is J, Japanese mo is μ, and Hungarian pronounces all three. Only μ can have the additive and quantificational uses of Japanese mo.

Main statements

• conjunction_apply: J′ over the μ phrases of two individuals holds of a predicate exactly when the predicate holds of each.
• mu_of_conjunctive_particle: μ on an indeterminate is the universal quantifier, as in Japanese dare-mo and Latin quis-que.
• muPrime_team: the collective μ′ of (20) holds of a predicate true only of a larger team, (22), so it gives no collective reading.
• mem_attested_iff: the examples pronounce exactly the nonempty sets of heads in which the first μ comes only with the second.
• languages_pronounced_eq_univ: all three heads are pronounced in Southeastern Macedonian, Serbo-Croatian, Hungarian and Avar.
• mu_has_other_use, j_has_no_other_use: the μ coordinators have additive or quantificational uses, and the J coordinators have neither.

Implementation notes

• The heads an example pronounces are those its gloss line writes outside parentheses, or for Latin -que and atque those of the configurations (38b) and (39). The examples are (1c), (23)–(29) with fn. 9, and (33).
• The J coordinators with Fragment entries are English and, Japanese to, the verbal conjunction of Table 1, and Hungarian és; the μ coordinators are Japanese mo, Hungarian is and Latin -que. A coordinator's additive use is Coordinator.IsAlsoAdditive against the additive particles of its language in the Fragments.

TODO

• Table 1, fifteen languages whose quantificational conjunction is the nominal one and not the verbal one, and the Indo-European shift from μ to J of §3.3.

References

• [MS16a]
• [MS14]

The two heads, (12)

def MitrovicSauerland2016.mu {α : Type u_1} (R S : α → Prop) : Prop

The head μ denotes the subset relation between two predicates, (12a).

Equations

• MitrovicSauerland2016.mu R S = (R ≤ S)

def MitrovicSauerland2016.shift {α : Type u_1} (a : α) : α → Prop

The shift from an individual to its characteristic property, the singleton.

Equations

• MitrovicSauerland2016.shift a x✝ = (x✝ = a)

theorem MitrovicSauerland2016.mu_eq_every {α : Type u_1} : mu = Quantifier.GQ.every

The subset relation is the generalized quantifier every, so a μ particle on a restrictor is a universal quantifier, (15).

theorem MitrovicSauerland2016.mu_shift {α : Type u_1} (a : α) : mu (shift a) = Quantifier.NP.individual a

μ of a shifted individual is its Montague lift.

theorem MitrovicSauerland2016.conjunction_eq {α : Type u_1} {j : Coordinator} (hj : j.role = Coordinator.Role.conjunctive) (a b : α) : j.denote {mu (shift a), mu (shift b)} = Quantifier.NP.individual a ⊓ Quantifier.NP.individual b

In the conjunction of two individuals, (13), J′, a conjunctive coordinator and so intersection, applied to the μ phrases of the shifted conjuncts gives the meet of their Montague lifts.

theorem MitrovicSauerland2016.conjunction_apply {α : Type u_1} {j : Coordinator} (hj : j.role = Coordinator.Role.conjunctive) (a b : α) (P : α → Prop) : j.denote {mu (shift a), mu (shift b)} P ↔ P a ∧ P b

The conjunction holds of a predicate that holds of each conjunct, so it has no collective reading, (14).

theorem MitrovicSauerland2016.shift_inf_shift_eq_bot_iff {α : Type u_1} {a b : α} : shift a ⊓ shift b = ⊥ ↔ a ≠ b

J′ cannot apply to the shifted individuals without μ, since the intersection of two singletons is empty unless the conjuncts are identical.

The collective μ′, (20)–(22)

def MitrovicSauerland2016.muPrime {α : Type u_1} [SemilatticeSup α] (x : α) (P : α → Prop) : Prop

muPrime x P, the collective μ′ that (20) tries, holds when P is true of some sum of which x is a part.

Equations

• MitrovicSauerland2016.muPrime x P = ∃ (y : α), y ⊔ x = y ∧ P y

theorem MitrovicSauerland2016.muPrime_iff_mem_lowerClosure {α : Type u_1} [SemilatticeSup α] {x : α} {P : α → Prop} : muPrime x P ↔ x ∈ lowerClosure {y : α | P y}

μ′ of an individual holds of a predicate when the individual is below some element of its extension.

theorem MitrovicSauerland2016.muPrime_of_le {α : Type u_1} [SemilatticeSup α] {x y : α} {P : α → Prop} (hxy : x ≤ y) (hy : P y) : muPrime x P

theorem MitrovicSauerland2016.muPrime_of_collective {α : Type u_1} [SemilatticeSup α] {P : α → Prop} {a b : α} (h : P (a ⊔ b)) : muPrime a P ∧ muPrime b P

The conjunction of two μ′ phrases, (21), holds of a predicate true of their sum, the collective reading of (19).

theorem MitrovicSauerland2016.muPrime_of_distributive {α : Type u_1} [SemilatticeSup α] {P : α → Prop} {a b : α} (ha : P a) (hb : P b) : muPrime a P ∧ muPrime b P

The conjunction of two μ′ phrases holds of a predicate true of each conjunct, the distributive reading.

theorem MitrovicSauerland2016.muPrime_team : ((muPrime {0} fun (x : Finset (Fin 3)) => x = Finset.univ) ∧ muPrime {1} fun (x : Finset (Fin 3)) => x = Finset.univ) ∧ {0} ⊔ {1} ≠ Finset.univ ∧ {0} ≠ Finset.univ

For two members of a team of three, (22), the conjunction of their μ′ phrases holds of forming the team, though neither the collective nor the distributive reading does, so μ′ is too weak to give a collective reading.

theorem MitrovicSauerland2016.mu_of_conjunctive_particle {q : IndeterminateQuantifier} (hq : q.particle.role = Coordinator.Role.conjunctive) {α : Type} [Fintype α] {d : Quantifier.GQ.Family} (h : d ∈ Semantics.Denotes.denote q) : d α = mu

An indeterminate quantifier whose particle is conjunctive denotes μ, (15).

theorem MitrovicSauerland2016.dare_mo_denotes_mu {α : Type} [Fintype α] {d : Quantifier.GQ.Family} (h : d ∈ Semantics.Denotes.denote Japanese.Determiners.dare_mo) : d α = mu

The universal reading of Japanese dare-mo 'everyone' is μ, (1a).

theorem MitrovicSauerland2016.quisque_denotes_mu {α : Type} [Fintype α] {d : Quantifier.GQ.Family} (h : d ∈ Semantics.Denotes.denote Latin.Determiners.quisque) : d α = mu

Latin quis-que 'each' is μ on the indeterminate quis, (40).

Exponence, §3.1

inductive MitrovicSauerland2016.Head : Type

The heads of the structure for the conjunction of two noun phrases, (11) and (13), are J and a μ head on each conjunct.

• j : Head
• mu (conjunct : Fin 2) : Head

@[instance_reducible]

instance MitrovicSauerland2016.instDecidableEqHead : DecidableEq Head

Equations

• MitrovicSauerland2016.instDecidableEqHead = MitrovicSauerland2016.instDecidableEqHead.decEq

def MitrovicSauerland2016.instDecidableEqHead.decEq (x✝ x✝¹ : Head) : Decidable (x✝ = x✝¹)

Equations

• MitrovicSauerland2016.instDecidableEqHead.decEq MitrovicSauerland2016.Head.j MitrovicSauerland2016.Head.j = isTrue ⋯
• MitrovicSauerland2016.instDecidableEqHead.decEq MitrovicSauerland2016.Head.j (MitrovicSauerland2016.Head.mu conjunct) = isFalse ⋯
• MitrovicSauerland2016.instDecidableEqHead.decEq (MitrovicSauerland2016.Head.mu conjunct) MitrovicSauerland2016.Head.j = isFalse ⋯
• MitrovicSauerland2016.instDecidableEqHead.decEq (MitrovicSauerland2016.Head.mu a) (MitrovicSauerland2016.Head.mu b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance MitrovicSauerland2016.instReprHead : Repr Head

Equations

• MitrovicSauerland2016.instReprHead = { reprPrec := MitrovicSauerland2016.instReprHead.repr }

def MitrovicSauerland2016.instReprHead.repr : Head → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance MitrovicSauerland2016.instFintypeHead : Fintype Head

Equations

• MitrovicSauerland2016.instFintypeHead = Fintype.ofEquiv (Unit ⊕ Fin 2) MitrovicSauerland2016.Head.proxyTypeEquiv

theorem MitrovicSauerland2016.card_head : Fintype.card Head = 3

def MitrovicSauerland2016.Head.labels : List (String × Head)

The labels of the heads in the rows.

Equations

• MitrovicSauerland2016.Head.labels = [("j", MitrovicSauerland2016.Head.j), ("mu-first", MitrovicSauerland2016.Head.mu 0), ("mu-second", MitrovicSauerland2016.Head.mu 1)]

def MitrovicSauerland2016.pronounced (d : Datum) : Finset Head

The heads an example pronounces.

Equations

• MitrovicSauerland2016.pronounced d = (List.filterMap (fun (x : String) => List.lookup x MitrovicSauerland2016.Head.labels) (d.features "head")).toFinset

def MitrovicSauerland2016.attested : Finset (Finset Head)

The sets of heads the examples pronounce.

Equations

• MitrovicSauerland2016.attested = (List.map MitrovicSauerland2016.pronounced MitrovicSauerland2016.Examples.all).toFinset

theorem MitrovicSauerland2016.attested_eq : attested = {{Head.j}, {Head.mu 1}, {Head.mu 0, Head.mu 1}, {Head.j, Head.mu 1}, Finset.univ}

theorem MitrovicSauerland2016.mem_attested_iff {h : Finset Head} : h ∈ attested ↔ h.Nonempty ∧ (Head.mu 0 ∈ h → Head.mu 1 ∈ h)

The examples pronounce exactly the nonempty sets of heads in which the μ of the first conjunct comes only with that of the second, all but the sets that keep the first μ and drop the second.

theorem MitrovicSauerland2016.languages_pronounced_eq_univ : List.map (fun (x : Datum) => x.language) (List.filter (fun (x : Datum) => decide (pronounced x = Finset.univ)) Examples.all) = ["mace1250", "sout1528", "hung1274", "avar1256"]

The examples that pronounce all three heads are Southeastern Macedonian (26), Serbo-Croatian (27), whose J is adversative, Hungarian (28) and Avar (29).

Other uses, §3

def MitrovicSauerland2016.jCoordinators : List Coordinator

The coordinators the paper takes for J that have Fragment entries.

Equations

• MitrovicSauerland2016.jCoordinators = [English.Coordination.and_, Japanese.Coordination.to_, Hungarian.Coordination.es]

def MitrovicSauerland2016.muCoordinators : List Coordinator

The coordinators the paper takes for μ that have Fragment entries.

Equations

• MitrovicSauerland2016.muCoordinators = [Japanese.Coordination.mo, Hungarian.Coordination.is_, Latin.Coordination.que]

def MitrovicSauerland2016.additiveParticles : List AdditiveParticle

The additive particles of their languages in the Fragments.

Equations

• MitrovicSauerland2016.additiveParticles = [English.FocusParticles.too, English.FocusParticles.also, Japanese.FocusParticles.mo, Hungarian.FocusParticles.is_]

def MitrovicSauerland2016.quantifiers : List IndeterminateQuantifier

The indeterminate quantifiers of their languages in the Fragments.

Equations

• MitrovicSauerland2016.quantifiers = Japanese.Determiners.indefinites ++ [Latin.Determiners.quisque]

theorem MitrovicSauerland2016.coordinators_conjunctive (c : Coordinator) : c ∈ jCoordinators ++ muCoordinators → c.role = Coordinator.Role.conjunctive

theorem MitrovicSauerland2016.mu_has_other_use (c : Coordinator) : c ∈ muCoordinators → (∃ a ∈ additiveParticles, c.IsAlsoAdditive a) ∨ ∃ q ∈ quantifiers, q.particle = c

Every μ coordinator has a use outside conjunction, as an additive particle or as the particle of an indeterminate quantifier.

theorem MitrovicSauerland2016.j_has_no_other_use (c : Coordinator) : c ∈ jCoordinators → (∀ a ∈ additiveParticles, ¬c.IsAlsoAdditive a) ∧ ∀ q ∈ quantifiers, q.particle ≠ c

No J coordinator has an additive or a quantificational use.