Belk, Neeleman and Philip (2023): What Divides, and What Unites, Right-Node Raising

Right-node raising (John likes, and Mary dislikes, opera) shows properties of ellipsis, such as morphological mismatches and vehicle change, and properties of multidominance, such as cumulative agreement and internal readings of same. Belk, Neeleman and Philip argue that it comes from either source, and that one pruning rule at PF unites the two. The rule removes a branch of the first conjunct when a corresponding branch of the second can stand in for it without disturbing the first conjunct's word order. Applied to a branch pointing to multidominated material, pruning is forced, since the structure could not otherwise be linearized without crossing branches; applied to a branch with a counterpart of its own, it leaves an orphan that goes unrealized, which is ellipsis. Forced pruning comes first, so a constituent elided in the first conjunct can contain a multidominated pivot only at its right edge, and a finite pivot, which ellipsis cannot create, contains no further pivot.

Main statements

• licensed_rnrMD, licensed_rnrE, not_licensed_gapBeforePP: multidominance and ellipsis derive the same right-node raising, and neither leaves a gap before other material of the first conjunct.
• licensed_pieBeforePim, not_licensed_pimBeforePie: inside an elided pivot a multidominated pivot may follow material that shows ellipsis, but not precede it.
• pivotOnset_nonfinite, pivotOnset_finite: a nonfinite pivot has derivations with the break before the auxiliary, the verb or the prepositional phrase; a finite pivot has only the first.

Implementation notes

• A derivation is a planar syntactic object, multidominated material shared, with its forced and its free prunings, each pairing a pruned branch of the first conjunct with its proxy in the second. That the conjuncts are parallel, a condition the paper states in focus semantics, is assumed of the pairing.
• The coordinator and the matrix clauses of the paper's examples are left out, so a string is the conjuncts' words.
• A multidominated pivot requires a prosodic break at its onset, before its first word.

References

• Z. Belk, A. Neeleman and J. Philip, What divides, and what unites, right-node raising (2023)
• C. Wilder, Right node raising and the LCA (1999)

Pruning

structure BelkNeelemanPhilip2023.Derivation : Type

A derivation of right-node raising is a coordination, the first conjunct at [0] and the second at [1], with the branches it prunes, each paired with its proxy in the second conjunct: first the branches to multidominated material, then the free ones.

• input : Minimalist.PlanarSyntacticObject

  The coordination, multidominated material shared.

• forced : List (Core.Order.TreePath × Core.Order.TreePath)

  The branches to multidominated material, with their proxies.

• free : List (Core.Order.TreePath × Core.Order.TreePath)

  The branches whose material goes unrealized, with their proxies.

def BelkNeelemanPhilip2023.Precedes (x y : Core.Order.TreePath) : Prop

x precedes y in the linear order of a tree, lexicographically by address.

Equations

• BelkNeelemanPhilip2023.Precedes x y = (x.toList < y.toList)

@[instance_reducible]

instance BelkNeelemanPhilip2023.instDecidablePrecedes (x y : Core.Order.TreePath) : Decidable (Precedes x y)

Equations

• BelkNeelemanPhilip2023.instDecidablePrecedes x y = BelkNeelemanPhilip2023.instDecidablePrecedes._aux_1 x y

def BelkNeelemanPhilip2023.realizedAt (P : List (Core.Order.TreePath × Core.Order.TreePath)) (x : Core.Order.TreePath) : Core.Order.TreePath

Where material of the first conjunct at x is realized once the branches P are pruned: inside a pruned branch, at the corresponding position under its proxy.

Equations

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

def BelkNeelemanPhilip2023.MayPrune (t : Minimalist.PlanarSyntacticObject) (P : List (Core.Order.TreePath × Core.Order.TreePath)) (p q : Core.Order.TreePath) : Prop

The pruning rule (86). After the prunings P, the branch at p may be pruned with proxy q when p lies inside the first conjunct and q inside the second, and the proxy's yield satisfies the ordering statements of p's yield in the first conjunct: pronounced material of the first conjunct that precedes p is realized before q, and material that follows p after it.

Equations

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

@[instance_reducible]

