Collins 2005: a smuggling approach to the passive in English

The principles-and-parameters passive lets the suffix -en absorb accusative Case and the external θ-role, so that the agent of The book was written by John is Merged nowhere near where the agent of the active is Merged, against the uniformity of θ-assignment. Collins returns to Syntactic Structures on this point: the external argument is Merged in Spec,vP in the passive exactly as in the active, the participle head Part takes the VP and vP takes PartP, and the verb precedes the external argument because PartP moves to the specifier of a VoiceP headed by by, a head of uninterpretable features that takes a vP complement and checks the Case that v checks in the active. That the movement is of the phrase and not of the verb's head is shown by particles and stranded prepositions, which precede the external argument and cannot follow it. The structure also orders the auxiliaries: have c-selects a participle, Voice attracts one, and a participle must be licensed by exactly one of them, which admits has seen and was seen by and excludes has seen by and was seen.

The movement is smuggling: the object inside PartP, which the external argument in Spec,vP c-commands and so shields from Infl by Relativized Minimality, is carried past it, after which the object is Infl's closest goal and raises to Spec,IP. Without the movement, or with head movement of the verb alone, the object stays behind the external argument and the passive cannot be derived; the derivation extracts the object from a moved constituent, and the paper takes Freezing not to hold of PartP movement. A PP that follows the by-phrase has evacuated PartP before the remnant fronted, so the external argument c-commands it, and a PP that precedes the by-phrase has not, so it does not: negative polarity, each … the other and Principle C line up with the position of the PP. A reflexive or a bound variable inside the fronted PartP is bound only by reconstruction, which the paper takes to be marginal, and Principle B applies as the external argument is Merged, so a coindexed pronoun inside PartP is out however PartP later moves.

The passive is a Derivation on the syntactic-object carrier under each of the three analyses, the surface strings are its externalizations, Relativized Minimality is the substrate's closest-goal relation at the stage where Infl attracts, smuggling and remnant fronting are the substrate's step predicates, and the paper's examples are the rows: rm_converges singles out PartP movement, which converges_iff_not_obeysFreezing shows the one analysis Freezing excludes, licensing_rows derives the c-command and binding judgments from surface and derivational c-command, the binding judgments being the conditions of Syntax/Binding at the levels the paper assigns them, of which the rows force Principle B's (principleB_anyStage), participle_rows the auxiliary paradigm from the licensing principle, and active_shares_vP is the θ-uniformity the analysis was built for.

Implementation notes

• Part is Cat.Asp, silent, and the verb's raising to it (8) is not modelled: the participle is the verb's leaf. Voice is by with selection stack [v], so a by-phrase over a DP is exocentric, the paper's (29). The evacuation host X of (58), AgrP or LkP for the paper, is a second Cat.Asp layer selecting PartP and the PP, so that v's selection is uniform; the object sits in Spec,VP rather than the paper's Spec,PartP. A PP enters as one leaf, and c-command of the leaf stands for c-command of the DP inside it.
• The rival analyses of (11) are the same derivation up to VoiceP: PartP movement raises the participle phrase, head movement re-Merges the verb's leaf at the root, standing in for the adjunction of (13), and the in-situ analysis raises nothing before the object moves. Convergence is whether the object is a closest D-goal for Infl at the stage where it raises; the Case side of the argument is prose.
• Principle A and bound-variable binding are evaluated at the surface, with reconstruction to any stage as the degraded option; Principle B at any stage, without the local-domain and Case-checked clauses of (83), which the monoclausal rows never exercise; Principle C at the surface, as §9 argues. The principles are the framework-neutral conditions of Syntax/Binding on the two positions, under one monoclausal configuration per level.

TODO

• The double-object (53)–(54), the ECM and CP cases of (55), (57) and (81), the Principle C data (76)–(77), the freezing and reciprocal data of §10 ((88)–(93)), the quantifier-raising data of (94)–(98), and the Kiswahili and Japanese passives of §5 are not modelled.
• The Case checking by by and by the null Voice of short passives (§4, §6) is stated in prose; nothing here derives (47).

References

• C. Collins, A Smuggling Approach to the Passive in English (2005)
• A. Barss and H. Lasnik, A Note on Anaphora and Double Objects (1986)
• G. Müller, Incomplete Category Fronting (1998)
• J. Sabel, Restrukturierung und Lokalität (1996)

The passive and its rival derivations (§2–§5)

inductive Collins2005.Analysis : Type

