Bill, Gonzalez, Driemel, Makharoblidze and Pintér (2025): Is DP conjunction always complex?

Bill and colleagues test Mitrović and Sauerland's decomposition of noun-phrase conjunction on how children understand the three conjunctive expressions of Georgian and Hungarian, a J particle alone, a μ particle on each conjunct, and both. With van Hout's Transparency Principle the decomposition predicts the fully pronounced J-μ expressions to be the easiest, and the rival structures of Szabolcsi and of Haslinger and colleagues predict the J expressions to be. Georgian children instead replayed J-μ sentences most, and Hungarian children showed no difference.

Main statements

• pronounced_mem_attested: each sentence type pronounces a set of heads that Mitrović and Sauerland's examples attest.
• transparency_prediction: the decomposition with the Transparency Principle predicts J-μ easiest, while playedMore_child_iff says Georgian children replayed J-μ more than either other sentence type, and those two did not differ.
• desiderata_iff: a measure meets the paper's conditions on a successful account exactly when the order it predicts is the observed one, which none of Account.universal.covert, Account.bareJ.complexity and Account.bareJ.covert does.
• not_sentenceEffect_hungarian: Hungarian shows no sentence-type effect on either measure.
• basicTrue_iff_conjunction, accurate_iff: the decomposition computes the basic truth conditions of the test sentences, and the accurate end state is the one with the mentioned objects and nothing else on the table.

Implementation notes

• An account assigns each sentence type the heads of its underlying structure, and a measure of difficulty counts the heads it leaves unpronounced or all of them. A difference is the paper's star on a contrast or a fixed effect, its direction the sign of the printed estimate.
• The sentence types are the paper's three; it sets aside the expressions with one μ (fn. 1).
• The type-shifter of the decomposition is not counted as a head, since no language pronounces it and it would add the same constant to every count. The rival structures are the paper's simplification, since neither Szabolcsi's nor Haslinger and colleagues' analysis is formalized.
• Accuracy exhaustifies against the domain alternatives o is on the table. The three kinds of error are classified in the order the paper lists them, so an error with an unmentioned object on the table counts as such whatever else it lacks.

References

• [BGD+25]
• [MS14]
• [MS16a]
• [vH98]
• [Sza15]
• [HPR+19]
• [Cla17]
• [Fox07]

The test sentences

def BillEtAl2025.Sentence.pronounced : Sentence → Finset MitrovicSauerland2016.Head

A sentence type pronounces J, the μ head of each conjunct, or all three heads.

Equations

• BillEtAl2025.Sentence.j.pronounced = {MitrovicSauerland2016.Head.j}
• BillEtAl2025.Sentence.mu.pronounced = {MitrovicSauerland2016.Head.mu 0, MitrovicSauerland2016.Head.mu 1}
• BillEtAl2025.Sentence.jMu.pronounced = Finset.univ

theorem BillEtAl2025.pronounced_mem_attested (s : Sentence) : s.pronounced ∈ MitrovicSauerland2016.attested

Each sentence type pronounces heads in a way that Mitrović and Sauerland's examples attest.

def BillEtAl2025.jParticle : Language → Coordinator

The J particle of a test language, Georgian da, (2), and Hungarian és, (1).

Equations

• BillEtAl2025.jParticle BillEtAl2025.Language.georgian = Georgian.Coordination.da
• BillEtAl2025.jParticle BillEtAl2025.Language.hungarian = Hungarian.Coordination.es

def BillEtAl2025.muParticle : Language → Coordinator

The μ particle of a test language, Georgian -c, (2), and Hungarian is, (1).

Equations

• BillEtAl2025.muParticle BillEtAl2025.Language.georgian = Georgian.Coordination.c
• BillEtAl2025.muParticle BillEtAl2025.Language.hungarian = Hungarian.Coordination.is_

def BillEtAl2025.additiveParticle : Language → AdditiveParticle

The additive particle of a test language, Georgian -c and Hungarian is.