instance BelkNeelemanPhilip2023.instDecidableMayPrune (t : Minimalist.PlanarSyntacticObject) (P : List (Core.Order.TreePath × Core.Order.TreePath)) (p q : Core.Order.TreePath) : Decidable (MayPrune t P p q)

Equations

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

def BelkNeelemanPhilip2023.Derivation.prunings (d : Derivation) : List (Core.Order.TreePath × Core.Order.TreePath)

All prunings, the forced ones first.

Equations

• d.prunings = d.forced ++ d.free

def BelkNeelemanPhilip2023.Derivation.Licensed (d : Derivation) : Prop

A derivation is licensed when each pruning obeys (86) given the ones before it; when forced pruning removes branches to multidominated material, the same constituent as their proxies, and free pruning branches with a counterpart of their own and no finite head, since a finite pivot cannot be created through ellipsis (26); and when, as the No-Tangling Condition requires, no multidominated token keeps a branch in the first conjunct.

Equations

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

@[instance_reducible]

instance BelkNeelemanPhilip2023.Derivation.instDecidableLicensed (d : Derivation) : Decidable d.Licensed

Equations

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

def BelkNeelemanPhilip2023.Derivation.yield (d : Derivation) : List Minimalist.LexicalItem.Token

The realized tokens, left to right, are those outside every pruned branch.

Equations

• d.yield = List.filterMap (fun (x : Core.Order.TreePath × Minimalist.LexicalItem.Token) => if ∀ pq ∈ d.prunings, ¬pq.1 ≤ x.1 then some x.2 else none) (Minimalist.tokenList ↑d.input)

def BelkNeelemanPhilip2023.Derivation.phon (d : Derivation) : List String

The realized words, left to right.

Equations

• d.phon = List.filterMap (fun (x : Minimalist.LexicalItem.Token) => x.item.phonForm?) d.yield

def BelkNeelemanPhilip2023.Derivation.pivotOnset (d : Derivation) : Option String

The first word of the first multidominated pivot, where a prosodic break falls.

Equations

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

Multidominance and ellipsis (§§1, 7)

def BelkNeelemanPhilip2023.john : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.john = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "John", id := 1 }

def BelkNeelemanPhilip2023.likes : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.likes = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.D] "likes", id := 2 }

def BelkNeelemanPhilip2023.mary : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.mary = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "Mary", id := 3 }

def BelkNeelemanPhilip2023.dislikes : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.dislikes = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.D] "dislikes", id := 4 }

def BelkNeelemanPhilip2023.opera : Minimalist.LexicalItem.Token

Opera, and a second token of it.

Equations

• BelkNeelemanPhilip2023.opera = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "opera", id := 5 }

def BelkNeelemanPhilip2023.opera' : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.opera' = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "opera", id := 6 }

def BelkNeelemanPhilip2023.likesDislikes (x y : Minimalist.PlanarSyntacticObject) : Minimalist.PlanarSyntacticObject

[John likes x] and [Mary dislikes y].

Equations

• BelkNeelemanPhilip2023.likesDislikes x y = ↑BelkNeelemanPhilip2023.john * (↑BelkNeelemanPhilip2023.likes * x) * (↑BelkNeelemanPhilip2023.mary * (↑BelkNeelemanPhilip2023.dislikes * y))

def BelkNeelemanPhilip2023.rnrMD : Derivation

Multidominance (84) puts one opera under both verbs and prunes the first branch (85).

Equations

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

def BelkNeelemanPhilip2023.rnrE : Derivation

Ellipsis (88) has an opera in each conjunct and prunes the first, leaving it unrealized.

Equations

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

def BelkNeelemanPhilip2023.leftNodeMD : Derivation

The gap in the second conjunct (89), by multidominance and by ellipsis.

Equations

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

def BelkNeelemanPhilip2023.leftNodeE : Derivation

Equations

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

theorem BelkNeelemanPhilip2023.phon_rnrMD : rnrMD.phon = ["John", "likes", "Mary", "dislikes", "opera"]

theorem BelkNeelemanPhilip2023.phon_rnrE : rnrE.phon = rnrMD.phon

theorem BelkNeelemanPhilip2023.licensed_rnrMD : rnrMD.Licensed

Both derivations of right-node raising are licensed.