What places the participle before the external argument (§3, (11)–(14)): PartP moves to Spec,VoiceP, the verb alone moves to Voice, or nothing moves.

• partP : Analysis
• headMovement : Analysis
• inSitu : Analysis

@[instance_reducible]

instance Collins2005.instDecidableEqAnalysis : DecidableEq Analysis

Equations

• Collins2005.instDecidableEqAnalysis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Collins2005.instReprAnalysis.repr : Analysis → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Collins2005.instReprAnalysis : Repr Analysis

Equations

• Collins2005.instReprAnalysis = { reprPrec := Collins2005.instReprAnalysis.repr }

structure Collins2005.Clause : Type

A transitive clause: its verb, external and internal arguments, the auxiliary of its passive, and an optional third element of VP, one leaf: a particle, the complement of V with the object in Spec,VP (17), or a PP, the leaf standing in for the PP the pseudo-passive strands its preposition from.

• verb : Minimalist.LexicalItem.Token

  The verb, in its participial form.

• agent : Minimalist.LexicalItem.Token

  The external argument, Merged in Spec,vP.

• patient : Minimalist.LexicalItem.Token

  The internal argument.

• be : Minimalist.LexicalItem.Token

  The auxiliary be.

• extra : Option Minimalist.LexicalItem.Token

  A particle, stranded preposition or PP, the verb's complement with the patient in Spec,VP (17).

def Collins2005.part₀ : Minimalist.LexicalItem.Token

The participle head, silent, over the VP.

Equations

• Collins2005.part₀ = { item := Minimalist.LexicalItem.of Minimalist.Cat.Asp [Minimalist.Cat.V], id := 5 }

def Collins2005.v₀ : Minimalist.LexicalItem.Token

The light verb, over PartP and the external argument.

Equations

• Collins2005.v₀ = { item := Minimalist.LexicalItem.of Minimalist.Cat.v [Minimalist.Cat.Asp, Minimalist.Cat.D], id := 6 }

def Collins2005.by₀ : Minimalist.LexicalItem.Token

Voice, by, which takes a vP (§4).

Equations

• Collins2005.by₀ = { item := Minimalist.LexicalItem.of Minimalist.Cat.Voice [Minimalist.Cat.v] "by", id := 7 }

def Collins2005.x₀ : Minimalist.LexicalItem.Token

The host X of an evacuated PP, (58): a second participial layer over PartP that takes the PP, so that v selects the same category with or without evacuation.

Equations

• Collins2005.x₀ = { item := Minimalist.LexicalItem.of Minimalist.Cat.Asp [Minimalist.Cat.Asp, Minimalist.Cat.P], id := 8 }

def Collins2005.infl₀ : Minimalist.LexicalItem.Token

Infl.

Equations

• Collins2005.infl₀ = { item := Minimalist.LexicalItem.of Minimalist.Cat.T [], id := 9 }

def Collins2005.has₀ : Minimalist.LexicalItem.Token

The auxiliary have of the active perfect (26).

Equations

• Collins2005.has₀ = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [] "has", id := 10 }

def Collins2005.Clause.of (verb agent patient : String) (extra : Option String := none) (be : String := "was") : Clause

A clause from its words.

Equations

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

def Collins2005.Clause.vpSteps (p : Clause) : List Minimalist.Step

The VP: the verb and its object (8), or with a third element {Patient, {V, X}} (17).

Equations

• p.vpSteps = match p.extra with | some x => [Minimalist.Step.em Edge.right ↑x, Minimalist.Step.em Edge.left ↑p.patient] | none => [Minimalist.Step.em Edge.right ↑p.patient]

def Collins2005.Clause.partP (p : Clause) (evacuate : Bool) : Minimalist.PlanarSyntacticObject

The PartP at the point it fronts: over the VP, with the evacuated element's trace when it has left.

Equations

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

def Collins2005.Clause.evacuation (p : Clause) (evacuate : Bool) : List Minimalist.Step

The evacuation of the third element to Spec,XP before PartP fronts, (58a)–(58b).

Equations

• p.evacuation evacuate = match p.extra with | some x => if evacuate = true then [Minimalist.Step.em Edge.left ↑Collins2005.x₀, Minimalist.Step.im ↑x] else [] | none => []

def Collins2005.Clause.vP (p : Clause) (evacuate : Bool) : Minimalist.Derivation

The derivation through vP, the same in the active and the passive (§2): VP, PartP, the light verb and the external argument.

Equations

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

def Collins2005.Clause.voiceP (p : Clause) (evacuate : Bool) : Minimalist.Derivation

