English Filler-Gap Constructions

[Sag10]

Parametric variation across the five types of English filler-gap (F-G) clause, following [Sag10]. The clauses share a common filler-head structure but differ systematically along the seven parameters of variation listed in the paper, and they cross-classify with clause-type supertypes from which their semantics is inherited.

The five F-G clause types

1. Wh-interrogative: "How foolish is he?" / "I wonder how foolish he is."
2. Wh-exclamative: "What a fool he is!" / "It's amazing how odd it is."
3. Topicalized: "The bagels, I like."
4. Wh-relative: "the person who they nominated"
5. The-clause: "The more people I met, the happier I became."

What is modeled

This file formalizes the descriptive parameter table of [Sag10] §2.1 plus the inheritance skeleton of the Sign-Based Construction Grammar analysis:

• a FGConstruction constraint bundle for each clause type, one field per parameter of variation;
• a cross-classifying clauseType supertype that determines the semantic type — so semantics is inherited, not stipulated per construction;
• the filler-head-cxt filler constraint ([CAT nonverbal]) stated once and proved inherited by all five constructions, rather than re-stipulated.

The full SBCG feature-structure unification engine (signs, MTR/DTRS feature geometry, multiple-inheritance lattice) is out of scope for a study file; it would live in the HPSG theory layer.

Bridges (true by construction, not by prose)

• islands reground on the canonical RSRL signature (Syntax/HPSG/Construction): islandhood is a Models fact — a topicalized/exclamative construct rejects a second, undischarged gap ([GAP ⟨⟩] plus amalgamation), not a boolean stipulation;
• agreement with [SWB03]'s SLASH model on the topicalization island;
• divergence from [Ros67]'s configurational Complex-NP Constraint on wh-relatives, which [Sag10] re-attributes to processing ([HS10]);
• the surface-form correspondents map to Features.ClauseForm.

Syntactic categories

inductive Sag2010.SynCat : Type

Syntactic categories relevant to F-G filler and head daughters. Nonverbal categories (NP, PP, AP, AdvP) appear as fillers; verbal projections (S, CP, VP) appear in the head daughter.

• NP : SynCat
• PP : SynCat
• AP : SynCat
• AdvP : SynCat
• S : SynCat
• CP : SynCat
• VP : SynCat

@[implicit_reducible]

instance Sag2010.instDecidableEqSynCat : DecidableEq SynCat

Equations

• Sag2010.instDecidableEqSynCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Sag2010.instReprSynCat.repr : SynCat → ℕ → Std.Format

Equations

• Sag2010.instReprSynCat.repr Sag2010.SynCat.NP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.SynCat.NP")).group prec✝
• Sag2010.instReprSynCat.repr Sag2010.SynCat.PP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.SynCat.PP")).group prec✝
• Sag2010.instReprSynCat.repr Sag2010.SynCat.AP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.SynCat.AP")).group prec✝
• Sag2010.instReprSynCat.repr Sag2010.SynCat.AdvP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.SynCat.AdvP")).group prec✝
• Sag2010.instReprSynCat.repr Sag2010.SynCat.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.SynCat.S")).group prec✝
• Sag2010.instReprSynCat.repr Sag2010.SynCat.CP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.SynCat.CP")).group prec✝
• Sag2010.instReprSynCat.repr Sag2010.SynCat.VP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.SynCat.VP")).group prec✝

@[implicit_reducible]

instance Sag2010.instReprSynCat : Repr SynCat

Equations

• Sag2010.instReprSynCat = { reprPrec := Sag2010.instReprSynCat.repr }

def Sag2010.SynCat.IsNonverbal (c : SynCat) : Prop

A category is nonverbal when it is not a verbal projection. [Sag10]'s filler-head construction constrains every filler daughter to be [CAT nonverbal] ((25)).

Equations

• c.IsNonverbal = (c = Sag2010.SynCat.NP ∨ c = Sag2010.SynCat.PP ∨ c = Sag2010.SynCat.AP ∨ c = Sag2010.SynCat.AdvP)

@[implicit_reducible]

instance Sag2010.instDecidablePredSynCatIsNonverbal : DecidablePred SynCat.IsNonverbal

