Zeijlstra (2012): There Is Only One Way to Agree

This file formalizes [Zei12]'s proposal that Agree applies upward only: an element carrying an uninterpretable feature is checked by the closest c-commanding element carrying the matching interpretable feature (IsUpwardGoalIn), reversing the direction of [Cho00]'s Agree, and several such elements may be checked by one goal at once (MultipleAgree). The evidence is the concord phenomena, Negative Concord and Sequence of Tense, whose configurations place one interpretable feature above one or more uninterpretable ones. In Sequence of Tense, an abstract past operator carries [iPAST] and every finite past morpheme, the matrix verb included, carries a vacuous [uPAST]; the matrix and the subordinate verb of John said Mary was ill both Agree upward with the operator (sot_multipleAgree), which no downward-probing Agree could establish (sot_not_downward). Agree across a phase boundary requires the phase edge to participate: the corollary of phase theory that distinguishes the two phenomena, since the embedding complementizer carries an uninterpretable tense feature but no uninterpretable negative feature, so Sequence of Tense crosses the clause boundary (sot_licit) while Negative Concord does not (nc_across_cp_illicit, nc_clausemate_licit).

Implementation notes

• Feature bearers are given by predicates on the leaves of a syntactic object, as the paper annotates its bracketings; the lexical items themselves carry only categories and selection.
• The phase-edge condition is stated for a phase head leaf through the substrate's phase domains: when the probe lies in the phase interior and the goal outside the phase, some element of the phase edge must carry the uninterpretable feature.
• The subordinate verb selects its subject as well as its predicate, so that the clause is a constituent the complementizer selects and projects over; the paper's bracketings leave the subject's position open.
• The semantics of the subordinate past morpheme as a relative non-future, which the paper leaves to later work, is not formalized.

References

• [Zei12]
• [Cho00]
• [Cho01]

Upward Agree

def Zeijlstra2012.IsUpwardGoalIn (root probe goal : Minimalist.SyntacticObject) (pred : Minimalist.SyntacticObject → Prop) : Prop

In upward Agree, goal, carrying the interpretable feature marked by pred, c-commands the uninterpretable probe and is the closest such element, no other pred-node c-commanding the probe being asymmetrically c-commanded by it.

Equations

• Zeijlstra2012.IsUpwardGoalIn root probe goal pred = (root.CCommands goal probe ∧ pred goal ∧ ∀ x ∈ root.terms, root.CCommands x probe → pred x → ¬root.AsymmCCommands goal x)

@[instance_reducible]

instance Zeijlstra2012.instDecidableIsUpwardGoalInOfDecidablePredSyntacticObject {pred : Minimalist.SyntacticObject → Prop} [DecidablePred pred] (root probe goal : Minimalist.SyntacticObject) : Decidable (IsUpwardGoalIn root probe goal pred)

Equations

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

def Zeijlstra2012.MultipleAgree (root goal : Minimalist.SyntacticObject) (probes : List Minimalist.SyntacticObject) (pred : Minimalist.SyntacticObject → Prop) : Prop

In Multiple Agree every probe in the list is checked by the same goal.

Equations

• Zeijlstra2012.MultipleAgree root goal probes pred = ∀ p ∈ probes, Zeijlstra2012.IsUpwardGoalIn root p goal pred

@[instance_reducible]

instance Zeijlstra2012.instDecidableMultipleAgreeOfDecidablePredSyntacticObject {pred : Minimalist.SyntacticObject → Prop} [DecidablePred pred] (root goal : Minimalist.SyntacticObject) (probes : List Minimalist.SyntacticObject) : Decidable (MultipleAgree root goal probes pred)

Equations

• Zeijlstra2012.instDecidableMultipleAgreeOfDecidablePredSyntacticObject root goal probes = Zeijlstra2012.instDecidableMultipleAgreeOfDecidablePredSyntacticObject._aux_1 root goal probes

def Zeijlstra2012.EdgeParticipates (root probe goal : Minimalist.SyntacticObject) (uF : Minimalist.SyntacticObject → Prop) (ℓ : Minimalist.LexicalItem.Token) : Prop

The phase-edge condition on Agree across a phase: with ℓ a phase head, a probe in the phase interior may Agree with a goal outside the phase only if an element of the phase edge carries the uninterpretable feature uF too.