Voice Merges over vP, (30).

Equations

• p.voiceP evacuate = (p.vP evacuate).append [Minimalist.Step.em Edge.left ↑Collins2005.by₀]

def Collins2005.Clause.fronted (p : Clause) (a : Analysis) (evacuate : Bool) : Minimalist.Derivation

The three analyses: PartP to Spec,VoiceP (14), the verb to Voice (13), or nothing.

Equations

• p.fronted Collins2005.Analysis.partP evacuate = (p.voiceP evacuate).append [Minimalist.Step.im ↑(p.partP evacuate)]
• p.fronted Collins2005.Analysis.headMovement evacuate = (p.voiceP evacuate).append [Minimalist.Step.im ↑p.verb]
• p.fronted Collins2005.Analysis.inSitu evacuate = (p.voiceP evacuate).append []

def Collins2005.Clause.preRaising (p : Clause) (a : Analysis) (evacuate : Bool) : Minimalist.Derivation

The stage at which Infl attracts: the auxiliary and Infl over VoiceP.

Equations

• p.preRaising a evacuate = (p.fronted a evacuate).append [Minimalist.Step.em Edge.left ↑p.be, Minimalist.Step.em Edge.left ↑Collins2005.infl₀]

def Collins2005.Clause.passive (p : Clause) (a : Analysis) (evacuate : Bool) : Minimalist.Derivation

The passive: the object raised to Spec,IP, (22).

Equations

• p.passive a evacuate = (p.preRaising a evacuate).append [Minimalist.Step.im ↑p.patient]

def Collins2005.Clause.active (p : Clause) : Minimalist.Derivation

The active perfect (26): have and Infl over vP, and the external argument to Spec,IP.

Equations

• p.active = (p.vP false).append [Minimalist.Step.em Edge.left ↑Collins2005.has₀, Minimalist.Step.em Edge.left ↑Collins2005.infl₀, Minimalist.Step.im ↑p.agent]

def Collins2005.Clause.Converges (p : Clause) (a : Analysis) (evacuate : Bool) : Prop

The analysis converges: at the stage where Infl attracts, the object is one of its closest D-goals, so its raising violates neither the Minimal Link Condition nor Relativized Minimality (§5).

Equations

• p.Converges a evacuate = ∃ q ∈ (p.preRaising a evacuate).externalize?, (↑q).isClosestGoalIn (↑Collins2005.infl₀) (↑p.patient) (Minimalist.SyntacticObject.isLeafOf Minimalist.Cat.D)

@[instance_reducible]

instance Collins2005.Clause.instDecidableConverges (p : Clause) (a : Analysis) (evacuate : Bool) : Decidable (p.Converges a evacuate)

Equations

• p.instDecidableConverges a evacuate = id inferInstance

def Collins2005.ex9 : Clause

(9), (22), (30): The book was written by John.

Equations

• Collins2005.ex9 = Collins2005.Clause.of "written" "John" "the book"

def Collins2005.ex15 : Clause

(15): The argument was summed up by the coach.

Equations

• Collins2005.ex15 = Collins2005.Clause.of "summed" "the coach" "the argument" (some "up")

def Collins2005.ex18 : Clause

(18): John was spoken to by Mary.

Equations

• Collins2005.ex18 = Collins2005.Clause.of "spoken" "Mary" "John" (some "to")

def Collins2005.ex56 : Clause

(56): The book was given to Mary by John.

Equations

• Collins2005.ex56 = Collins2005.Clause.of "given" "John" "the book" (some "to Mary")

def Collins2005.ex23 : Clause

(23a), (26): John has seen the book.

Equations

• Collins2005.ex23 = Collins2005.Clause.of "seen" "John" "the book"

theorem Collins2005.ex9_orders : (ex9.passive Analysis.partP false).surfacePhon = ["the book", "was", "written", "by", "John"] ∧ (ex9.passive Analysis.headMovement false).surfacePhon = ["the book", "was", "written", "by", "John"] ∧ (ex9.passive Analysis.inSitu false).surfacePhon = ["the book", "was", "by", "John", "written"]

The three analyses externalize (9b), and, for the two that do not converge, (9a).

theorem Collins2005.particle_orders : (ex15.passive Analysis.partP false).surfacePhon = ["the argument", "was", "summed", "up", "by", "the coach"] ∧ (ex15.passive Analysis.headMovement false).surfacePhon = ["the argument", "was", "summed", "by", "the coach", "up"] ∧ (ex18.passive Analysis.partP false).surfacePhon = ["John", "was", "spoken", "to", "by", "Mary"] ∧ (ex18.passive Analysis.headMovement false).surfacePhon = ["John", "was", "spoken", "by", "Mary", "to"]