Equations

• Sag2010.instDecidablePredSynCatIsNonverbal x✝ = Sag2010.instDecidablePredSynCatIsNonverbal._aux_1 x✝

Parameters of variation ((6))

inductive Sag2010.FillerWh : Type

The distinguished wh-element a construction requires in its filler daughter ((6a), (7)).

• noWh : FillerWh
• interrogative : FillerWh
• exclamative : FillerWh
• relative : FillerWh
• degreeThe : FillerWh

@[implicit_reducible]

instance Sag2010.instDecidableEqFillerWh : DecidableEq FillerWh

Equations

• Sag2010.instDecidableEqFillerWh x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Sag2010.instReprFillerWh : Repr FillerWh

Equations

• Sag2010.instReprFillerWh = { reprPrec := Sag2010.instReprFillerWh.repr }

def Sag2010.instReprFillerWh.repr : FillerWh → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Sag2010.instReprFillerWh.repr Sag2010.FillerWh.noWh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.FillerWh.noWh")).group prec✝
• Sag2010.instReprFillerWh.repr Sag2010.FillerWh.relative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.FillerWh.relative")).group prec✝
• Sag2010.instReprFillerWh.repr Sag2010.FillerWh.degreeThe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.FillerWh.degreeThe")).group prec✝

inductive Sag2010.InversionPolicy : Type

Inversion policy on the head daughter ((28)). Wh-interrogatives invert iff the clause is independent — the IC/INV identity constraint of construction (80), not an unconditional requirement.

• iffIndependent : InversionPolicy
• prohibited : InversionPolicy
• optional : InversionPolicy

@[implicit_reducible]

instance Sag2010.instDecidableEqInversionPolicy : DecidableEq InversionPolicy

Equations

• Sag2010.instDecidableEqInversionPolicy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Sag2010.instReprInversionPolicy : Repr InversionPolicy

Equations

• Sag2010.instReprInversionPolicy = { reprPrec := Sag2010.instReprInversionPolicy.repr }

def Sag2010.instReprInversionPolicy.repr : InversionPolicy → ℕ → Std.Format

Equations

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

inductive Sag2010.Finiteness : Type

Whether the head daughter may be infinitival ((29)).

• finiteOnly : Finiteness
• infinitivalPossible : Finiteness

@[implicit_reducible]

instance Sag2010.instDecidableEqFiniteness : DecidableEq Finiteness

Equations

• Sag2010.instDecidableEqFiniteness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Sag2010.instReprFiniteness.repr : Finiteness → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Sag2010.instReprFiniteness : Repr Finiteness

Equations

• Sag2010.instReprFiniteness = { reprPrec := Sag2010.instReprFiniteness.repr }

inductive Sag2010.HeadCat : Type

Syntactic category of the head daughter ((6c), (27)).

• s : HeadCat
• sOrCP : HeadCat

@[implicit_reducible]

instance Sag2010.instDecidableEqHeadCat : DecidableEq HeadCat

Equations

• Sag2010.instDecidableEqHeadCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Sag2010.instReprHeadCat : Repr HeadCat

Equations

• Sag2010.instReprHeadCat = { reprPrec := Sag2010.instReprHeadCat.repr }

def Sag2010.instReprHeadCat.repr : HeadCat → ℕ → Std.Format

Equations

• Sag2010.instReprHeadCat.repr Sag2010.HeadCat.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.HeadCat.s")).group prec✝
• Sag2010.instReprHeadCat.repr Sag2010.HeadCat.sOrCP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.HeadCat.sOrCP")).group prec✝

inductive Sag2010.ICStatus : Type

The [IC ±] (independent-clause) status a construction imposes, with its embedding profile ((31); §5.1, §5.3).

• mainClause : ICStatus
• embeddedOnly : ICStatus
• unconstrained : ICStatus

@[implicit_reducible]

instance Sag2010.instDecidableEqICStatus : DecidableEq ICStatus

Equations

• Sag2010.instDecidableEqICStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Sag2010.instReprICStatus.repr : ICStatus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Sag2010.instReprICStatus : Repr ICStatus

Equations