Equations

• Zeijlstra2012.EdgeParticipates root probe goal uF ℓ = (probe ∈ root.phaseInterior ℓ → goal ∉ root.phase ℓ → ∃ e ∈ root.phaseEdge ℓ, uF e)

@[instance_reducible]

instance Zeijlstra2012.instDecidableEdgeParticipatesOfDecidablePredSyntacticObject {uF : Minimalist.SyntacticObject → Prop} [DecidablePred uF] (root probe goal : Minimalist.SyntacticObject) (ℓ : Minimalist.LexicalItem.Token) : Decidable (EdgeParticipates root probe goal uF ℓ)

Equations

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

Sequence of Tense

def Zeijlstra2012.opPast : Minimalist.PlanarSyntacticObject

The abstract past operator carrying [iPAST].

Equations

• Zeijlstra2012.opPast = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.T [Minimalist.Cat.V] "Op[PAST]", id := 1 }

def Zeijlstra2012.john : Minimalist.PlanarSyntacticObject

Equations

• Zeijlstra2012.john = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "John", id := 2 }

def Zeijlstra2012.said : Minimalist.PlanarSyntacticObject

The matrix verb, with its own vacuous [uPAST].

Equations

• Zeijlstra2012.said = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.C] "said", id := 3 }

def Zeijlstra2012.thatC : Minimalist.PlanarSyntacticObject

The embedding complementizer, carrying [uT].

Equations

• Zeijlstra2012.thatC = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.C [Minimalist.Cat.V] "that", id := 4 }

def Zeijlstra2012.mary : Minimalist.PlanarSyntacticObject

Equations

• Zeijlstra2012.mary = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "Mary", id := 5 }

def Zeijlstra2012.was : Minimalist.PlanarSyntacticObject

The subordinate verb, with [uPAST], selecting its predicate and its subject.

Equations

• Zeijlstra2012.was = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.A, Minimalist.Cat.D] "was", id := 6 }

def Zeijlstra2012.ill : Minimalist.PlanarSyntacticObject

Equations

• Zeijlstra2012.ill = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.A [] "ill", id := 7 }

def Zeijlstra2012.sot : Minimalist.PlanarSyntacticObject

John said Mary was ill, with the past operator above both verbs.

Equations

• Zeijlstra2012.sot = {Zeijlstra2012.john, {Zeijlstra2012.opPast, {Zeijlstra2012.said, {Zeijlstra2012.thatC, {Zeijlstra2012.mary, {Zeijlstra2012.was, Zeijlstra2012.ill}}}}}}

def Zeijlstra2012.iPast (s : Minimalist.SyntacticObject) : Prop

The bearers of [iPAST].

Equations

• Zeijlstra2012.iPast s = (s = ↑Zeijlstra2012.opPast)

def Zeijlstra2012.uPast (s : Minimalist.SyntacticObject) : Prop

The bearers of [uPAST] or [uT] are both finite verbs and the complementizer.

Equations

• Zeijlstra2012.uPast s = (s = ↑Zeijlstra2012.said ∨ s = ↑Zeijlstra2012.was ∨ s = ↑Zeijlstra2012.thatC)

theorem Zeijlstra2012.sot_multipleAgree : MultipleAgree ↑sot ↑opPast [↑said, ↑was] iPast

Both past morphemes Agree upward with the single past operator.

theorem Zeijlstra2012.sot_not_downward : ¬(↑sot).CCommands ↑said ↑opPast ∧ ¬(↑sot).CCommands ↑was ↑opPast

Neither verb c-commands the operator, so no downward-probing Agree relates them.

theorem Zeijlstra2012.sot_licit : (↑sot).WithinComplement { item := Minimalist.LexicalItem.of Minimalist.Cat.C [Minimalist.Cat.V] "that", id := 4 } ↑was ∧ ¬(↑sot).WithinProjection { item := Minimalist.LexicalItem.of Minimalist.Cat.C [Minimalist.Cat.V] "that", id := 4 } ↑opPast ∧ EdgeParticipates (↑sot) (↑was) (↑opPast) uPast { item := Minimalist.LexicalItem.of Minimalist.Cat.C [Minimalist.Cat.V] "that", id := 4 }

Sequence of Tense crosses the clause boundary: the subordinate verb sits in the interior of the phase headed by the complementizer, which itself carries an uninterpretable tense feature and so lies in the participating edge.