Particles (15) and stranded prepositions (18) tell the analyses apart: PartP movement carries them before the external argument, head movement strands them after it.

theorem Collins2005.pp_orders : (ex56.passive Analysis.partP false).surfacePhon = ["the book", "was", "given", "to Mary", "by", "John"] ∧ (ex56.passive Analysis.partP true).surfacePhon = ["the book", "was", "given", "by", "John", "to Mary"]

A PP pied-piped inside PartP precedes the by-phrase (56c); evacuated to Spec,XP before the remnant fronts, it follows it (56d).

theorem Collins2005.active_order : ex23.active.surfacePhon = ["John", "has", "seen", "the book"]

The active perfect (23a).

theorem Collins2005.active_shares_vP (p : Clause) (a : Analysis) : p.active.take (p.vP false).length = (p.passive a false).take (p.vP false).length

θ-uniformity (§2): the active and the passive share the derivation through vP, so the external argument is Merged in Spec,vP in both.

Smuggling (§5)

theorem Collins2005.partP_smuggles : (ex9.passive Analysis.partP false).IsSmugglingStep (ex9.voiceP false).length ↑ex9.patient ↑ex9.agent ∧ ¬(ex9.passive Analysis.headMovement false).IsSmugglingStep (ex9.voiceP false).length ↑ex9.patient ↑ex9.agent

PartP movement smuggles the object past the external argument, (34): the external argument c-commands the object before the step and the fronted PartP c-commands it after; the verb's head, moved alone, carries no object.

theorem Collins2005.rm_converges (a : Analysis) : ex9.Converges a false ↔ a = Analysis.partP

Relativized Minimality (§5): the object is a closest D-goal for Infl only once smuggled; in place, or with the verb moved alone, the external argument intervenes, so The book was by John written (9a) and head movement both fail.

theorem Collins2005.converges_iff_not_obeysFreezing (a : Analysis) : ex9.Converges a false ↔ ¬(ex9.passive a false).ObeysFreezing

Of the three analyses, the one that converges is the one that violates [Mul98]'s Freezing (35): the object raises out of the fronted PartP that smuggled it, so the paper assumes that Freezing does not hold of PartP movement (fn. 25).

theorem Collins2005.agent_over_patient_at_vP : ex9.active.CCommandsAt (ex9.vP false).length ↑ex9.agent ↑ex9.patient ∧ (ex9.passive Analysis.partP false).CCommandsAt (ex9.vP false).length ↑ex9.agent ↑ex9.patient

θ-uniformity in the structure: at the vP stage of the active and of the passive alike, the external argument c-commands the internal one.

theorem Collins2005.pp_remnant : (ex56.passive Analysis.partP true).IsRemnantStep (ex56.voiceP true).length

The evacuated-PP derivation (58) fronts a remnant: PartP carries the PP's trace.

By takes a vP (§4)

theorem Collins2005.by_selects_vP : (↑{↑by₀, ↑ex9.patient}).selHead = none ∧ ∃ q ∈ (ex9.voiceP false).externalize?, (↑q).selHead = some by₀

The by-phrase of (29), by the book, has no projecting head: by selects a vP, and a DP does not satisfy it; over the vP of (30) it projects.

The rows

def Collins2005.bools : List (String × Bool)

Equations

• Collins2005.bools = [("true", true), ("false", false)]

def Collins2005.Clause.ofRow (row : Datum) : Option Clause

The clause a row records.

Equations

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

Word order and convergence (§3, §5)

structure Collins2005.Order : Type

A word-order row's configuration: its clause, the analysis that derives its string, and whether the PP evacuated.

• clause : Clause

  The clause.

• analysis : Analysis

  The analysis that derives the row's string.

• evacuated : Bool

  Whether the PP evacuated PartP.

def Collins2005.Order.ofRow (row : Datum) : Option Order

The configuration a row records.

Equations

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

theorem Collins2005.order_rows (row : Datum) : row ∈ Examples.all → ∀ o ∈ Order.ofRow row, row.judgment ≠ Judgment.ungrammatical ↔ o.clause.Converges o.analysis o.evacuated

A word-order row is grammatical exactly when the analysis that derives its string converges: PartP movement does, head movement and no movement leave the external argument between Infl and the object.

C-command and binding across the by-phrase (§3, §7, §9, §10)

