Gisborne (2026): Mutual dependency, English wh-clauses and Word Grammar

This file formalizes Gisborne's account of word order under mutual dependency in Word Grammar. Word order is fixed by landmarks, which must form a projective tree as in Robinson's axioms, and we compare Hudson's earlier and later theories of landmarks with Gisborne's revision, in which an extracted word is placed by a positional head outside the landmark tree.

Main definitions

• Analysis n: a Word Grammar analysis of n words, a network of typed dependencies in which a word may have several heads and two words may depend on each other.
• Analysis.IsLandmark A w p: p is the landmark of w by Hudson's 2007 rules, under which a head is a landmark unless it is subordinate to another head.
• Analysis.Orders A L root: the landmark relation L forms a projective tree from root, with every word on its side of its landmark.
• Analysis.OrderedByLandmarks A, Analysis.OrderedByChosenLandmarks A, Analysis.OrderedByPositionalHeads A: A is ordered by the 2007 theory, by landmarks chosen as in the 2018 theory, and by the revision.

Main statements

• Analysis.isLandmark_iff: the 2007 rules, stated as default inheritance, make p the landmark of w exactly when p is a head of w not subordinate to another of its heads.
• Analysis.not_orderedByLandmarks_of_extraction: an analysis is not ordered by the 2007 theory when a word is extracted from a head that it heads and has another head as well.
• Analysis.OrderedByLandmarks.orderedByPositionalHeads: the revision orders every analysis the 2007 theory orders.
• orderedByPositionalHeads_whatHeBoughtCostLots, not_orderedByLandmarks_whatHeBoughtCostLots: the revision orders the free relative What he bought cost lots, and the 2007 theory does not.

Implementation notes

• The landmark rules are a DefaultInheritance network over the concepts parent and subordinate parent, and a landmark relation is checked for IsTree and IsProjective as a DependencyGrammar.Graph with UD's dep on each arc.
• Each dependency type fixes the direction of its head with respect to its dependent (Rel.direction), and an extractee's direction overrides an object's.
• Chosen landmarks range over each word's heads; the Best Landmark Principle's preference for the nearest more prominent word is not modelled.

TODO

• The distributional evidence that free relatives are headed by their wh word and dependent interrogatives by their verb.

References

• N. Gisborne, Mutual Dependency, English wh-Clauses and Word Grammar (2026)
• R. Hudson, Language Networks: The New Word Grammar (2007)
• R. Hudson, Pied-Piping in Cognition (2018)
• J. J. Robinson, Dependency Structures and Transformational Rules (1970)

Word Grammar analyses

inductive Gisborne2026.Rel : Type

The dependencies of the diagrams are subject, object, complement, the complement of a raising verb labelled xc in (9), extractee, and adjuncts before and after their heads.

• subj : Rel
• obj : Rel
• comp : Rel
• xcomp : Rel
• extractee : Rel
• preAdjunct : Rel
• postAdjunct : Rel

@[instance_reducible]

instance Gisborne2026.instDecidableEqRel : DecidableEq Rel

Equations

• Gisborne2026.instDecidableEqRel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Gisborne2026.instFintypeRel : Fintype Rel

Equations

• Gisborne2026.instFintypeRel = { elems := { val := ↑Gisborne2026.Rel.enumList, nodup := Gisborne2026.Rel.enumList_nodup }, complete := Gisborne2026.instFintypeRel._proof_1 }

@[instance_reducible]

instance Gisborne2026.instReprRel : Repr Rel

Equations

• Gisborne2026.instReprRel = { reprPrec := Gisborne2026.instReprRel.repr }

def Gisborne2026.instReprRel.repr : Rel → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Gisborne2026.instReprRel.repr Gisborne2026.Rel.subj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gisborne2026.Rel.subj")).group prec✝
• Gisborne2026.instReprRel.repr Gisborne2026.Rel.obj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gisborne2026.Rel.obj")).group prec✝
• Gisborne2026.instReprRel.repr Gisborne2026.Rel.comp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gisborne2026.Rel.comp")).group prec✝
• Gisborne2026.instReprRel.repr Gisborne2026.Rel.xcomp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gisborne2026.Rel.xcomp")).group prec✝
• Gisborne2026.instReprRel.repr Gisborne2026.Rel.extractee prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gisborne2026.Rel.extractee")).group prec✝
• Gisborne2026.instReprRel.repr Gisborne2026.Rel.preAdjunct prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gisborne2026.Rel.preAdjunct")).group prec✝