Negative Concord

def Zeijlstra2012.gianni : Minimalist.PlanarSyntacticObject

Equations

• Zeijlstra2012.gianni = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "Gianni", id := 11 }

def Zeijlstra2012.non : Minimalist.PlanarSyntacticObject

The negative marker carrying [iNEG].

Equations

• Zeijlstra2012.non = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.Neg [Minimalist.Cat.T] "non", id := 12 }

def Zeijlstra2012.ha : Minimalist.PlanarSyntacticObject

Equations

• Zeijlstra2012.ha = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.T [Minimalist.Cat.V] "ha", id := 13 }

def Zeijlstra2012.detto : Minimalist.PlanarSyntacticObject

Equations

• Zeijlstra2012.detto = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.D] "detto", id := 14 }

def Zeijlstra2012.dettoC : Minimalist.PlanarSyntacticObject

Equations

• Zeijlstra2012.dettoC = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.C] "detto", id := 15 }

def Zeijlstra2012.niente : Minimalist.PlanarSyntacticObject

Equations

• Zeijlstra2012.niente = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.D [Minimalist.Cat.P] "niente", id := 16 }

def Zeijlstra2012.a : Minimalist.PlanarSyntacticObject

Equations

• Zeijlstra2012.a = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.P [Minimalist.Cat.D] "a", id := 17 }

def Zeijlstra2012.nessuno : Minimalist.PlanarSyntacticObject

Equations

• Zeijlstra2012.nessuno = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "nessuno", id := 18 }

def Zeijlstra2012.che : Minimalist.PlanarSyntacticObject

The embedding complementizer, without any negative feature.

Equations

• Zeijlstra2012.che = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.C [Minimalist.Cat.T] "che", id := 19 }

def Zeijlstra2012.ha₂ : Minimalist.PlanarSyntacticObject

Equations

• Zeijlstra2012.ha₂ = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.T [Minimalist.Cat.V] "ha", id := 20 }

def Zeijlstra2012.telefonato : Minimalist.PlanarSyntacticObject

Equations

• Zeijlstra2012.telefonato = ↑{ item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.P] "telefonato", id := 21 }

def Zeijlstra2012.ncClausemate : Minimalist.PlanarSyntacticObject

Gianni non ha detto niente a nessuno has two n-words under one negative marker.

Equations

• Zeijlstra2012.ncClausemate = {Zeijlstra2012.gianni, {Zeijlstra2012.non, {Zeijlstra2012.ha, {Zeijlstra2012.detto, {Zeijlstra2012.niente, {Zeijlstra2012.a, Zeijlstra2012.nessuno}}}}}}

def Zeijlstra2012.ncAcrossCP : Minimalist.PlanarSyntacticObject

Gianni non ha detto che ha telefonato a nessuno has the n-word inside an embedded clause.

Equations

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

def Zeijlstra2012.iNeg (s : Minimalist.SyntacticObject) : Prop

The bearers of [iNEG].

Equations

• Zeijlstra2012.iNeg s = (s = ↑Zeijlstra2012.non)

def Zeijlstra2012.uNeg (s : Minimalist.SyntacticObject) : Prop

The bearers of [uNEG], the n-words.

Equations

• Zeijlstra2012.uNeg s = (s = ↑Zeijlstra2012.niente ∨ s = ↑Zeijlstra2012.nessuno)

theorem Zeijlstra2012.nc_clausemate_multipleAgree : MultipleAgree ↑ncClausemate ↑non [↑niente, ↑nessuno] iNeg

Both n-words Agree upward with the negative marker.

theorem Zeijlstra2012.nc_clausemate_licit (x : Minimalist.SyntacticObject) : x ∈ (↑ncClausemate).terms → x.cat? ≠ some Minimalist.Cat.C

Within the clause no complementizer heads a phase, so no phase edge intervenes.

theorem Zeijlstra2012.nc_across_cp_illicit : ¬EdgeParticipates (↑ncAcrossCP) (↑nessuno) (↑non) uNeg { item := Minimalist.LexicalItem.of Minimalist.Cat.C [Minimalist.Cat.T] "che", id := 19 }

Across the embedded clause the complementizer carries no negative feature, so the phase edge does not participate and the concord relation is blocked.