• Sag2010.instReprICStatus = { reprPrec := Sag2010.instReprICStatus.repr }

Clause-type supertype and inherited semantics ((30))

inductive Sag2010.ClauseType : Type

The clause-type supertype an F-G construction cross-classifies with in [Sag10]'s type hierarchy (§3, Appendix B). A nonsubject wh-interrogative construct is simultaneously a filler-head-cxt and an interrogative-cl; its semantic type is inherited from the latter and shared with non-F-G clauses of the same type.

• interrogativeCl : ClauseType
• relativeCl : ClauseType
• exclamativeCl : ClauseType
• declarativeCl : ClauseType

@[implicit_reducible]

instance Sag2010.instDecidableEqClauseType : DecidableEq ClauseType

Equations

• Sag2010.instDecidableEqClauseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Sag2010.instReprClauseType : Repr ClauseType

Equations

• Sag2010.instReprClauseType = { reprPrec := Sag2010.instReprClauseType.repr }

def Sag2010.instReprClauseType.repr : ClauseType → ℕ → Std.Format

Equations

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

inductive Sag2010.SemType : Type

Semantic type of a clause ((30), following [GS00]'s Vendlerian typology of facts, propositions, questions, and outcomes).

• question : SemType
• proposition : SemType
• fact : SemType
• austinean : SemType

@[implicit_reducible]

instance Sag2010.instDecidableEqSemType : DecidableEq SemType

Equations

• Sag2010.instDecidableEqSemType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Sag2010.instReprSemType : Repr SemType

Equations

• Sag2010.instReprSemType = { reprPrec := Sag2010.instReprSemType.repr }

def Sag2010.instReprSemType.repr : SemType → ℕ → Std.Format

Equations

• Sag2010.instReprSemType.repr Sag2010.SemType.question prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.SemType.question")).group prec✝
• Sag2010.instReprSemType.repr Sag2010.SemType.proposition prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.SemType.proposition")).group prec✝
• Sag2010.instReprSemType.repr Sag2010.SemType.fact prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.SemType.fact")).group prec✝
• Sag2010.instReprSemType.repr Sag2010.SemType.austinean prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.SemType.austinean")).group prec✝

def Sag2010.ClauseType.semType : ClauseType → SemType

The semantic type is a property of the clause-type supertype ((30)): it is determined by the clause type, not stipulated per construction.

Equations

• Sag2010.ClauseType.interrogativeCl.semType = Sag2010.SemType.question
• Sag2010.ClauseType.relativeCl.semType = Sag2010.SemType.proposition
• Sag2010.ClauseType.exclamativeCl.semType = Sag2010.SemType.fact
• Sag2010.ClauseType.declarativeCl.semType = Sag2010.SemType.austinean

inductive Sag2010.Composition : Type

The compositional contribution of a construction, kept distinct from the clause's semantic type. The wh-relative clause denotes a proposition ((30b)), but the wh-relative construction contributes a common-noun-phrase modifier λPλx[…] ((90)) — two things [Sag10] keeps separate.

• clausal : Composition
• cnpModifier : Composition

@[implicit_reducible]

instance Sag2010.instDecidableEqComposition : DecidableEq Composition

Equations

• Sag2010.instDecidableEqComposition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Sag2010.instReprComposition : Repr Composition

Equations

• Sag2010.instReprComposition = { reprPrec := Sag2010.instReprComposition.repr }

def Sag2010.instReprComposition.repr : Composition → ℕ → Std.Format

Equations

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

The construction bundle

structure Sag2010.FGConstruction : Type

The constraints a filler-gap construction imposes, indexed by [Sag10]'s parameters of variation ((6)). Models the descriptive parameter table of §2.1; clauseType records the cross-classifying supertype from which the semantic type is inherited. The (6f) island parameter is not a field here — islandhood is a Models fact about the construction's RSRL sort (FGClauseType.IsIsland), derived from the [GAP ⟨⟩] principle plus amalgamation, not stored as a tag.

• fillerCategories : List SynCat

  (6b) Allowed syntactic categories of the filler daughter ((25)).

• fillerWh : FillerWh

  (6a) The distinguished wh-element in the filler ((6a), (7)).

• headCategory : HeadCat

  (6c) Syntactic category of the head daughter ((27)).

• headInversion : InversionPolicy

  (6d) Inversion policy on the head daughter ((28)).

• headFiniteness : Finiteness

  (6d) Whether the head daughter may be infinitival ((29)).

• clauseType : ClauseType

  (6e) The cross-classifying clause-type supertype, which determines the semantic type ((30)).

• ic : ICStatus

  (6g) The [IC ±] status and embedding profile ((31)).

• composition : Composition

  Compositional contribution; cnpModifier for wh-relatives ((90)).

@[implicit_reducible]

instance Sag2010.instReprFGConstruction : Repr FGConstruction

Equations

• Sag2010.instReprFGConstruction = { reprPrec := Sag2010.instReprFGConstruction.repr }

def Sag2010.instReprFGConstruction.repr : FGConstruction → ℕ → Std.Format

Equations

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

def Sag2010.FGConstruction.semType (k : FGConstruction) : SemType

The semantic type of a construction, inherited from its clause supertype.

Equations

• k.semType = k.clauseType.semType

The five constructions

inductive Sag2010.FGClauseType : Type

The five types of English filler-gap clause ((1)-(5)).

• whInterrogative : FGClauseType
• whExclamative : FGClauseType
• topicalized : FGClauseType
• whRelative : FGClauseType
• theClause : FGClauseType

@[implicit_reducible]

instance Sag2010.instDecidableEqFGClauseType : DecidableEq FGClauseType

Equations

• Sag2010.instDecidableEqFGClauseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Sag2010.instReprFGClauseType.repr : FGClauseType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Sag2010.instReprFGClauseType : Repr FGClauseType

Equations

• Sag2010.instReprFGClauseType = { reprPrec := Sag2010.instReprFGClauseType.repr }

def Sag2010.allTypes : List FGClauseType

The five filler-gap clause types, in canonical order.

Equations

• Sag2010.allTypes = [Sag2010.FGClauseType.whInterrogative, Sag2010.FGClauseType.whExclamative, Sag2010.FGClauseType.topicalized, Sag2010.FGClauseType.whRelative, Sag2010.FGClauseType.theClause]

def Sag2010.fgParams : FGClauseType → FGConstruction

The parameter bundle of each filler-gap construction, with every value sourced from [Sag10] §2.1 and §5.

Equations

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

Inheritance from the filler-head-cxt supertype

[Sag10] derives the shared properties of filler-gap clauses from constraints on the superordinate filler-head-cxt, inherited by all five subtypes — not stipulated five times. We state the supertype constraint once and verify every construction inherits it.

def Sag2010.FGConstruction.FillerIsNonverbal (k : FGConstruction) : Prop

The filler-daughter constraint imposed by the filler-head-cxt supertype: the filler is [CAT nonverbal] ((25)).

Equations

• k.FillerIsNonverbal = ∀ cat ∈ k.fillerCategories, cat.IsNonverbal

@[implicit_reducible]

instance Sag2010.instDecidablePredFGConstructionFillerIsNonverbal : DecidablePred FGConstruction.FillerIsNonverbal

Equations

• Sag2010.instDecidablePredFGConstructionFillerIsNonverbal k = Sag2010.instDecidablePredFGConstructionFillerIsNonverbal._aux_1 k

theorem Sag2010.fg_inherits_nonverbal_filler (c : FGClauseType) : (fgParams c).FillerIsNonverbal

Every filler-gap construction inherits the [CAT nonverbal] filler constraint from filler-head-cxt — proved once for the whole family, never a verbal projection ((25)).

Cross-classification and inherited semantics ((30))

theorem Sag2010.semType_inherited (c : FGClauseType) : (fgParams c).semType = (fgParams c).clauseType.semType

The semantic type is inherited from the clause-type supertype: it is not an independent per-construction stipulation.

theorem Sag2010.semTypes : List.map (fun (c : FGClauseType) => (fgParams c).semType) allTypes = [SemType.question, SemType.fact, SemType.austinean, SemType.proposition, SemType.austinean]

The five constructions realize all four semantic types, with topicalization and the-clause sharing austinean — [Sag10]'s point that F-G clauses are not semantically uniform ((30)).

theorem Sag2010.interrogative_question_via_clauseType : (fgParams FGClauseType.whInterrogative).clauseType = ClauseType.interrogativeCl ∧ ClauseType.interrogativeCl.semType = SemType.question

Wh-interrogatives inherit question semantics from interrogative-cl, the supertype they share with non-filler-gap (e.g. subject) interrogatives.

theorem Sag2010.topicalized_theClause_share_clauseType : (fgParams FGClauseType.topicalized).clauseType = (fgParams FGClauseType.theClause).clauseType

Topicalization and the-clause share the declarative-cl supertype, hence the same austinean semantics — one shared fact, not two stipulations ((30d), (30e)). The declarative-cl membership of topicalization follows [Sag10]'s Appendix-B hierarchy; construction (61) states only ↑filler-head-cxt explicitly.

Grounding in the RSRL construct hierarchy ([SCA+20b] Figs. 6–7)

The five clause types are sorts in the RSRL construct hierarchy (Syntax/HPSG/Construction), where the filler-head inheritance and the clausal cross-classification above are theorems about the sort order — the model-theoretic substrate ([Ric00]) under the fgParams record.

def Sag2010.fgSort : FGClauseType → HPSG.Construction.Srt

Each filler-gap clause type as a construct sort in the RSRL hierarchy.

Equations

• Sag2010.fgSort Sag2010.FGClauseType.whInterrogative = HPSG.Construction.Srt.nsWhIntCl
• Sag2010.fgSort Sag2010.FGClauseType.whExclamative = HPSG.Construction.Srt.whExclCl
• Sag2010.fgSort Sag2010.FGClauseType.topicalized = HPSG.Construction.Srt.topCl
• Sag2010.fgSort Sag2010.FGClauseType.whRelative = HPSG.Construction.Srt.whRelCl
• Sag2010.fgSort Sag2010.FGClauseType.theClause = HPSG.Construction.Srt.theCl

theorem Sag2010.fgSort_filler_head (c : FGClauseType) : fgSort c ≤ HPSG.Construction.Srt.fillerHeadCxt

Every clause type is a filler-head construct in the RSRL hierarchy, so it inherits filler-head-cxt's constraints (head verbal, filler↔gap token identity) proved in Construction.lean — the model-theoretic ground of fg_inherits_nonverbal_filler.

def Sag2010.clauseTypeSort : ClauseType → HPSG.Construction.Srt

The local ClauseType as the matching RSRL clausal sort (Fig. 7).

Equations

• Sag2010.clauseTypeSort Sag2010.ClauseType.interrogativeCl = HPSG.Construction.Srt.interrogativeCl
• Sag2010.clauseTypeSort Sag2010.ClauseType.relativeCl = HPSG.Construction.Srt.relativeCl
• Sag2010.clauseTypeSort Sag2010.ClauseType.exclamativeCl = HPSG.Construction.Srt.exclamativeCl
• Sag2010.clauseTypeSort Sag2010.ClauseType.declarativeCl = HPSG.Construction.Srt.declarativeCl

theorem Sag2010.fgSort_matches_clauseType (c : FGClauseType) : fgSort c ≤ clauseTypeSort (fgParams c).clauseType

The RSRL clausal cross-classification agrees with the local clauseType assignment: each clause type's construct sits below the RSRL clausal sort matching (fgParams c).clauseType. The cross-classification of this section is thus the same fact as the RSRL sort order.

Inversion ((28))

theorem Sag2010.inversionPolicies : List.map (fun (c : FGClauseType) => (fgParams c).headInversion) allTypes = [InversionPolicy.iffIndependent, InversionPolicy.prohibited, InversionPolicy.prohibited, InversionPolicy.prohibited, InversionPolicy.optional]

Inversion policy across the family: only wh-interrogatives covary with independence (the IC/INV identity of (80)); topicalization, exclamatives, and relatives never invert ((28b)); noninitial the-clauses invert optionally ((28c)).

Islands as a property of the construction type ([Sag10] §5.1)

[Sag10] argues islandhood is a construction-specific [GAP ⟨⟩] restriction, not universal Subjacency. Here islandhood is a Models fact about the construction's sort in the canonical RSRL signature (Syntax/HPSG/Construction): a construction is an absolute island iff its construct cannot host a second, undischarged gap — the [GAP ⟨⟩] principle plus amalgamation reject it.

def Sag2010.FGClauseType.IsIsland : FGClauseType → Prop

A filler-gap construction is an absolute extraction island iff its construct cannot host a second, undischarged gap — a Models fact about the RSRL sort ((67), (73), (74)), derived from the [GAP ⟨⟩] principle plus amalgamation, not stored as a tag. Each case is ¬ Models of the construction's two-gap RSRL worked model (Syntax/HPSG/Construction): an island rejects the second gap, a non-island admits it.

Equations

• Sag2010.FGClauseType.whInterrogative.IsIsland = ¬HPSG.Construction.nsWhIntSecondGap.Models HPSG.Construction.grammar
• Sag2010.FGClauseType.whExclamative.IsIsland = ¬HPSG.Construction.whExclSecondGap.Models HPSG.Construction.grammar
• Sag2010.FGClauseType.topicalized.IsIsland = ¬HPSG.Construction.topClSecondGap.Models HPSG.Construction.grammar
• Sag2010.FGClauseType.whRelative.IsIsland = ¬HPSG.Construction.whRelSecondGap.Models HPSG.Construction.grammar
• Sag2010.FGClauseType.theClause.IsIsland = ¬HPSG.Construction.theClSecondGap.Models HPSG.Construction.grammar

@[implicit_reducible]

instance Sag2010.instDecidablePredFGClauseTypeIsIsland : DecidablePred FGClauseType.IsIsland

Equations

• Sag2010.instDecidablePredFGClauseTypeIsIsland Sag2010.FGClauseType.whInterrogative = Sag2010.instDecidablePredFGClauseTypeIsIsland._aux_1
• Sag2010.instDecidablePredFGClauseTypeIsIsland Sag2010.FGClauseType.whExclamative = Sag2010.instDecidablePredFGClauseTypeIsIsland._aux_3
• Sag2010.instDecidablePredFGClauseTypeIsIsland Sag2010.FGClauseType.topicalized = Sag2010.instDecidablePredFGClauseTypeIsIsland._aux_5
• Sag2010.instDecidablePredFGClauseTypeIsIsland Sag2010.FGClauseType.whRelative = Sag2010.instDecidablePredFGClauseTypeIsIsland._aux_7
• Sag2010.instDecidablePredFGClauseTypeIsIsland Sag2010.FGClauseType.theClause = Sag2010.instDecidablePredFGClauseTypeIsIsland._aux_9

theorem Sag2010.topicalized_isIsland : FGClauseType.topicalized.IsIsland

Topicalization is an absolute island ((67)): a topicalized construct with a second gap is rejected by the [GAP ⟨⟩] principle.

theorem Sag2010.exclamative_isIsland : FGClauseType.whExclamative.IsIsland

Wh-exclamatives are absolute islands ((74)).

theorem Sag2010.interrogative_relative_theClause_not_islands : ¬FGClauseType.whInterrogative.IsIsland ∧ ¬FGClauseType.whRelative.IsIsland ∧ ¬FGClauseType.theClause.IsIsland

Wh-interrogatives, wh-relatives, and the-clauses are not constructional islands: a second gap amalgamates freely (no [GAP ⟨⟩]). For wh-relatives this diverges from the classic Complex-NP Constraint — [Sag10] re-attributes the residual degradation to processing ([HS10]), not grammar.

def Sag2010.islandConstructions : List FGClauseType

The filler-gap constructions that are absolute extraction islands — exactly those whose construct rejects a second gap ((67), (73), (74)). Computed from the RSRL Models verdict, not stipulated.

Equations

• Sag2010.islandConstructions = List.filter (fun (c : Sag2010.FGClauseType) => decide c.IsIsland) Sag2010.allTypes

theorem Sag2010.islandConstructions_eq : islandConstructions = [FGClauseType.whExclamative, FGClauseType.topicalized]

Exactly wh-exclamatives and topicalization are filler-gap islands.

Reconciliation with the Ross taxonomy and the HPSG mechanism

[Sag10]'s construction-typed islands classify whole construction types, orthogonal to [Ros67]'s configurational island domains. The chronologically-later account (Sag) draws the comparison.

theorem Sag2010.island_grounded_in_rsrl : ¬HPSG.Construction.islandTwoGap.Models HPSG.Construction.grammar

The construction-typed IsIsland verdicts are grounded in the same RSRL gap mechanism as the SLASH analysis: the model-theoretic content of an absolute island is [GAP ⟨⟩] plus amalgamation blocking a second gap. Derived from [SWB03]'s authoritative islands_rsrl_grounded (over the canonical Syntax/HPSG/Construction signature), not re-stated — the construction-tag level and the gap-list mechanism agree.

theorem Sag2010.topicalized_island_agrees_swb : FGClauseType.topicalized.IsIsland ∧ ¬HPSG.Construction.islandTwoGap.Models HPSG.Construction.grammar

Agreement with [SWB03]: the topicalization island is the same datum in two analyses — Sag's [GAP ⟨⟩] topicalization construct and the generic HPSG SLASH model both block a second gap.

theorem Sag2010.relative_diverges_from_cnpc : HPSG.Construction.whRelSecondGap.Models HPSG.Construction.grammar ∧ ¬HPSG.Construction.islandTwoGap.Models HPSG.Construction.grammar

The sharpest divergence from [Ros67]: the relative clause is Ross's paradigm Complex-NP-Constraint island, yet [Sag10]'s wh-relative construction is no grammatical island — its construct admits a second gap, whereas a configurational island (Ross's CNPC domain, modeled as a generic absolute island) blocks it. The residual effect is processing, not grammar ([HS10]).

Surface clause form (bridge to Features.ClauseForm)

def Sag2010.clauseForm : FGClauseType → Option Features.ClauseForm

Surface clause form, where a construction has a direct correspondent in Features.ClauseForm. Wh-interrogatives map to the independent (matrix) form; topicalization and the-clause are declarative; exclamatives and relatives have no ClauseForm correspondent.

Equations

• Sag2010.clauseForm Sag2010.FGClauseType.whInterrogative = some Features.ClauseForm.matrixQuestion
• Sag2010.clauseForm Sag2010.FGClauseType.topicalized = some Features.ClauseForm.declarative
• Sag2010.clauseForm Sag2010.FGClauseType.theClause = some Features.ClauseForm.declarative
• Sag2010.clauseForm Sag2010.FGClauseType.whExclamative = none
• Sag2010.clauseForm Sag2010.FGClauseType.whRelative = none

theorem Sag2010.topicalized_is_declarative_form : clauseForm FGClauseType.topicalized = some Features.ClauseForm.declarative

Topicalization corresponds to a declarative surface form.

theorem Sag2010.interrogative_is_question_form : clauseForm FGClauseType.whInterrogative = some Features.ClauseForm.matrixQuestion

Wh-interrogatives correspond to the matrix-question surface form.

Wh-word inventory (Table 1)

[Sag10]'s Table 1 classifies each wh-form by syntactic category with a three-valued judgment (+ full, % for some speakers, - excluded) across the three wh-construction types. The category splits carry Sag's central claim that 'wh-expression' is not a unitary category (§2.1). Where Table 1 and the worked examples diverge (e.g. what·NP relative is - in the table but % at (11c)), this transcribes the printed table.

inductive Sag2010.WhStatus : Type

A three-valued participation judgment (Table 1: +, %, -).

• full : WhStatus
• someSpeakers : WhStatus
• excluded : WhStatus

@[implicit_reducible]

instance Sag2010.instDecidableEqWhStatus : DecidableEq WhStatus

Equations

• Sag2010.instDecidableEqWhStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Sag2010.instReprWhStatus.repr : WhStatus → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Sag2010.instReprWhStatus.repr Sag2010.WhStatus.full prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhStatus.full")).group prec✝
• Sag2010.instReprWhStatus.repr Sag2010.WhStatus.excluded prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhStatus.excluded")).group prec✝

@[implicit_reducible]

instance Sag2010.instReprWhStatus : Repr WhStatus

Equations

• Sag2010.instReprWhStatus = { reprPrec := Sag2010.instReprWhStatus.repr }

inductive Sag2010.WhForm : Type

The wh-forms of Table 1.

• who : WhForm
• whose : WhForm
• what : WhForm
• whatA : WhForm
• which : WhForm
• how : WhForm
• when : WhForm
• whereWh : WhForm
• why : WhForm

@[implicit_reducible]

instance Sag2010.instDecidableEqWhForm : DecidableEq WhForm

Equations

• Sag2010.instDecidableEqWhForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Sag2010.instReprWhForm.repr : WhForm → ℕ → Std.Format

Equations

• Sag2010.instReprWhForm.repr Sag2010.WhForm.who prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.who")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.whose prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.whose")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.what prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.what")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.whatA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.whatA")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.which prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.which")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.how prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.how")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.when prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.when")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.whereWh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.whereWh")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.why prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.why")).group prec✝