def Gisborne2026.Rel.direction : Rel → HeadDirection

The direction of a head with respect to a dependent of each type, head-final for subjects, extractees and pre-adjuncts, which stand before it, and head-initial for the others.

Equations

• Gisborne2026.Rel.subj.direction = HeadDirection.headFinal
• Gisborne2026.Rel.extractee.direction = HeadDirection.headFinal
• Gisborne2026.Rel.preAdjunct.direction = HeadDirection.headFinal
• Gisborne2026.Rel.obj.direction = HeadDirection.headInitial
• Gisborne2026.Rel.comp.direction = HeadDirection.headInitial
• Gisborne2026.Rel.xcomp.direction = HeadDirection.headInitial
• Gisborne2026.Rel.postAdjunct.direction = HeadDirection.headInitial

structure Gisborne2026.Analysis (n : ℕ) : Type

A Word Grammar analysis has the words in their order, the typed dependencies, each from a head to a dependent, and the root. Several dependencies may link one pair, and two words may depend on each other.

• words : Fin n → Morphology.Word

  The words in their order.

• arcs : List (Fin n × Fin n × Rel)

  The dependencies, head first.

• root : Fin n

  The root.

def Gisborne2026.Analysis.Dep {n : ℕ} (A : Analysis n) (h w : Fin n) (r : Rel) : Prop

w depends on h by r.

Equations

• A.Dep h w r = ((h, w, r) ∈ A.arcs)

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableDep {n : ℕ} (A : Analysis n) (h w : Fin n) (r : Rel) : Decidable (A.Dep h w r)

Equations

• A.instDecidableDep h w r = { decide := decide (List.elem (h, w, r) A.arcs = true), reflects_decide := ⋯ }

def Gisborne2026.Analysis.Parent {n : ℕ} (A : Analysis n) (h w : Fin n) : Prop

h is a parent of w.

Equations

• A.Parent h w = ∃ (r : Gisborne2026.Rel), A.Dep h w r

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableRelFinParent {n : ℕ} (A : Analysis n) : DecidableRel A.Parent

Equations

• A.instDecidableRelFinParent x✝¹ x✝ = { decide := decide (∃ a ∈ Finset.univ, A.Dep x✝¹ x✝ a), reflects_decide := ⋯ }

def Gisborne2026.Analysis.Subordinate {n : ℕ} (A : Analysis n) (x y : Fin n) : Prop

x is subordinate to y: a chain of dependencies leads from y to x.

Equations

• A.Subordinate x y = Relation.TransGen A.Parent y x

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableRelFinSubordinate {n : ℕ} (A : Analysis n) : DecidableRel A.Subordinate

Equations

• A.instDecidableRelFinSubordinate x✝¹ x✝ = Gisborne2026.Analysis.instDecidableRelFinSubordinate._aux_1 A x✝¹ x✝

def Gisborne2026.Analysis.SubordinateParent {n : ℕ} (A : Analysis n) (w p : Fin n) : Prop

p is a subordinate parent of w: a parent of w subordinate to another of its parents.

Equations

• A.SubordinateParent w p = (A.Parent p w ∧ ∃ (q : Fin n), q ≠ p ∧ A.Parent q w ∧ A.Subordinate p q)

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableRelFinSubordinateParent {n : ℕ} (A : Analysis n) : DecidableRel A.SubordinateParent

Equations

• A.instDecidableRelFinSubordinateParent x✝¹ x✝ = { decide := decide (A.Parent x✝ x✝¹) && decide (∃ (q : Fin n), q ≠ x✝ ∧ A.Parent q x✝¹ ∧ A.Subordinate x✝ q), reflects_decide := ⋯ }

The landmark rules

inductive Gisborne2026.Analysis.Concept {n : ℕ} (A : Analysis n) : Type

The concepts of the landmark rules are parents, subordinate parents, and the pairs of a word and a position, the exemplars.

• parent {n : ℕ} {A : Analysis n} : A.Concept
• subordinateParent {n : ℕ} {A : Analysis n} : A.Concept
• pair {n : ℕ} {A : Analysis n} (w p : Fin n) : A.Concept