Equations

• BillEtAl2025.additiveParticle BillEtAl2025.Language.georgian = Georgian.FocusParticles.c
• BillEtAl2025.additiveParticle BillEtAl2025.Language.hungarian = Hungarian.FocusParticles.is_

theorem BillEtAl2025.muParticle_isAlsoAdditive (l : Language) : (muParticle l).IsAlsoAdditive (additiveParticle l)

The μ particle of each test language is also its additive particle, as Mitrović and Sauerland predict of μ.

theorem BillEtAl2025.not_jParticle_isAlsoAdditive (l : Language) : ¬(jParticle l).IsAlsoAdditive (additiveParticle l)

The J particle of neither test language is its additive particle.

Accounts and their measures

structure BillEtAl2025.Account : Type

An account assigns each sentence type the heads of its underlying structure, among which are the heads it pronounces.

• underlying : Sentence → Finset MitrovicSauerland2016.Head

  The heads of the structure underlying a sentence type.

• pronounced_subset (s : Sentence) : s.pronounced ⊆ self.underlying s

  A sentence type pronounces only heads of its structure.

def BillEtAl2025.Account.universal : Account

Mitrović and Sauerland give every sentence type the whole structure.

Equations

• BillEtAl2025.Account.universal = { underlying := fun (x : BillEtAl2025.Sentence) => Finset.univ, pronounced_subset := BillEtAl2025.Account.universal._proof_1 }

def BillEtAl2025.Account.bareJ : Account

The rival structures give J expressions J alone, and μ and J-μ expressions the whole structure.

Equations

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

def BillEtAl2025.Account.complexity (a : Account) (s : Sentence) : ℕ

The complexity of a sentence type is the number of heads in its structure.

Equations

• a.complexity s = (a.underlying s).card

def BillEtAl2025.Account.covert (a : Account) (s : Sentence) : ℕ

The covert pieces of a sentence type are the heads of its structure it leaves unpronounced, the Transparency Principle's measure of difficulty.

Equations

• a.covert s = (a.underlying s \ s.pronounced).card

theorem BillEtAl2025.Account.card_pronounced_add_covert (a : Account) (s : Sentence) : s.pronounced.card + a.covert s = a.complexity s

theorem BillEtAl2025.Account.universal_covert (s : Sentence) : universal.covert s = Fintype.card MitrovicSauerland2016.Head - s.pronounced.card

The predictions

theorem BillEtAl2025.transparency_prediction (s : Sentence) (h : s ≠ Sentence.jMu) : Account.universal.covert Sentence.jMu < Account.universal.covert s

The decomposition with the Transparency Principle predicts J-μ, which pronounces every head, easier than either other sentence type.

theorem BillEtAl2025.bareJ_prediction : Account.bareJ.complexity Sentence.j < Account.bareJ.complexity Sentence.jMu

If the more complex is the harder, the rival predicts J expressions easier than J-μ expressions.

theorem BillEtAl2025.bareJ_underlying_mu : Account.bareJ.underlying Sentence.mu = Account.bareJ.underlying Sentence.jMu

The rival gives μ and J-μ expressions one structure.

theorem BillEtAl2025.bareJ_mu_opaque : Account.bareJ.covert Sentence.jMu < Account.bareJ.covert Sentence.mu

On the rival structures μ expressions are the more opaque of μ and J-μ.

The findings

def BillEtAl2025.Contrast.sentences : Contrast → Sentence × Sentence

The two sentence types a follow-up contrast compares, in the paper's order.

Equations

• BillEtAl2025.Contrast.jVsJMu.sentences = (BillEtAl2025.Sentence.j, BillEtAl2025.Sentence.jMu)
• BillEtAl2025.Contrast.jVsMu.sentences = (BillEtAl2025.Sentence.j, BillEtAl2025.Sentence.mu)
• BillEtAl2025.Contrast.jMuVsMu.sentences = (BillEtAl2025.Sentence.jMu, BillEtAl2025.Sentence.mu)