inductive Collins2005.Position : Type

The two positions the tests relate are the external argument and the third element of VP.

• external : Position
• pp : Position

@[instance_reducible]

instance Collins2005.instDecidableEqPosition : DecidableEq Position

Equations

• Collins2005.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Collins2005.instFintypePosition : Fintype Position

Equations

• Collins2005.instFintypePosition = { elems := { val := ↑Collins2005.Position.enumList, nodup := Collins2005.Position.enumList_nodup }, complete := Collins2005.instFintypePosition._proof_1 }

def Collins2005.instReprPosition.repr : Position → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Collins2005.instReprPosition.repr Collins2005.Position.pp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Collins2005.Position.pp")).group prec✝

@[instance_reducible]

instance Collins2005.instReprPosition : Repr Position

Equations

• Collins2005.instReprPosition = { reprPrec := Collins2005.instReprPosition.repr }

def Collins2005.Clause.at? (p : Clause) : Position → Option Minimalist.LexicalItem.Token

The leaf at a position.

Equations

• p.at? Collins2005.Position.external = some p.agent
• p.at? Collins2005.Position.pp = p.extra

inductive Collins2005.Level : Type

The level at which a binding condition is evaluated, the surface or any stage of the derivation, reconstruction included.

• surface : Level
• anyStage : Level

@[instance_reducible]

instance Collins2005.instDecidableEqLevel : DecidableEq Level

Equations

• Collins2005.instDecidableEqLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Collins2005.instReprLevel : Repr Level

Equations

• Collins2005.instReprLevel = { reprPrec := Collins2005.instReprLevel.repr }

def Collins2005.instReprLevel.repr : Level → ℕ → Std.Format

Equations

• Collins2005.instReprLevel.repr Collins2005.Level.surface prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Collins2005.Level.surface")).group prec✝
• Collins2005.instReprLevel.repr Collins2005.Level.anyStage prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Collins2005.Level.anyStage")).group prec✝

def Collins2005.Level.CCommands : Level → Minimalist.Derivation → Minimalist.SyntacticObject → Minimalist.SyntacticObject → Prop

C-command at a level of d, at its last stage or at some stage.

Equations

• Collins2005.Level.surface.CCommands x✝ = x✝.BindsAtSurface
• Collins2005.Level.anyStage.CCommands x✝ = x✝.BindsAtSomeStage

@[instance_reducible]

instance Collins2005.instDecidableRelSyntacticObjectCCommands (ℓ : Level) (d : Minimalist.Derivation) : DecidableRel (ℓ.CCommands d)

Equations

• Collins2005.instDecidableRelSyntacticObjectCCommands Collins2005.Level.surface x✝ = fun (x y : Minimalist.SyntacticObject) => Collins2005.instDecidableRelSyntacticObjectCCommands._aux_1 x✝ x y
• Collins2005.instDecidableRelSyntacticObjectCCommands Collins2005.Level.anyStage x✝ = fun (x y : Minimalist.SyntacticObject) => Collins2005.instDecidableRelSyntacticObjectCCommands._aux_3 x✝ x y

@[reducible, inline]

abbrev Collins2005.Level.configuration (ℓ : Level) (p : Clause) (d : Minimalist.Derivation) : Binding.Configuration Position

The binding configuration of p at level ℓ of its derivation d, in which one position commands another when its leaf c-commands the other's there.

Equations

• ℓ.configuration p d = Binding.Configuration.monoclausal p.at? fun (x y : Minimalist.LexicalItem.Token) => ℓ.CCommands d ↑x ↑y

inductive Collins2005.Dependency : Type

The dependencies the rows test are a negative polarity item, the other, a bound variable, a reflexive, a pronoun and a name.

• npi : Dependency
• other : Dependency
• variable : Dependency
• reflexive : Dependency
• pronoun : Dependency
• name : Dependency

@[instance_reducible]

instance Collins2005.instDecidableEqDependency : DecidableEq Dependency

Equations

• Collins2005.instDecidableEqDependency x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Collins2005.instReprDependency.repr : Dependency → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Collins2005.instReprDependency : Repr Dependency

Equations

• Collins2005.instReprDependency = { reprPrec := Collins2005.instReprDependency.repr }

def Collins2005.Dependency.predict (dep : Dependency) (p : Clause) (d : Minimalist.Derivation) (x y : Position) : Judgment

