Keine (2020): Probes and Their Horizons

This file formalizes the horizons theory of [Kei20] as it parameterizes probes across languages. A probe's search terminates at its horizon category ((33)); labels are bilateral within an extended projection, so a clause is opaque to a probe exactly when its label contains the horizon, and Upward Entailment holds for every probe, transparency being antitone in the extension order of clause sizes (sizes_le). Hindi's four clause sizes ((168)) follow from the probes of (219), with NmlzP and CP incomparable, the one transparent to wh-licensing and the other to Ā-movement (hindi_table, nmlzP_cP_incomparable), and the A-Movement–Agreement Generalization ((231)) from the two probes on T⁰ sharing a horizon. English ((241)) and German ((367)), with ForceP above CP, follow the same way (english_table, german_table), and the Itelmen ((269)) and Tsez ((271)) probes mismatch movement and agreement in both directions (mismatches). Vacuity ((274)–(278)) yields the Height–Locality Theorem ((279)), which the attested probes obey, and the default horizon ((307)) is the strictest nonvacuous one (hlt_location_to_horizon, default_horizon_strictest). Variation is a horizon parameter: the A-movement settings of (300) form an entailment chain (a_movement_chain), and the Ban on Improper Movement (Section 6.2) with the smuggling and remnant-movement restrictions (Section 3.4.3) is the opacity of a CP to the A-probes whose horizon it inherits (improper_movement).

Implementation notes

Labels are the bilateral labels of the substrate's ClauseSpines, with the Hindi NmlzP, the German ForceP and the Tsez TopP and ForceP defined here, and so are the probes of (219), (241), (300) and (367); the Itelmen and Tsez probes are parameterized by their head, which (269) and (271) leave open. Chapters 4 and 5, on CP and vP phases, are not formalized beyond the opacity facts the tables record.

References

• [Kei20]
• [BW05]
• [PP01]

def Keine2020.row (sizes : List Minimalist.ClauseSpine) (p : Minimalist.Probe.Profile) : List Bool

A probe's row of a transparency table over clause sizes.

Equations

• Keine2020.row sizes p = List.map (fun (s : Minimalist.ClauseSpine) => decide (p.TransparentTo s.label)) sizes

def Keine2020.nmlzP : Minimalist.ClauseSpine

The Hindi nominalized clause [V, v, T, Nmlz], a clause type distinct from CP (Chapter 2).

Equations

• Keine2020.nmlzP = { heads := [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.T, Minimalist.Cat.Nmlz] }

def Keine2020.forceP : Minimalist.ClauseSpine

The German verb-second clause [V, v, T, C, Force], projecting ForceP above CP (Chapter 4).

Equations

• Keine2020.forceP = { heads := [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.T, Minimalist.Cat.C, Minimalist.Cat.Force] }

Upward Entailment

theorem Keine2020.sizes_le : Minimalist.ClauseSpine.vP ≤ Minimalist.ClauseSpine.tP ∧ Minimalist.ClauseSpine.tP ≤ Minimalist.ClauseSpine.cP ∧ Minimalist.ClauseSpine.tP ≤ nmlzP ∧ Minimalist.ClauseSpine.cP ≤ forceP

The book's clause sizes stand in the extension order, TP extending vP, CP and NmlzP extending TP and ForceP extending CP. Transparency is antitone in this order for every probe (Probe.Profile.transparentTo_label_antitone), which is Upward Entailment.

structure Keine2020.LanguageProbeConfig : Type

A language's probe settings for the four operations of the transparency tables.

• phi : Minimalist.Probe.Profile

  The φ-agreement probe.

• aMove : Minimalist.Probe.Profile

  The A-movement probe.

• wh : Minimalist.Probe.Profile

  The wh-licensing probe.

• ābar : Minimalist.Probe.Profile

  The Ā-movement or topicalization probe.

@[instance_reducible]

instance Keine2020.instReprLanguageProbeConfig : Repr LanguageProbeConfig

Equations

• Keine2020.instReprLanguageProbeConfig = { reprPrec := Keine2020.instReprLanguageProbeConfig.repr }

def Keine2020.instReprLanguageProbeConfig.repr : LanguageProbeConfig → ℕ → Std.Format

Equations

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

def Keine2020.LanguageProbeConfig.hindi : LanguageProbeConfig

The Hindi probes of (219) put A-movement and φ-agreement on T⁰ with horizon T, wh-licensing on C⁰ with horizon C and Ā-movement on C⁰ with horizon Nmlz.