@[implicit_reducible]

instance Sag2010.instReprWhForm : Repr WhForm

Equations

• Sag2010.instReprWhForm = { reprPrec := Sag2010.instReprWhForm.repr }

inductive Sag2010.WhCategory : Type

The syntactic categories a wh-form bears in Table 1.

• np : WhCategory
• det : WhCategory
• detSing : WhCategory
• detPl : WhCategory
• degree : WhCategory
• advpManner : WhCategory
• ap : WhCategory
• ppTime : WhCategory
• ppPlace : WhCategory
• ppReason : WhCategory

@[implicit_reducible]

instance Sag2010.instDecidableEqWhCategory : DecidableEq WhCategory

Equations

• Sag2010.instDecidableEqWhCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Sag2010.instReprWhCategory : Repr WhCategory

Equations

• Sag2010.instReprWhCategory = { reprPrec := Sag2010.instReprWhCategory.repr }

def Sag2010.instReprWhCategory.repr : WhCategory → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.np prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.np")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.det prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.det")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.detSing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.detSing")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.detPl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.detPl")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.degree prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.degree")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.ap prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.ap")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.ppTime prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.ppTime")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.ppPlace prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.ppPlace")).group prec✝

structure Sag2010.WhWordProfile : Type

One row of Table 1: a wh-form in a given category, with its participation in each of the three wh-construction types.