def BillEtAl2025.PlayedMore (g : Group) (s t : Sentence) : Prop

A group replayed sentences of one type more than those of another when the paper stars their contrast, in the direction of the estimate, which is negative when the first was played less. Children replay the sentences they find difficult, so this is the order of difficulty the Georgian data show.

Equations

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

@[instance_reducible]

instance BillEtAl2025.instDecidableRelSentencePlayedMore (g : Group) : DecidableRel (PlayedMore g)

Equations

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

theorem BillEtAl2025.playedMore_child_iff (s t : Sentence) : PlayedMore Group.child s t ↔ s = Sentence.jMu ∧ t ≠ Sentence.jMu

Georgian children replayed J-μ sentences more than J and than μ sentences, and J and μ sentences did not differ.

theorem BillEtAl2025.not_playedMore_adult (s t : Sentence) : ¬PlayedMore Group.adult s t

Georgian adults replayed no sentence type more than another.

theorem BillEtAl2025.playedMore_child_contradicts_transparency {s t : Sentence} (h : PlayedMore Group.child s t) : Account.universal.covert s < Account.universal.covert t

The observed differences run against the decomposition's prediction.

def BillEtAl2025.SentenceEffect (l : Language) (m : Measure) : Prop

A language shows a sentence-type effect on a measure when the paper stars that fixed effect.

Equations

• BillEtAl2025.SentenceEffect l m = ((BillEtAl2025.lrt l m BillEtAl2025.Effect.sentence).mark = BillEtAl2025.Mark.starred)

@[instance_reducible]

instance BillEtAl2025.instDecidableSentenceEffect (l : Language) (m : Measure) : Decidable (SentenceEffect l m)

Equations

• BillEtAl2025.instDecidableSentenceEffect l m = BillEtAl2025.instDecidableSentenceEffect._aux_1 l m

theorem BillEtAl2025.not_sentenceEffect_hungarian (m : Measure) : ¬SentenceEffect Language.hungarian m

Hungarian showed no difference between the sentence types on either measure.

theorem BillEtAl2025.georgian_sentenceEffect_iff (m : Measure) : SentenceEffect Language.georgian m ↔ m = Measure.playedN

Georgian showed a difference between the sentence types only in how often they were replayed, not in accuracy.

def BillEtAl2025.Desiderata (c : Sentence → ℕ) : Prop

A measure meets the paper's conditions on a successful account when J-μ is more complex than J and than μ, and J and μ are equally complex.

Equations

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

@[instance_reducible]

instance BillEtAl2025.instDecidableDesiderata (c : Sentence → ℕ) : Decidable (Desiderata c)

Equations

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

theorem BillEtAl2025.desiderata_iff (c : Sentence → ℕ) : Desiderata c ↔ ∀ (s t : Sentence), c s < c t ↔ PlayedMore Group.child t s

The conditions say that the order a measure predicts is the one the Georgian children showed.

theorem BillEtAl2025.not_desiderata_universal_covert : ¬Desiderata Account.universal.covert

theorem BillEtAl2025.not_desiderata_bareJ_complexity : ¬Desiderata Account.bareJ.complexity

theorem BillEtAl2025.not_desiderata_bareJ_covert : ¬Desiderata Account.bareJ.covert

theorem BillEtAl2025.mu_kind_differs : (muParticle Language.georgian).morph.kind = Morphology.Morph.Kind.bound Morphology.Morph.Position.after Morphology.Morph.Attachment.clitic ∧ (muParticle Language.hungarian).morph.kind = Morphology.Morph.Kind.free

The paper's third condition asks for Hungarian μ to be less complex than Georgian μ, and its morphological route is that Georgian -c is a bound clitic where Hungarian is is free ([Cla17]).

The act-out task

@[reducible, inline]

abbrev BillEtAl2025.Object : Type

A trial shows three objects, of which the test sentence mentions two.