Equations

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

def Keine2020.LanguageProbeConfig.english : LanguageProbeConfig

The English probes of (241), the A-probe on T⁰ with horizon C and the wh-probe on C⁰ without horizon, Ā-movement being wh-movement. The book lists no separate φ-probe, taken here to share the A-probe's settings.

Equations

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

def Keine2020.englishExtr : Minimalist.Probe.Profile

The English extraposition probe of (241), on T⁰ with horizon T.

Equations

• Keine2020.englishExtr = { probeHead := Minimalist.Cat.T, horizon := some Minimalist.Cat.T }

def Keine2020.lubukusuAProbe : Minimalist.Probe.Profile

The Lubukusu A-probe of (300), without horizon, so that it hyperraises out of finite clauses.

Equations

• Keine2020.lubukusuAProbe = { probeHead := Minimalist.Cat.T, horizon := none }

def Keine2020.defaultHorizon (probeHead : Minimalist.Cat) : Minimalist.Probe.Profile

The default horizon of a probe on X⁰ is X itself ((307)).

Equations

• Keine2020.defaultHorizon probeHead = { probeHead := probeHead, horizon := some probeHead }

Hindi (Chapters 2 and 3)

def Keine2020.hindiSizes : List Minimalist.ClauseSpine

The four Hindi clause sizes of (168), the nominalized clause beside the finite one.

Equations

• Keine2020.hindiSizes = [Minimalist.ClauseSpine.vP, Minimalist.ClauseSpine.tP, Minimalist.ClauseSpine.cP, Keine2020.nmlzP]

theorem Keine2020.hindi_table : row hindiSizes LanguageProbeConfig.hindi.aMove = [true, false, false, false] ∧ row hindiSizes LanguageProbeConfig.hindi.phi = [true, false, false, false] ∧ row hindiSizes LanguageProbeConfig.hindi.wh = [true, true, false, true] ∧ row hindiSizes LanguageProbeConfig.hindi.ābar = [true, true, true, false]

(168) from (219): A-movement and φ-agreement, on T⁰ with horizon T, enter only vP clauses; wh-licensing, on C⁰ with horizon C, every clause but CP; Ā-movement, on C⁰ with horizon Nmlz, every clause but NmlzP.

theorem Keine2020.nmlzP_cP_incomparable : (¬nmlzP ≤ Minimalist.ClauseSpine.cP ∧ ¬Minimalist.ClauseSpine.cP ≤ nmlzP) ∧ (LanguageProbeConfig.hindi.wh.TransparentTo nmlzP.label ∧ ¬LanguageProbeConfig.hindi.wh.TransparentTo Minimalist.ClauseSpine.cP.label) ∧ (LanguageProbeConfig.hindi.ābar.TransparentTo Minimalist.ClauseSpine.cP.label ∧ ¬LanguageProbeConfig.hindi.ābar.TransparentTo nmlzP.label) ∧ (List.map (row hindiSizes) [LanguageProbeConfig.hindi.phi, LanguageProbeConfig.hindi.wh, LanguageProbeConfig.hindi.ābar]).Nodup

NmlzP and CP are incomparable in the extension order, and each is opaque to a probe on C⁰ that the other admits, so transparency does not order the clause sizes linearly and three locality profiles arise.

theorem Keine2020.a_movement_agreement_generalization : LanguageProbeConfig.hindi.aMove = LanguageProbeConfig.hindi.phi ∧ LanguageProbeConfig.hindi.ābar.TransparentTo Minimalist.ClauseSpine.cP.label ∧ ¬LanguageProbeConfig.hindi.phi.TransparentTo Minimalist.ClauseSpine.cP.label

The A- and φ-probes coincide, so a clause that A-extraction has entered is transparent to agreement, which is then obligatory, while the Ā-probe's horizon differs, and a finite clause shows it (231).

English and German (Section 3.4.2 and Chapter 4)

def Keine2020.englishSizes : List Minimalist.ClauseSpine

The English clause sizes.

Equations

• Keine2020.englishSizes = [Minimalist.ClauseSpine.vP, Minimalist.ClauseSpine.tP, Minimalist.ClauseSpine.cP]

theorem Keine2020.english_table : row englishSizes LanguageProbeConfig.english.aMove = [true, true, false] ∧ row englishSizes LanguageProbeConfig.english.wh = [true, true, true] ∧ row englishSizes englishExtr = [true, false, false]