def Gisborne2026.Analysis.instDecidableEqConcept.decEq {n✝ : ℕ} {A✝ : Analysis n✝} (x✝ x✝¹ : A✝.Concept) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Gisborne2026.Analysis.instDecidableEqConcept.decEq Gisborne2026.Analysis.Concept.parent Gisborne2026.Analysis.Concept.parent = isTrue ⋯
• Gisborne2026.Analysis.instDecidableEqConcept.decEq Gisborne2026.Analysis.Concept.parent Gisborne2026.Analysis.Concept.subordinateParent = isFalse ⋯
• Gisborne2026.Analysis.instDecidableEqConcept.decEq Gisborne2026.Analysis.Concept.parent (Gisborne2026.Analysis.Concept.pair w p) = isFalse ⋯
• Gisborne2026.Analysis.instDecidableEqConcept.decEq Gisborne2026.Analysis.Concept.subordinateParent Gisborne2026.Analysis.Concept.parent = isFalse ⋯
• Gisborne2026.Analysis.instDecidableEqConcept.decEq Gisborne2026.Analysis.Concept.subordinateParent Gisborne2026.Analysis.Concept.subordinateParent = isTrue ⋯
• Gisborne2026.Analysis.instDecidableEqConcept.decEq Gisborne2026.Analysis.Concept.subordinateParent (Gisborne2026.Analysis.Concept.pair w p) = isFalse ⋯
• Gisborne2026.Analysis.instDecidableEqConcept.decEq (Gisborne2026.Analysis.Concept.pair w p) Gisborne2026.Analysis.Concept.parent = isFalse ⋯
• Gisborne2026.Analysis.instDecidableEqConcept.decEq (Gisborne2026.Analysis.Concept.pair w p) Gisborne2026.Analysis.Concept.subordinateParent = isFalse ⋯

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableEqConcept {n✝ : ℕ} {A✝ : Analysis n✝} : DecidableEq A✝.Concept

Equations

• Gisborne2026.Analysis.instDecidableEqConcept = Gisborne2026.Analysis.instDecidableEqConcept.decEq

@[instance_reducible]

instance Gisborne2026.Analysis.instFintypeConcept {n✝ : ℕ} {A✝ : Analysis n✝} : Fintype A✝.Concept

Equations

• Gisborne2026.Analysis.instFintypeConcept = Fintype.ofEquiv (Unit ⊕ Unit ⊕ (_ : Fin n✝) × Fin n✝) (Gisborne2026.Analysis.Concept.proxyTypeEquiv A✝)

def Gisborne2026.Analysis.conceptParents {n : ℕ} (A : Analysis n) : A.Concept → List A.Concept

The concepts each concept immediately isA. A subordinate parent is a parent, and a pair of a word and one of its parents is a subordinate parent or else a parent.

Equations

• One or more equations did not get rendered due to their size.
• A.conceptParents Gisborne2026.Analysis.Concept.parent = []
• A.conceptParents Gisborne2026.Analysis.Concept.subordinateParent = [Gisborne2026.Analysis.Concept.parent]

def Gisborne2026.Analysis.Concept.rank {n : ℕ} (A : Analysis n) : A.Concept → ℕ

The depth of a concept below parent.

Equations

• Gisborne2026.Analysis.Concept.rank A Gisborne2026.Analysis.Concept.parent = 0
• Gisborne2026.Analysis.Concept.rank A Gisborne2026.Analysis.Concept.subordinateParent = 1
• Gisborne2026.Analysis.Concept.rank A (Gisborne2026.Analysis.Concept.pair a a_1) = 2

@[instance_reducible]

instance Gisborne2026.Analysis.instPartialOrderConcept {n : ℕ} (A : Analysis n) : PartialOrder A.Concept

Equations

• A.instPartialOrderConcept = partialOrderOfCovers (fun (a b : A.Concept) => b ∈ A.conceptParents a) (Gisborne2026.Analysis.Concept.rank A) ⋯

def Gisborne2026.Analysis.landmarkRule {n : ℕ} (A : Analysis n) : A.Concept → Option Bool

The landmark rules, by which parents are landmarks and subordinate parents are not.

Equations

• A.landmarkRule Gisborne2026.Analysis.Concept.parent = some true
• A.landmarkRule Gisborne2026.Analysis.Concept.subordinateParent = some false
• A.landmarkRule (Gisborne2026.Analysis.Concept.pair a a_1) = none

def Gisborne2026.Analysis.IsLandmark {n : ℕ} (A : Analysis n) (w p : Fin n) : Prop

p is the landmark of w: the pair of w and p inherits landmark by the rules.

Equations

• A.IsLandmark w p = (true ∈ DefaultInheritance.inherited A.landmarkRule (Gisborne2026.Analysis.Concept.pair w p))