theorem BelkNeelemanPhilip2023.licensed_rnrE : rnrE.Licensed

theorem BelkNeelemanPhilip2023.not_licensed_leftNode : ¬leftNodeMD.Licensed ∧ ¬leftNodeE.Licensed ∧ ¬{ input := rnrMD.input, forced := [], free := [] }.Licensed

Neither derives a gap in the second conjunct (89), and multidominance without pruning tangles.

def BelkNeelemanPhilip2023.bought : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.bought = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.D] "bought", id := 7 }

def BelkNeelemanPhilip2023.forMary : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.forMary = { item := Minimalist.LexicalItem.of Minimalist.Cat.P [] "for Mary", id := 8 }

def BelkNeelemanPhilip2023.bill : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.bill = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "Bill", id := 9 }

def BelkNeelemanPhilip2023.wrapped : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.wrapped = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.D] "wrapped", id := 10 }

def BelkNeelemanPhilip2023.aBook : Minimalist.LexicalItem.Token

A book about opera, and a second token of it.

Equations

• BelkNeelemanPhilip2023.aBook = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "a book about opera", id := 11 }

def BelkNeelemanPhilip2023.aBook' : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.aBook' = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "a book about opera", id := 12 }

def BelkNeelemanPhilip2023.boughtWrapped (x y : Minimalist.PlanarSyntacticObject) : Minimalist.PlanarSyntacticObject

[John [[bought x] for Mary]] and [Bill [wrapped y]] (91).

Equations

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

theorem BelkNeelemanPhilip2023.not_licensed_gapBeforePP : ¬{ input := boughtWrapped ↑aBook ↑aBook', forced := [], free := [({ toList := [0, 1, 0, 1] }, { toList := [1, 1, 1] })] }.Licensed ∧ ¬{ input := boughtWrapped ↑aBook ↑aBook, forced := [({ toList := [0, 1, 0, 1] }, { toList := [1, 1, 1] })], free := [] }.Licensed

Material of the first conjunct follows the gap (90), so neither pruning the first object (91a) nor the branch to a shared object (91b) is licensed.

def BelkNeelemanPhilip2023.flattered : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.flattered = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.D] "flattered", id := 13 }

def BelkNeelemanPhilip2023.disparaged : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.disparaged = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.D] "disparaged", id := 14 }

def BelkNeelemanPhilip2023.excessively : Minimalist.LexicalItem.Token

Excessively, and a second token of it, and a second John.

Equations

• BelkNeelemanPhilip2023.excessively = { item := Minimalist.LexicalItem.of Minimalist.Cat.A [] "excessively", id := 15 }

def BelkNeelemanPhilip2023.excessively' : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.excessively' = { item := Minimalist.LexicalItem.of Minimalist.Cat.A [] "excessively", id := 16 }

def BelkNeelemanPhilip2023.john' : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.john' = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "John", id := 17 }

def BelkNeelemanPhilip2023.flatteredDisparaged (x y x' y' : Minimalist.LexicalItem.Token) : Minimalist.PlanarSyntacticObject

[Mary [[flattered x] y]] and [Bill [[disparaged x'] y']] (92).

Equations

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

def BelkNeelemanPhilip2023.twoPivotsE : Derivation

Two pivots, by ellipsis (92a) or multidominance (92b), pruning the adverb's branch before the object's (93).

Equations

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

def BelkNeelemanPhilip2023.twoPivotsMD : Derivation

Equations

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

theorem BelkNeelemanPhilip2023.licensed_twoPivots : twoPivotsE.phon = ["Mary", "flattered", "Bill", "disparaged", "John", "excessively"] ∧ twoPivotsMD.phon = twoPivotsE.phon ∧ twoPivotsE.Licensed ∧ twoPivotsMD.Licensed ∧ ¬{ input := twoPivotsE.input, forced := [], free := twoPivotsE.free.reverse }.Licensed

Both derive Mary flattered, and Bill disparaged, John excessively; pruning the object first is not licensed, since the adverb would still follow it in the first conjunct.

Ellipsis before multidominance (§5)

def BelkNeelemanPhilip2023.she : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.she = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "she", id := 18 }