(241): the A-probe, with horizon C, enters nonfinite clauses but not finite ones, the ban on hyperraising (242); the wh-probe has no horizon; extraposition, with horizon T, leaves no clause larger than vP.

def Keine2020.germanScr : Minimalist.Probe.Profile

The German probes of (367) put scrambling on T⁰ with horizon T, relativization on C⁰ with horizon C, wh-movement into a verb-final clause on C⁰ with horizon Force, and topicalization on Force⁰ without a horizon.

Equations

• Keine2020.germanScr = { probeHead := Minimalist.Cat.T, horizon := some Minimalist.Cat.T }

def Keine2020.germanRel : Minimalist.Probe.Profile

Equations

• Keine2020.germanRel = { probeHead := Minimalist.Cat.C, horizon := some Minimalist.Cat.C }

def Keine2020.germanWh : Minimalist.Probe.Profile

Equations

• Keine2020.germanWh = { probeHead := Minimalist.Cat.C, horizon := some Minimalist.Cat.Force }

def Keine2020.germanTop : Minimalist.Probe.Profile

Equations

• Keine2020.germanTop = { probeHead := Minimalist.Cat.Force, horizon := none }

def Keine2020.germanSizes : List Minimalist.ClauseSpine

The German clause sizes, whose verb-second clauses project ForceP above CP.

Equations

• Keine2020.germanSizes = [Minimalist.ClauseSpine.vP, Minimalist.ClauseSpine.tP, Minimalist.ClauseSpine.cP, Keine2020.forceP]

theorem Keine2020.german_table : row germanSizes germanScr = [true, false, false, false] ∧ row germanSizes germanRel = [true, true, false, false] ∧ row germanSizes germanWh = [true, true, true, false] ∧ row germanSizes germanTop = [true, true, true, true]

Chapter 4: the four German movements cut off at successive clause sizes.

Movement–agreement mismatches (Section 3.4.5)

def Keine2020.itelmenPhi (head : Minimalist.Cat) : Minimalist.Probe.Profile

The Itelmen probes of (269), φ-agreement with horizon T and movement without a horizon.

Equations

• Keine2020.itelmenPhi head = { probeHead := head, horizon := some Minimalist.Cat.T }

def Keine2020.itelmenMove (head : Minimalist.Cat) : Minimalist.Probe.Profile

Equations

• Keine2020.itelmenMove head = { probeHead := head, horizon := none }

def Keine2020.tsezPhi (head : Minimalist.Cat) : Minimalist.Probe.Profile

The Tsez probes of (271), φ-agreement with horizon Force and movement with horizon Top.

Equations

• Keine2020.tsezPhi head = { probeHead := head, horizon := some Minimalist.Cat.Force }

def Keine2020.tsezMove (head : Minimalist.Cat) : Minimalist.Probe.Profile

Equations

• Keine2020.tsezMove head = { probeHead := head, horizon := some Minimalist.Cat.Top }

def Keine2020.tsezTopP : Minimalist.ClauseSpine

The Tsez clause sizes above TP are TopP and ForceP, which requires TopP below it.

Equations

• Keine2020.tsezTopP = { heads := [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.T, Minimalist.Cat.Top] }

def Keine2020.tsezForceP : Minimalist.ClauseSpine

Equations

• Keine2020.tsezForceP = { heads := [Minimalist.Cat.V, Minimalist.Cat.v, Minimalist.Cat.T, Minimalist.Cat.Top, Minimalist.Cat.Force] }

theorem Keine2020.mismatches (head : Minimalist.Cat) : ((itelmenMove head).TransparentTo Minimalist.ClauseSpine.tP.label ∧ ¬(itelmenPhi head).TransparentTo Minimalist.ClauseSpine.tP.label) ∧ ((tsezPhi head).TransparentTo tsezTopP.label ∧ ¬(tsezMove head).TransparentTo tsezTopP.label) ∧ ¬(tsezPhi head).TransparentTo tsezForceP.label ∧ ¬(tsezMove head).TransparentTo tsezForceP.label

(269), (271): movement and agreement mismatch in both directions. An Itelmen TP clause is transparent to movement but opaque to agreement; a Tsez TopP clause is transparent to agreement but opaque to movement, and a ForceP clause, inheriting Top, to neither.

The Height–Locality Theorem (Section 3.5)

theorem Keine2020.vacuous_on_C (h : Minimalist.Cat) : h ∈ Minimalist.ClauseSpine.tP → { probeHead := Minimalist.Cat.C, horizon := some h }.IsVacuous