• form : WhForm
• category : WhCategory
• interrogative : WhStatus
• exclamative : WhStatus
• relative : WhStatus

def Sag2010.instDecidableEqWhWordProfile.decEq (x✝ x✝¹ : WhWordProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Sag2010.instDecidableEqWhWordProfile : DecidableEq WhWordProfile

Equations

• Sag2010.instDecidableEqWhWordProfile = Sag2010.instDecidableEqWhWordProfile.decEq

@[implicit_reducible]

instance Sag2010.instReprWhWordProfile : Repr WhWordProfile

Equations

• Sag2010.instReprWhWordProfile = { reprPrec := Sag2010.instReprWhWordProfile.repr }

def Sag2010.instReprWhWordProfile.repr : WhWordProfile → ℕ → Std.Format

Equations

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

def Sag2010.whWordProfiles : List WhWordProfile

[Sag10] Table 1, faithful to its category splits and three-valued judgments.

Equations

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

theorem Sag2010.no_universal_wh_word (w : WhWordProfile) : w ∈ whWordProfiles → ¬(w.interrogative = WhStatus.full ∧ w.exclamative = WhStatus.full ∧ w.relative = WhStatus.full)

No wh-form/category row is a full participant in all three construction types — [Sag10]'s point that 'wh-expression' is not a unitary category (§2.1). The closest cases (e.g. manner how) are only % in the relative column.

theorem Sag2010.how_crosses_interrogative_exclamative : ∃ w ∈ whWordProfiles, w.form = WhForm.how ∧ w.interrogative = WhStatus.full ∧ w.exclamative = WhStatus.full

The manner wh-word how participates fully in both interrogatives and exclamatives — one of the few wh-forms crossing that boundary ((18)-(20)).