The judgment a dependency predicts for the element at y, dependent on the element at x, in the derivation d of p. A reflexive meets Condition A at the surface, or only at some stage, which the paper grades ??, (72); a bound variable is bound at the surface, or only at some stage, graded ?, (75); a pronoun meets Condition B at every stage, Principle B applying as the DP is Merged, (83)–(84) (§9.3); a name meets Condition C at the surface, without reconstruction (§9.2); a negative polarity item and the other need a c-commanding licensor at the surface.

Equations

• One or more equations did not get rendered due to their size.
• dep.predict p d x y = if (Collins2005.Level.surface.configuration p d).commands x y then Judgment.acceptable else Judgment.ungrammatical

structure Collins2005.Licensing : Type

A licensing row's configuration.

• clause : Clause

  The clause.

• evacuated : Bool

  Whether the PP evacuated PartP.

• dependency : Dependency

  The dependency.

• antecedent : Position

  The position that must, or must not, c-command.

• dependent : Position

  The position of the dependent element.

def Collins2005.Licensing.ofRow (row : Datum) : Option Licensing

The configuration a row records.

Equations

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

def Collins2005.Licensing.derivation (c : Licensing) : Minimalist.Derivation

The PartP-movement derivation of the configuration, with the PP evacuated or not.

Equations

• c.derivation = c.clause.passive Collins2005.Analysis.partP c.evacuated

def Collins2005.Licensing.predict (c : Licensing) : Judgment

The judgment the configuration predicts on its derivation.

Equations

• c.predict = c.dependency.predict c.clause c.derivation c.antecedent c.dependent

theorem Collins2005.licensing_rows (row : Datum) : row ∈ Examples.all → ∀ c ∈ Licensing.ofRow row, c.predict = row.judgment

The [BL86] tests (10), Principle A (72), (74), the bound variable (75), Principle B (80) and Principle C (85) all follow from where the PP sits: evacuated to Spec,XP it is c-commanded by the external argument at the surface, inside the fronted PartP only before PartP moved.

theorem Collins2005.principleB_anyStage (ℓ : Level) : (∀ row ∈ Examples.all, ∀ c ∈ Licensing.ofRow row, c.dependency = Dependency.pronoun → (row.judgment = Judgment.acceptable ↔ (ℓ.configuration c.clause c.derivation).Condition (Binding.pair c.antecedent c.dependent) ∅ c.dependent Binding.BindingClass.pronoun)) ↔ ℓ = Level.anyStage

Principle B holds at every stage, as the external argument is Merged. Evaluated at the surface it would admit (80a), whose pronoun the fronted PartP has carried out of the external argument's c-command.

Participle licensing (§3, (23)–(28))

inductive Collins2005.Auxiliary : Type

The auxiliary over the participle: have, be, or none, as in a participial modifier.

• have : Auxiliary
• be : Auxiliary
• bare : Auxiliary

@[instance_reducible]

instance Collins2005.instDecidableEqAuxiliary : DecidableEq Auxiliary

Equations

• Collins2005.instDecidableEqAuxiliary x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Collins2005.instReprAuxiliary.repr : Auxiliary → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Collins2005.instReprAuxiliary.repr Collins2005.Auxiliary.be prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Collins2005.Auxiliary.be")).group prec✝

@[instance_reducible]

instance Collins2005.instReprAuxiliary : Repr Auxiliary

Equations

• Collins2005.instReprAuxiliary = { reprPrec := Collins2005.instReprAuxiliary.repr }

structure Collins2005.Participle : Type

A participle clause: its auxiliary and whether a VoiceP is present.

• auxiliary : Auxiliary

  The auxiliary.

• voiceP : Bool

  Whether a Voice head is present.

def Collins2005.Participle.Licensed (c : Participle) : Prop

A participle must be licensed by exactly one of have, which c-selects it, and Voice, which attracts it, (24)–(25): (24) requires one, a participle Voice has licensed cannot also be checked by have, and be imposes nothing (§3).

Equations

• c.Licensed = Xor (c.auxiliary = Collins2005.Auxiliary.have) (c.voiceP = true)

@[instance_reducible]

instance Collins2005.instDecidableLicensed (c : Participle) : Decidable c.Licensed

Equations

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

def Collins2005.Participle.ofRow (row : Datum) : Option Participle

The configuration a row records.

Equations

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

theorem Collins2005.participle_rows (row : Datum) : row ∈ Examples.all → ∀ c ∈ Participle.ofRow row, row.judgment = Judgment.acceptable ↔ c.Licensed

The auxiliary paradigm (23) and the participial modifiers (27): a participle clause is acceptable exactly when its participle has one licenser.