(274)–(278): a probe on C⁰ whose horizon is a category of its sister TP terminates there and is vacuous.

theorem Keine2020.hlt_location_to_horizon : (∀ (h : Minimalist.Cat), h ∈ Minimalist.ClauseSpine.vP → { probeHead := Minimalist.Cat.T, horizon := some h }.IsVacuous) ∧ (∀ (h : Minimalist.Cat), h ∈ Minimalist.ClauseSpine.tP → { probeHead := Minimalist.Cat.C, horizon := some h }.IsVacuous) ∧ ∀ (h : Minimalist.Cat), h ∈ Minimalist.ClauseSpine.cP → { probeHead := Minimalist.Cat.Force, horizon := some h }.IsVacuous

(279a), location to horizon: a probe on T⁰, C⁰ or Force⁰ with a horizon among the projections below it is vacuous.

theorem Keine2020.hlt_horizon_to_location : (∀ (head : Minimalist.Cat), head ∈ [Minimalist.Cat.C, Minimalist.Cat.Force] → { probeHead := head, horizon := some Minimalist.Cat.T }.IsVacuous) ∧ { probeHead := Minimalist.Cat.Force, horizon := some Minimalist.Cat.C }.IsVacuous

(279b), horizon to location: a probe with horizon T is vacuous above T⁰, and one with horizon C above C⁰.

theorem Keine2020.attested_nonvacuous (p : Minimalist.Probe.Profile) : p ∈ [LanguageProbeConfig.hindi.aMove, LanguageProbeConfig.hindi.phi, LanguageProbeConfig.hindi.wh, LanguageProbeConfig.hindi.ābar, LanguageProbeConfig.english.aMove, LanguageProbeConfig.english.wh, englishExtr, germanScr, germanRel, germanWh, germanTop] → ¬p.IsVacuous

The attested probes of (219), (241) and (367) are nonvacuous, as (279) requires.

theorem Keine2020.default_horizon_strictest : (∀ (X : Minimalist.Cat), X ∈ [Minimalist.Cat.T, Minimalist.Cat.C, Minimalist.Cat.Force] → ¬(defaultHorizon X).IsVacuous) ∧ LanguageProbeConfig.hindi.phi = defaultHorizon Minimalist.Cat.T ∧ englishExtr = defaultHorizon Minimalist.Cat.T ∧ germanScr = defaultHorizon Minimalist.Cat.T

(307): the default horizon of a probe on X⁰ is X, the strictest choice that is not vacuous; the Hindi probes on T⁰, English extraposition and German scrambling take it.

Variation and improper movement (Sections 3.6, 3.4.3, 6.2)

theorem Keine2020.a_movement_chain (L : Finset Minimalist.Cat) (hL : Minimalist.Cat.C ∈ L → Minimalist.Cat.T ∈ L) : (LanguageProbeConfig.hindi.aMove.TransparentTo L → LanguageProbeConfig.english.aMove.TransparentTo L) ∧ (LanguageProbeConfig.english.aMove.TransparentTo L → lubukusuAProbe.TransparentTo L)

(300): the A-movement settings, Lubukusu without a horizon, English with C and Hindi with T, form an entailment chain over the clauses of an extended projection, whose labels contain T whenever they contain C.

theorem Keine2020.improper_movement (h : Minimalist.Cat) (hh : h ∈ Minimalist.ClauseSpine.cP) : ¬{ probeHead := Minimalist.Cat.T, horizon := some h }.TransparentTo Minimalist.ClauseSpine.cP.label

Sections 3.4.3 and 6.2: the Ban on Improper Movement and the smuggling and remnant-movement restrictions are one fact about domains rather than items: a CP is opaque to every A-probe whose horizon it inherits, edge included, so nothing Ā-movement has placed in or under a CP is reachable by A-movement, while Ā-probes with no horizon or one outside the label are unaffected.

theorem Keine2020.improper_movement_attested : (∀ (p : Minimalist.Probe.Profile), p ∈ [LanguageProbeConfig.hindi.aMove, LanguageProbeConfig.english.aMove, germanScr] → ¬p.TransparentTo Minimalist.ClauseSpine.cP.label) ∧ ∀ (p : Minimalist.Probe.Profile), p ∈ [LanguageProbeConfig.hindi.ābar, LanguageProbeConfig.english.wh] → p.TransparentTo Minimalist.ClauseSpine.cP.label

The three A-probes of (300) with a horizon are blocked by CP, and the Hindi and English Ā-probes are not.