Equations

• BillEtAl2025.Object = Fin BillEtAl2025.objectsPerTrial

instance BillEtAl2025.instNeZeroNatObjectsPerTrial_studies : NeZero objectsPerTrial

@[reducible, inline]

abbrev BillEtAl2025.EndState : Type

An end state of a trial is the set of objects on the table.

Equations

• BillEtAl2025.EndState = Finset BillEtAl2025.Object

def BillEtAl2025.mentioned : Finset Object

The test sentence mentions the first two objects.

Equations

• BillEtAl2025.mentioned = {0, 1}

def BillEtAl2025.onTable (o : Object) : Set EndState

The proposition that an object is on the table, the alternative to the test sentence that names it alone.

Equations

• BillEtAl2025.onTable o = {st : BillEtAl2025.EndState | o ∈ st}

@[instance_reducible]

instance BillEtAl2025.instDecidablePredEndStateMemSetOnTable (o : Object) : DecidablePred fun (x : EndState) => x ∈ onTable o

Equations

• BillEtAl2025.instDecidablePredEndStateMemSetOnTable o st = BillEtAl2025.instDecidablePredEndStateMemSetOnTable._aux_1 o st

def BillEtAl2025.BasicTrue (st : EndState) : Prop

An end state meets the basic truth conditions of the test sentence when each mentioned object is on the table.

Equations

• BillEtAl2025.BasicTrue st = (BillEtAl2025.mentioned ⊆ st)

@[instance_reducible]

instance BillEtAl2025.instDecidablePredEndStateBasicTrue : DecidablePred BasicTrue

Equations

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

theorem BillEtAl2025.not_basicTrue_singleton : ¬BasicTrue {0}

theorem BillEtAl2025.basicTrue_iff_conjunction {j : Coordinator} (hj : j.role = Coordinator.Role.conjunctive) (st : EndState) : BasicTrue st ↔ j.denote {MitrovicSauerland2016.mu (MitrovicSauerland2016.shift 0), MitrovicSauerland2016.mu (MitrovicSauerland2016.shift 1)} fun (x : Object) => x ∈ st

The decomposition, a conjunctive J over the μ phrases of the shifted conjuncts, computes the basic truth conditions of is on the table.

def BillEtAl2025.Accurate (st : EndState) : Prop

An end state is accurate when it matches the exhaustified sentence, the basic truth conditions with every innocently excludable alternative naming one object denied.

Equations

• BillEtAl2025.Accurate st = (st ∈ Exhaustification.exhIE (Set.range BillEtAl2025.onTable) {st : BillEtAl2025.EndState | BillEtAl2025.BasicTrue st})

theorem BillEtAl2025.accurate_iff (st : EndState) : Accurate st ↔ st = mentioned

The accurate end state has the mentioned objects and nothing else on the table.

@[instance_reducible]

instance BillEtAl2025.instDecidablePredEndStateAccurate : DecidablePred Accurate

Equations

• BillEtAl2025.instDecidablePredEndStateAccurate st = decidable_of_iff' (st = BillEtAl2025.mentioned) ⋯

theorem BillEtAl2025.Accurate.basicTrue {st : EndState} (h : Accurate st) : BasicTrue st

def BillEtAl2025.errorKind (st : EndState) : ErrorKind

The kind of an inaccurate end state, which has an unmentioned object on the table, or else exactly one of the mentioned objects, or else neither.

Equations

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

theorem BillEtAl2025.errorKind_eq_neitherMentioned_iff {st : EndState} (h : ¬Accurate st) : errorKind st = ErrorKind.neitherMentioned ↔ st = ∅

An error of the third kind has an empty table, since nothing unmentioned is there, nor exactly one mentioned object, and the state is not the accurate one.

theorem BillEtAl2025.errorKind_surjOn : Set.SurjOn errorKind {st : EndState | ¬Accurate st} Set.univ

Each kind of error is the kind of some inaccurate end state.