theorem Gisborne2026.Analysis.subordinateParent_le_parent {n : ℕ} {A : Analysis n} : Concept.subordinateParent ≤ Concept.parent

theorem Gisborne2026.Analysis.pair_le_iff {n : ℕ} {A : Analysis n} {p w : Fin n} {c : A.Concept} : Concept.pair w p ≤ c ↔ c = Concept.pair w p ∨ c = Concept.subordinateParent ∧ A.SubordinateParent w p ∨ c = Concept.parent ∧ A.Parent p w

A pair of a word and a position lies below subordinate parent when the position is a subordinate parent of the word, and below parent when it is a parent.

theorem Gisborne2026.Analysis.mem_specifiers_pair {n : ℕ} {A : Analysis n} {p w : Fin n} {c : A.Concept} : c ∈ DefaultInheritance.specifiers A.landmarkRule (Concept.pair w p) ↔ c = Concept.subordinateParent ∧ A.SubordinateParent w p ∨ c = Concept.parent ∧ A.Parent p w

theorem Gisborne2026.Analysis.isLandmark_iff {n : ℕ} {A : Analysis n} {p w : Fin n} : A.IsLandmark w p ↔ A.Parent p w ∧ ¬A.SubordinateParent w p

The landmark rules make p the landmark of w exactly when p is a parent of w and not a subordinate parent.

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableIsLandmark {n : ℕ} {A : Analysis n} {p w : Fin n} : Decidable (A.IsLandmark w p)

Equations

• Gisborne2026.Analysis.instDecidableIsLandmark = decidable_of_iff (A.Parent p w ∧ ¬A.SubordinateParent w p) ⋯

Landmark trees and word order

def Gisborne2026.Analysis.graphOf {n : ℕ} (A : Analysis n) (L : Fin n → Fin n → Prop) [DecidableRel L] (root : Fin n) : DependencyGrammar.Graph n

The graph of a landmark relation, L w p saying that p is the landmark of w, rooted at root, with an arc from each word's landmark to the word, labelled with UD's unspecified relation.

Equations

• A.graphOf L root = { words := A.words, label := fun (p w : Fin n) => if L w p then some UD.DepRel.dep else none, root := root }

def Gisborne2026.Analysis.RespectsLandmarks {n : ℕ} (A : Analysis n) (L : Fin n → Fin n → Prop) : Prop

Every word stands on the side of its landmark that its dependency on the landmark fixes, the extractee's side when it is extracted from the landmark, which overrides the side of its other dependency there.

Equations

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

def Gisborne2026.Analysis.Orders {n : ℕ} (A : Analysis n) (L : Fin n → Fin n → Prop) [DecidableRel L] (root : Fin n) : Prop

The landmarks order the analysis when they form a projective tree from the root and every word stands on its side of its landmark.

Equations

• A.Orders L root = ((A.graphOf L root).IsTree ∧ (A.graphOf L root).IsProjective ∧ A.RespectsLandmarks L)

def Gisborne2026.Analysis.ExtractionBy {n : ℕ} (A : Analysis n) (L : Fin n → Fin n → Prop) : Prop

Extraction by landmark, where the head a word is extracted from is its landmark.

Equations

• A.ExtractionBy L = ∀ (h w : Fin n), A.Dep h w Gisborne2026.Rel.extractee → L w h

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableRespectsLandmarks {n : ℕ} (A : Analysis n) (L : Fin n → Fin n → Prop) [DecidableRel L] : Decidable (A.RespectsLandmarks L)

Equations

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

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableOrders {n : ℕ} (A : Analysis n) (L : Fin n → Fin n → Prop) [DecidableRel L] (root : Fin n) : Decidable (A.Orders L root)

Equations

• A.instDecidableOrders L root = { decide := decide (A.graphOf L root).IsTree && decide ((A.graphOf L root).IsProjective ∧ A.RespectsLandmarks L), reflects_decide := ⋯ }

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableExtractionBy {n : ℕ} (A : Analysis n) (L : Fin n → Fin n → Prop) [DecidableRel L] : Decidable (A.ExtractionBy L)

Equations

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

@[reducible, inline]

abbrev Gisborne2026.Analysis.parentGraph {n : ℕ} (A : Analysis n) : DependencyGrammar.Graph n

The graph in which every parent is a landmark, as in the diagrams (52) to (55).

Equations

• A.parentGraph = A.graphOf (fun (w p : Fin n) => A.Parent p w) A.root

def Gisborne2026.Analysis.PositionalHead {n : ℕ} (A : Analysis n) (w h : Fin n) : Prop