def BelkNeelemanPhilip2023.isGoingTo : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.isGoingTo = { item := Minimalist.LexicalItem.of Minimalist.Cat.T [Minimalist.Cat.V] "is going to", id := 19 }

def BelkNeelemanPhilip2023.ryo : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.ryo = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "Ryo", id := 20 }

def BelkNeelemanPhilip2023.willSoon : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.willSoon = { item := Minimalist.LexicalItem.of Minimalist.Cat.T [Minimalist.Cat.V] "will soon", id := 21 }

def BelkNeelemanPhilip2023.showV : Minimalist.LexicalItem.Token

Show, and a second token of it.

Equations

• BelkNeelemanPhilip2023.showV = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.D, Minimalist.Cat.D] "show", id := 22 }

def BelkNeelemanPhilip2023.showV' : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.showV' = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.D, Minimalist.Cat.D] "show", id := 23 }

def BelkNeelemanPhilip2023.supervisor : Minimalist.LexicalItem.Token

The objects of (58), Ava's supervisor and the same paper, and of (61), the same person and Ava's paper, each with a second token.

Equations

• BelkNeelemanPhilip2023.supervisor = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "Ava's supervisor", id := 24 }

def BelkNeelemanPhilip2023.supervisor' : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.supervisor' = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "Ava's supervisor", id := 25 }

def BelkNeelemanPhilip2023.samePaper : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.samePaper = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "the same paper", id := 26 }

def BelkNeelemanPhilip2023.samePerson : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.samePerson = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "the same person", id := 42 }

def BelkNeelemanPhilip2023.avasPaper : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.avasPaper = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "Ava's paper", id := 43 }

def BelkNeelemanPhilip2023.avasPaper' : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.avasPaper' = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "Ava's paper", id := 44 }

def BelkNeelemanPhilip2023.showVP (x y x' y' : Minimalist.LexicalItem.Token) : Minimalist.PlanarSyntacticObject

[she [is going to [show [x y]]]] and [Ryo [will soon [show [x' y']]]] (58), (61).

Equations

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

def BelkNeelemanPhilip2023.pieBeforePim : Derivation

In (58) the verb phrase is an elided pivot, the indirect object showing vehicle change, and the direct object at its right edge a multidominated pivot.

Equations

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

def BelkNeelemanPhilip2023.pimBeforePie : Derivation

In (61) the multidominated pivot, the indirect object, precedes the elided direct object.

Equations

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

theorem BelkNeelemanPhilip2023.phon_pieBeforePim : pieBeforePim.phon = ["she", "is going to", "Ryo", "will soon", "show", "Ava's supervisor", "the same paper"]

theorem BelkNeelemanPhilip2023.licensed_pieBeforePim : pieBeforePim.Licensed ∧ pieBeforePim.pivotOnset = some "the same paper"

A multidominated pivot may stand at the right edge of an elided pivot (49), with the prosodic break before it.

theorem BelkNeelemanPhilip2023.not_licensed_pimBeforePie : ¬pimBeforePie.Licensed ∧ ¬MayPrune pimBeforePie.input [] { toList := [0, 1, 1, 1, 0] } { toList := [1, 1, 1, 1, 0] }

But not before material of the elided pivot, since forced pruning comes first, while the direct object still follows the indirect one in the first conjunct.

Finite and nonfinite pivots (§5)

def BelkNeelemanPhilip2023.she' : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.she' = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "she", id := 28 }

def BelkNeelemanPhilip2023.will : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.will = { item := Minimalist.LexicalItem.of Minimalist.Cat.T [Minimalist.Cat.V] "will", id := 29 }

def BelkNeelemanPhilip2023.will' : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.will' = { item := Minimalist.LexicalItem.of Minimalist.Cat.T [Minimalist.Cat.V] "will", id := 30 }

def BelkNeelemanPhilip2023.could : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.could = { item := Minimalist.LexicalItem.of Minimalist.Cat.T [Minimalist.Cat.V] "could", id := 31 }

def BelkNeelemanPhilip2023.haveAux : Minimalist.LexicalItem.Token

The perfect auxiliary have, and a second one.

Equations

• BelkNeelemanPhilip2023.haveAux = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.V] "have", id := 32 }