The positional head of an extracted word, by the revision's start-rule of extraction, is the head it is extracted from.

Equations

• A.PositionalHead w h = A.Dep h w Gisborne2026.Rel.extractee

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidablePositionalHead {n : ℕ} (A : Analysis n) (w h : Fin n) : Decidable (A.PositionalHead w h)

Equations

• A.instDecidablePositionalHead w h = { decide := decide (List.elem (h, w, Gisborne2026.Rel.extractee) A.arcs = true), reflects_decide := ⋯ }

def Gisborne2026.Analysis.RespectsPositionalHeads {n : ℕ} (A : Analysis n) : Prop

Every extracted word stands on the extractee's side of its positional head, before it.

Equations

• A.RespectsPositionalHeads = ∀ (w h : Fin n), A.PositionalHead w h → Gisborne2026.Rel.extractee.direction.Orders h w

def Gisborne2026.Analysis.OrderedByLandmarks {n : ℕ} (A : Analysis n) : Prop

Word order by the 2007 theory. The landmarks the rules pick out order the analysis, and an extracted word's landmark is the head it is extracted from.

Equations

• A.OrderedByLandmarks = (A.Orders A.IsLandmark A.root ∧ A.ExtractionBy A.IsLandmark)

def Gisborne2026.Analysis.OrderedByPositionalHeads {n : ℕ} (A : Analysis n) : Prop

Word order by the revised theory. The landmarks the rules pick out order the analysis, and every extracted word precedes its positional head.

Equations

• A.OrderedByPositionalHeads = (A.Orders A.IsLandmark A.root ∧ A.RespectsPositionalHeads)

@[reducible, inline]

abbrev Gisborne2026.Analysis.Choice {n : ℕ} (A : Analysis n) : Type

A choice of landmarks in the later theory of [Hud18], where the Best Landmark Principle assigns them in place of the rules, giving each word one of its parents or none.

Equations

• A.Choice = ((w : Fin n) → Option { p : Fin n // A.Parent p w })

def Gisborne2026.Analysis.Choice.Landmark {n : ℕ} {A : Analysis n} (c : A.Choice) (w p : Fin n) : Prop

The landmark relation of a choice.

Equations

• c.Landmark w p = (Option.map Subtype.val (c w) = some p)

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableRelFinLandmark {n : ℕ} (A : Analysis n) (c : A.Choice) : DecidableRel c.Landmark

Equations

• A.instDecidableRelFinLandmark c x✝¹ x✝ = Gisborne2026.Analysis.instDecidableRelFinLandmark._aux_1 A c x✝¹ x✝

def Gisborne2026.Analysis.OrderedByChosenLandmarks {n : ℕ} (A : Analysis n) : Prop

Word order by the later theory. Some root and some choice of landmarks order the analysis, and every extracted word's landmark is the head it is extracted from.

Equations

• A.OrderedByChosenLandmarks = ∃ (root : Fin n) (c : A.Choice), A.Orders c.Landmark root ∧ A.ExtractionBy c.Landmark

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableRespectsPositionalHeads {n : ℕ} (A : Analysis n) : Decidable A.RespectsPositionalHeads

Equations

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

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableOrderedByLandmarks {n : ℕ} (A : Analysis n) : Decidable A.OrderedByLandmarks

Equations

• A.instDecidableOrderedByLandmarks = { decide := decide (A.Orders A.IsLandmark A.root) && decide (A.ExtractionBy A.IsLandmark), reflects_decide := ⋯ }

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableOrderedByPositionalHeads {n : ℕ} (A : Analysis n) : Decidable A.OrderedByPositionalHeads

Equations

• A.instDecidableOrderedByPositionalHeads = { decide := decide (A.Orders A.IsLandmark A.root) && decide A.RespectsPositionalHeads, reflects_decide := ⋯ }

@[instance_reducible]

instance Gisborne2026.Analysis.instDecidableOrderedByChosenLandmarks {n : ℕ} (A : Analysis n) : Decidable A.OrderedByChosenLandmarks

Equations

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

@[simp]

theorem Gisborne2026.Analysis.graphOf_adj {n : ℕ} {A : Analysis n} {p w : Fin n} {L : Fin n → Fin n → Prop} [DecidableRel L] {root : Fin n} : (A.graphOf L root).Adj p w ↔ L w p

theorem Gisborne2026.Analysis.not_isTree_graphOf {n : ℕ} {A : Analysis n} {p w : Fin n} {L : Fin n → Fin n → Prop} [DecidableRel L] {root : Fin n} (h₁ : L w p) (h₂ : L p w) : ¬(A.graphOf L root).IsTree

Two words cannot each be the other's landmark, since by transitivity each would be its own.

theorem Gisborne2026.Analysis.not_isTree_parentGraph {n : ℕ} {A : Analysis n} {p w : Fin n} (h₁ : A.Parent p w) (h₂ : A.Parent w p) : ¬A.parentGraph.IsTree

Two words that depend on each other cannot each be the other's landmark.

theorem Gisborne2026.Analysis.not_extractionBy_isLandmark {n : ℕ} {A : Analysis n} {h w : Fin n} (hex : A.Dep h w Rel.extractee) (hs : A.SubordinateParent w h) : ¬A.ExtractionBy A.IsLandmark

A word extracted from a head that is a subordinate parent of it is not positioned by a landmark, since the Subordinate Head Rule denies the head the landmark.

theorem Gisborne2026.Analysis.not_orderedByLandmarks_of_extraction {n : ℕ} {A : Analysis n} {h q w : Fin n} (hex : A.Dep h w Rel.extractee) (hq : A.Parent q w) (hqh : q ≠ h) (hwh : A.Parent w h) : ¬A.OrderedByLandmarks

A word that heads the clause it is extracted from and depends on a head outside it cannot be positioned by landmarks, since the head it is extracted from is subordinate to the outside head.

theorem Gisborne2026.Analysis.OrderedByLandmarks.orderedByPositionalHeads {n : ℕ} {A : Analysis n} (hO : A.OrderedByLandmarks) : A.OrderedByPositionalHeads

The revision accepts every analysis the 2007 theory accepts, since an extracted word precedes the head it is extracted from when that head is its landmark.

Raising, (9)

@[reducible, inline]

abbrev Gisborne2026.they : Morphology.Word

Equations

• Gisborne2026.they = English.Pronouns.they.toWord

@[reducible, inline]

abbrev Gisborne2026.seemed : Morphology.Word

Equations

• Gisborne2026.seemed = English.Verbs.seem.toWord English.Verbs.Verb.Cell.past

@[reducible, inline]

abbrev Gisborne2026.to_ : Morphology.Word

Equations

• Gisborne2026.to_ = English.Auxiliaries.toInf

@[reducible, inline]

abbrev Gisborne2026.dance : Morphology.Word

Equations

• Gisborne2026.dance = English.Verbs.dance.toWord English.Verbs.Verb.Cell.base

def Gisborne2026.theySeemedToDance : Analysis 4

In They seemed to dance, (9), the subject depends on each verb, and each verb's xc complement is the next.

Equations

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

theorem Gisborne2026.not_isTree_parentGraph_theySeemedToDance : ¬theySeemedToDance.parentGraph.IsTree ∧ ¬theySeemedToDance.parentGraph.IsProjective

The network of (9) is neither a tree nor projective, since the subject has three parents and the arcs from to and dance cross the root.

theorem Gisborne2026.isLandmark_theySeemedToDance : theySeemedToDance.IsLandmark 0 1 ∧ ¬theySeemedToDance.IsLandmark 0 2 ∧ ¬theySeemedToDance.IsLandmark 0 3

The subject's landmark is seemed, its one parent that is not subordinate to another.

theorem Gisborne2026.orderedByLandmarks_theySeemedToDance : theySeemedToDance.OrderedByLandmarks

The landmarks of (9) form a projective tree.

Dependent interrogatives, (51) and (52)

@[reducible, inline]

abbrev Gisborne2026.know : Morphology.Word

Equations

• Gisborne2026.know = English.Verbs.know.toWord English.Verbs.Verb.Cell.base

@[reducible, inline]

abbrev Gisborne2026.what : Morphology.Word

Equations

• Gisborne2026.what = English.Pronouns.what.toWord

@[reducible, inline]

abbrev Gisborne2026.she : Morphology.Word

Equations

• Gisborne2026.she = English.Pronouns.she.toWord

@[reducible, inline]

abbrev Gisborne2026.said : Morphology.Word

Equations

• Gisborne2026.said = English.Verbs.say.toWord English.Verbs.Verb.Cell.past

def Gisborne2026.verbHeaded : Analysis 4

In (51), (I don't) know what she said with the verb as head, said is the complement of know, and what its extracted object.

Equations

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

theorem Gisborne2026.orderedByLandmarks_verbHeaded : verbHeaded.OrderedByLandmarks

The verb-headed analysis has no mutual dependency and satisfies the 2007 theory.

def Gisborne2026.whHeaded : Analysis 4

In (52), the traditional analysis with the wh word as head, what is the complement of know and takes said as its complement, and it is also said's extracted object.

Equations

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

theorem Gisborne2026.not_orderedByLandmarks_whHeaded : ¬whHeaded.parentGraph.IsTree ∧ ¬whHeaded.OrderedByLandmarks

The wh-headed analysis fails the 2007 theory whichever way it goes. Were every parent a landmark, what and said would be each other's, and by the Subordinate Head Rule said is not the landmark of the word extracted from it.

theorem Gisborne2026.orderedByPositionalHeads_whHeaded : whHeaded.OrderedByPositionalHeads

The revised theory orders the wh-headed analysis too, so the case against it is not word order. The paper sets it aside on the distributional evidence of Section 4, and keeps the dissociation of landmark and positional head for exceptional constructions such as the free relative.

Free relatives, (53), (55) to (58)

@[reducible, inline]

abbrev Gisborne2026.i : Morphology.Word

Equations

• Gisborne2026.i = English.Pronouns.i.toWord

@[reducible, inline]

abbrev Gisborne2026.ate : Morphology.Word

Equations

• Gisborne2026.ate = English.Verbs.eat.toWord English.Verbs.Verb.Cell.past

def Gisborne2026.iAteWhatTheyAte : Analysis 5

In (53), I ate what they ate, what is the object of the first ate, takes the second as its complement, and is the second's extracted object.

Equations

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

theorem Gisborne2026.not_orderedByLandmarks_iAteWhatTheyAte : ¬iAteWhatTheyAte.parentGraph.IsTree ∧ ¬iAteWhatTheyAte.OrderedByLandmarks

The free relative (53) fails the 2007 theory whichever way it goes, as (55) does.

theorem Gisborne2026.orderedByPositionalHeads_iAteWhatTheyAte : iAteWhatTheyAte.OrderedByPositionalHeads

The revised theory orders the free relative (53).

@[reducible, inline]

abbrev Gisborne2026.he : Morphology.Word

Equations

• Gisborne2026.he = English.Pronouns.he.toWord

@[reducible, inline]

abbrev Gisborne2026.bought : Morphology.Word

Equations

• Gisborne2026.bought = English.Verbs.buy.toWord English.Verbs.Verb.Cell.past

@[reducible, inline]

abbrev Gisborne2026.cost : Morphology.Word

Equations

• Gisborne2026.cost = English.Verbs.cost.toWord English.Verbs.Verb.Cell.past

@[reducible, inline]

abbrev Gisborne2026.lots : Morphology.Word

Equations

• Gisborne2026.lots = (English.Nouns.lot.toWord Number.plural).get Gisborne2026.lots._proof_1

def Gisborne2026.whatHeBoughtCostLots : Analysis 5

In (55) and (56), What he bought cost lots, What is the subject of cost, takes bought as its complement, and is bought's extracted object.

Equations

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

theorem Gisborne2026.not_orderedByLandmarks_whatHeBoughtCostLots : ¬whatHeBoughtCostLots.parentGraph.IsTree ∧ ¬whatHeBoughtCostLots.OrderedByLandmarks

In (55), were every parent a landmark, What and bought would be each other's (lm-1, lm-2) and What would have two; by the Subordinate Head Rule, bought is not the landmark of the word extracted from it.

theorem Gisborne2026.landmarks_whatHeBoughtCostLots : whatHeBoughtCostLots.IsLandmark 2 0 ∧ whatHeBoughtCostLots.PositionalHead 0 2 ∧ whatHeBoughtCostLots.IsLandmark 0 3 ∧ ¬whatHeBoughtCostLots.IsLandmark 0 2

In (57a) to (57f) What is the landmark of bought, its complement, and bought is the positional head of What, its extractee; What's landmark is cost.

theorem Gisborne2026.orderedByPositionalHeads_whatHeBoughtCostLots : whatHeBoughtCostLots.OrderedByPositionalHeads

In (56) the landmarks form a projective tree, every word stands on its side of its landmark, and What precedes its positional head, the order in which bought follows What as its complement.

@[reducible, inline]

abbrev Gisborne2026.we : Morphology.Word

Equations

• Gisborne2026.we = English.Pronouns.we.toWord

@[reducible, inline]

abbrev Gisborne2026.saw : Morphology.Word

Equations

• Gisborne2026.saw = English.Verbs.see.toWord English.Verbs.Verb.Cell.past

@[reducible, inline]

abbrev Gisborne2026.happened : Morphology.Word

Equations

• Gisborne2026.happened = English.Verbs.happen.toWord English.Verbs.Verb.Cell.past

def Gisborne2026.weSawWhatHappened : Analysis 4

In (58), We saw what happened, a subject free relative without extraction, what is the complement of saw, takes happened as its complement, and is its subject.

Equations

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

theorem Gisborne2026.not_isTree_parentGraph_weSawWhatHappened : ¬weSawWhatHappened.parentGraph.IsTree

The mutual dependency of (58) would make what and happened each other's landmark, as in (54).

theorem Gisborne2026.orderedByLandmarks_weSawWhatHappened : weSawWhatHappened.OrderedByLandmarks

The Subordinate Head Rule leaves what with its one landmark saw, and the 2007 theory orders the subject free relative (58).

The later theory of landmarks, (11) to (14)

In the later theory [Hud18] landmarks are chosen online by the Best Landmark Principle rather than inherited, and in a mutual dependency either word may be the landmark of the other. Hudson's analyses of (11b) to (11e), which the paper diagrams in (12) and (13), are ordered or not by some choice of landmarks.

@[reducible, inline]

abbrev Gisborne2026.then_ : Morphology.Word

Equations

• Gisborne2026.then_ = Morphology.Word.mk' English.TemporalDeictic.then_.form UD.UPOS.ADV

@[reducible, inline]

abbrev Gisborne2026.wonder : Morphology.Word

Equations

• Gisborne2026.wonder = English.Verbs.wonder.toWord English.Verbs.Verb.Cell.base

def Gisborne2026.whatHappenedThen : Analysis 3

In (11b), What happened then?, what is the subject of happened and takes it as its complement, and then follows happened as its adjunct.

Equations

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

theorem Gisborne2026.landmarks_whatHappenedThen : (∃ (root : Fin 3) (c : whatHappenedThen.Choice), whatHappenedThen.Orders c.Landmark root ∧ c.Landmark 0 1) ∧ ∃ (root : Fin 3) (c : whatHappenedThen.Choice), whatHappenedThen.Orders c.Landmark root ∧ c.Landmark 1 0

Either word of the mutual dependency may be the landmark of the other.

def Gisborne2026.thenWhatHappened : Analysis 3

In (11c), Then what happened?, then precedes happened as its adjunct.

Equations

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

theorem Gisborne2026.landmarks_thenWhatHappened : thenWhatHappened.OrderedByChosenLandmarks ∧ ∀ (root : Fin 3) (c : thenWhatHappened.Choice), thenWhatHappened.Orders c.Landmark root → c.Landmark 1 2

The fronted then depends only on happened, and happened must be the landmark of what.

def Gisborne2026.iWonderWhatHappenedThen : Analysis 5

In (11d), I wonder what happened then, what is the complement of wonder.

Equations

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

theorem Gisborne2026.landmarks_iWonderWhatHappenedThen : iWonderWhatHappenedThen.OrderedByChosenLandmarks ∧ ∀ (root : Fin 5) (c : iWonderWhatHappenedThen.Choice), iWonderWhatHappenedThen.Orders c.Landmark root → c.Landmark 3 2

What has its landmark wonder, so it must be the landmark of happened.

def Gisborne2026.iWonderThenWhatHappened : Analysis 5

(11e), I wonder then what happened, has the dependencies of (11c) under wonder.

Equations

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

theorem Gisborne2026.not_orderedByChosenLandmarks_iWonderThenWhatHappened : ¬iWonderThenWhatHappened.OrderedByChosenLandmarks

No choice of landmarks orders (11e). The parent wonder excludes happened as the landmark of what, and the landmark link from then to happened crosses the one from what to wonder, (13).

def Gisborne2026.iWonderWhatTheySaw : Analysis 5

In (14), I wonder what they saw with the wh word as head, what is the complement of wonder, takes saw as its complement, and is its extracted object.

Equations

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

theorem Gisborne2026.not_orderedByChosenLandmarks_iWonderWhatTheySaw : ¬iWonderWhatTheySaw.OrderedByChosenLandmarks ∧ iWonderWhatTheySaw.OrderedByPositionalHeads

The later theory cannot order the extraction in (14), since what has one landmark, wonder, and were it saw, the head it is extracted from, saw would have what as its own. The revision orders it.