def BelkNeelemanPhilip2023.haveAux' : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.haveAux' = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.V] "have", id := 33 }

def BelkNeelemanPhilip2023.traveled : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.traveled = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.P] "traveled", id := 34 }

def BelkNeelemanPhilip2023.traveled' : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.traveled' = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.P] "traveled", id := 35 }

def BelkNeelemanPhilip2023.travel : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.travel = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.P] "travel", id := 36 }

def BelkNeelemanPhilip2023.travel' : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.travel' = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.P] "travel", id := 37 }

def BelkNeelemanPhilip2023.toP : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.toP = { item := Minimalist.LexicalItem.of Minimalist.Cat.P [Minimalist.Cat.D] "to", id := 38 }

def BelkNeelemanPhilip2023.the : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.the = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [Minimalist.Cat.N] "the", id := 39 }

def BelkNeelemanPhilip2023.same : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.same = { item := Minimalist.LexicalItem.of Minimalist.Cat.A [] "same", id := 40 }

def BelkNeelemanPhilip2023.country : Minimalist.LexicalItem.Token

Equations

• BelkNeelemanPhilip2023.country = { item := Minimalist.LexicalItem.of Minimalist.Cat.N [] "country", id := 41 }

def BelkNeelemanPhilip2023.samePivot : Minimalist.PlanarSyntacticObject

The pivot to the same country, whose internal reading requires it to be multidominated.

Equations

• BelkNeelemanPhilip2023.samePivot = ↑BelkNeelemanPhilip2023.toP * (↑BelkNeelemanPhilip2023.the * (↑BelkNeelemanPhilip2023.same * ↑BelkNeelemanPhilip2023.country))

def BelkNeelemanPhilip2023.shareAuxP : Derivation

Example (51) with the auxiliary phrase multidominated, and no ellipsis.

Equations

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

def BelkNeelemanPhilip2023.shareVP : Derivation

Example (51) with the verb phrase multidominated and the first auxiliary phrase elided.

Equations

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

def BelkNeelemanPhilip2023.sharePP : Derivation

Example (51) with only the prepositional phrase multidominated.

Equations

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

def BelkNeelemanPhilip2023.derivations51 : List Derivation

The three derivations of (51).

Equations

• BelkNeelemanPhilip2023.derivations51 = [BelkNeelemanPhilip2023.shareAuxP, BelkNeelemanPhilip2023.shareVP, BelkNeelemanPhilip2023.sharePP]

theorem BelkNeelemanPhilip2023.phon_derivations51 (d : Derivation) : d ∈ derivations51 → d.phon = ["she", "will", "she", "could", "have", "traveled", "to", "the", "same", "country"]

theorem BelkNeelemanPhilip2023.pivotOnset_nonfinite : (∀ d ∈ derivations51, d.Licensed) ∧ List.map (fun (x : Derivation) => x.pivotOnset) derivations51 = [some "have", some "traveled", some "to"]

The nonfinite pivot of (51) has three licensed derivations, which put the prosodic break before have, traveled or to.

def BelkNeelemanPhilip2023.finiteShareT : Derivation

Example (52), its finite pivot multidominated.

Equations

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

def BelkNeelemanPhilip2023.finiteShareVP : Derivation

Its rivals with the verb phrase or the prepositional phrase multidominated and the rest of the finite pivot elided.

Equations

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

def BelkNeelemanPhilip2023.finiteSharePP : Derivation

Equations

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

theorem BelkNeelemanPhilip2023.pivotOnset_finite : finiteShareT.Licensed ∧ finiteShareT.pivotOnset = some "will" ∧ ¬finiteShareVP.Licensed ∧ ¬finiteSharePP.Licensed

The finite pivot of (52) is multidominated as a whole, so the prosodic break cannot shift rightward: its rivals would create a finite pivot through ellipsis (26).

theorem BelkNeelemanPhilip2023.mayPrune_finiteRivals (d : Derivation) : d ∈ [finiteShareVP, finiteSharePP] → ∀ x ∈ d.prunings.zipIdx, MayPrune d.input (List.take x.2 d.prunings) x.1.1 x.1.2

The rivals obey the pruning rule at every step; only (26) excludes them.