inductive Phenomena.FillerGap.Studies.Sag2010.FGClauseType : Type

The five types of English filler-gap clause.

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

instance Phenomena.FillerGap.Studies.Sag2010.instReprFGClauseType : Repr FGClauseType

Equations

• Phenomena.FillerGap.Studies.Sag2010.instReprFGClauseType = { reprPrec := Phenomena.FillerGap.Studies.Sag2010.instReprFGClauseType.repr }

def Phenomena.FillerGap.Studies.Sag2010.instReprFGClauseType.repr : FGClauseType → Nat → Std.Format

Equations

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

instance Phenomena.FillerGap.Studies.Sag2010.instDecidableEqFGClauseType : DecidableEq FGClauseType

Equations

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

def Phenomena.FillerGap.Studies.Sag2010.instBEqFGClauseType.beq : FGClauseType → FGClauseType → Bool

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqFGClauseType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.FillerGap.Studies.Sag2010.instBEqFGClauseType : BEq FGClauseType

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqFGClauseType = { beq := Phenomena.FillerGap.Studies.Sag2010.instBEqFGClauseType.beq }

inductive Phenomena.FillerGap.Studies.Sag2010.FillerWhType : Type

What kind of distinguished wh-element appears in the filler daughter. (§2.1, parameter 6a)

• none : FillerWhType
• interrogative : FillerWhType
• exclamative : FillerWhType
• relative : FillerWhType
• the : FillerWhType

instance Phenomena.FillerGap.Studies.Sag2010.instReprFillerWhType : Repr FillerWhType

Equations

• Phenomena.FillerGap.Studies.Sag2010.instReprFillerWhType = { reprPrec := Phenomena.FillerGap.Studies.Sag2010.instReprFillerWhType.repr }

def Phenomena.FillerGap.Studies.Sag2010.instReprFillerWhType.repr : FillerWhType → Nat → Std.Format

Equations

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

instance Phenomena.FillerGap.Studies.Sag2010.instDecidableEqFillerWhType : DecidableEq FillerWhType

Equations

• Phenomena.FillerGap.Studies.Sag2010.instDecidableEqFillerWhType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.FillerGap.Studies.Sag2010.instBEqFillerWhType.beq : FillerWhType → FillerWhType → Bool

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqFillerWhType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.FillerGap.Studies.Sag2010.instBEqFillerWhType : BEq FillerWhType

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqFillerWhType = { beq := Phenomena.FillerGap.Studies.Sag2010.instBEqFillerWhType.beq }

inductive Phenomena.FillerGap.Studies.Sag2010.InversionRequirement : Type

Constraints on head daughter inversion (§2.1, parameter 6d / example 28).

• required : InversionRequirement
• prohibited : InversionRequirement
• optional : InversionRequirement

instance Phenomena.FillerGap.Studies.Sag2010.instReprInversionRequirement : Repr InversionRequirement

Equations

• Phenomena.FillerGap.Studies.Sag2010.instReprInversionRequirement = { reprPrec := Phenomena.FillerGap.Studies.Sag2010.instReprInversionRequirement.repr }

def Phenomena.FillerGap.Studies.Sag2010.instReprInversionRequirement.repr : InversionRequirement → Nat → Std.Format

Equations

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

instance Phenomena.FillerGap.Studies.Sag2010.instDecidableEqInversionRequirement : DecidableEq InversionRequirement

Equations

• Phenomena.FillerGap.Studies.Sag2010.instDecidableEqInversionRequirement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.FillerGap.Studies.Sag2010.instBEqInversionRequirement : BEq InversionRequirement

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqInversionRequirement = { beq := Phenomena.FillerGap.Studies.Sag2010.instBEqInversionRequirement.beq }

def Phenomena.FillerGap.Studies.Sag2010.instBEqInversionRequirement.beq : InversionRequirement → InversionRequirement → Bool

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqInversionRequirement.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Phenomena.FillerGap.Studies.Sag2010.Finiteness : Type

Whether head daughter can be infinitival (§2.1, parameter 6d / example 29).

• finiteOnly : Finiteness
• infinitivalPossible : Finiteness

instance Phenomena.FillerGap.Studies.Sag2010.instReprFiniteness : Repr Finiteness

Equations

• Phenomena.FillerGap.Studies.Sag2010.instReprFiniteness = { reprPrec := Phenomena.FillerGap.Studies.Sag2010.instReprFiniteness.repr }

def Phenomena.FillerGap.Studies.Sag2010.instReprFiniteness.repr : Finiteness → Nat → Std.Format

Equations

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

instance Phenomena.FillerGap.Studies.Sag2010.instDecidableEqFiniteness : DecidableEq Finiteness

Equations

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

instance Phenomena.FillerGap.Studies.Sag2010.instBEqFiniteness : BEq Finiteness

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqFiniteness = { beq := Phenomena.FillerGap.Studies.Sag2010.instBEqFiniteness.beq }

def Phenomena.FillerGap.Studies.Sag2010.instBEqFiniteness.beq : Finiteness → Finiteness → Bool

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqFiniteness.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Phenomena.FillerGap.Studies.Sag2010.FGSemanticType : Type

Semantic type of the clause (§2.1, example 30; follows @cite{ginzburg-sag-2000}).

• question : FGSemanticType
• fact : FGSemanticType
• austinean : FGSemanticType
• modifier : FGSemanticType

instance Phenomena.FillerGap.Studies.Sag2010.instReprFGSemanticType : Repr FGSemanticType

Equations

• Phenomena.FillerGap.Studies.Sag2010.instReprFGSemanticType = { reprPrec := Phenomena.FillerGap.Studies.Sag2010.instReprFGSemanticType.repr }

def Phenomena.FillerGap.Studies.Sag2010.instReprFGSemanticType.repr : FGSemanticType → Nat → Std.Format

Equations

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

instance Phenomena.FillerGap.Studies.Sag2010.instDecidableEqFGSemanticType : DecidableEq FGSemanticType

Equations

• Phenomena.FillerGap.Studies.Sag2010.instDecidableEqFGSemanticType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.FillerGap.Studies.Sag2010.instBEqFGSemanticType : BEq FGSemanticType

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqFGSemanticType = { beq := Phenomena.FillerGap.Studies.Sag2010.instBEqFGSemanticType.beq }

def Phenomena.FillerGap.Studies.Sag2010.instBEqFGSemanticType.beq : FGSemanticType → FGSemanticType → Bool

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqFGSemanticType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Phenomena.FillerGap.Studies.Sag2010.Independence : Type

Whether the clause must/can be independent (§2.1, parameter 6g / example 31).

• required : Independence
• prohibited : Independence
• either : Independence

def Phenomena.FillerGap.Studies.Sag2010.instReprIndependence.repr : Independence → Nat → Std.Format

Equations

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

instance Phenomena.FillerGap.Studies.Sag2010.instReprIndependence : Repr Independence

Equations

• Phenomena.FillerGap.Studies.Sag2010.instReprIndependence = { reprPrec := Phenomena.FillerGap.Studies.Sag2010.instReprIndependence.repr }

instance Phenomena.FillerGap.Studies.Sag2010.instDecidableEqIndependence : DecidableEq Independence

Equations

• Phenomena.FillerGap.Studies.Sag2010.instDecidableEqIndependence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.FillerGap.Studies.Sag2010.instBEqIndependence.beq : Independence → Independence → Bool

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqIndependence.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.FillerGap.Studies.Sag2010.instBEqIndependence : BEq Independence

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqIndependence = { beq := Phenomena.FillerGap.Studies.Sag2010.instBEqIndependence.beq }

structure Phenomena.FillerGap.Studies.Sag2010.FGParameters : Type

The 7 parameters of variation across F-G clause types (§2.1, example 6).

Each parameter corresponds to a feature already formalized elsewhere in linglib; the bridge theorems below verify consistency.

• fillerWhType : FillerWhType

  (6a) What wh-element in the filler?

• headInversion : InversionRequirement

  (6d) Must/can head be inverted?

• headFiniteness : Finiteness

  (6d) Can head be infinitival?

• semanticType : FGSemanticType

  (6e) Semantic type of the clause

• isIsland : Bool

  (6f) Is this an extraction island?

• independence : Independence

  (6g) Must this be independent?

• fillerIsNonverbal : Bool

  (6b) Allowed filler categories (NP, PP, AP, AdvP, etc.)

def Phenomena.FillerGap.Studies.Sag2010.instReprFGParameters.repr : FGParameters → Nat → Std.Format

Equations

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

instance Phenomena.FillerGap.Studies.Sag2010.instReprFGParameters : Repr FGParameters

Equations

• Phenomena.FillerGap.Studies.Sag2010.instReprFGParameters = { reprPrec := Phenomena.FillerGap.Studies.Sag2010.instReprFGParameters.repr }

def Phenomena.FillerGap.Studies.Sag2010.instDecidableEqFGParameters.decEq (x✝ x✝¹ : FGParameters) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.FillerGap.Studies.Sag2010.instDecidableEqFGParameters : DecidableEq FGParameters

Equations

• Phenomena.FillerGap.Studies.Sag2010.instDecidableEqFGParameters = Phenomena.FillerGap.Studies.Sag2010.instDecidableEqFGParameters.decEq

def Phenomena.FillerGap.Studies.Sag2010.instBEqFGParameters.beq : FGParameters → FGParameters → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.FillerGap.Studies.Sag2010.instBEqFGParameters.beq x✝¹ x✝ = false

instance Phenomena.FillerGap.Studies.Sag2010.instBEqFGParameters : BEq FGParameters

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqFGParameters = { beq := Phenomena.FillerGap.Studies.Sag2010.instBEqFGParameters.beq }

def Phenomena.FillerGap.Studies.Sag2010.whInterrogativeParams : FGParameters

Wh-interrogative parameters (§5.3, constructions 80–81). "Who did they visit?" — interrogative wh, inverted in matrix, question semantics.

Equations

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

def Phenomena.FillerGap.Studies.Sag2010.whExclamativeParams : FGParameters

Wh-exclamative parameters (§5.2, construction 70). "What a fool he is!" — exclamative wh, uninverted, fact semantics.

Equations

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

def Phenomena.FillerGap.Studies.Sag2010.topicalizedParams : FGParameters

Topicalization parameters (§5.1, construction 61). "The bagels, I like." — no wh, uninverted, austinean semantics.

Equations

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

def Phenomena.FillerGap.Studies.Sag2010.whRelativeParams : FGParameters

Wh-relative parameters (§5.4, constructions 90–92). "the person who they nominated" — relative wh, uninverted, modifier semantics.

Equations

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

def Phenomena.FillerGap.Studies.Sag2010.theClauseParams : FGParameters

The-clause parameters (§5.5, construction 108). "The more you read, the more you understand." — degree marker the, optional inversion, austinean semantics.

Equations

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

def Phenomena.FillerGap.Studies.Sag2010.fgParams : FGClauseType → FGParameters

Map each F-G clause type to its parameters.

Equations

• Phenomena.FillerGap.Studies.Sag2010.fgParams Phenomena.FillerGap.Studies.Sag2010.FGClauseType.whInterrogative = Phenomena.FillerGap.Studies.Sag2010.whInterrogativeParams
• Phenomena.FillerGap.Studies.Sag2010.fgParams Phenomena.FillerGap.Studies.Sag2010.FGClauseType.whExclamative = Phenomena.FillerGap.Studies.Sag2010.whExclamativeParams
• Phenomena.FillerGap.Studies.Sag2010.fgParams Phenomena.FillerGap.Studies.Sag2010.FGClauseType.topicalized = Phenomena.FillerGap.Studies.Sag2010.topicalizedParams
• Phenomena.FillerGap.Studies.Sag2010.fgParams Phenomena.FillerGap.Studies.Sag2010.FGClauseType.whRelative = Phenomena.FillerGap.Studies.Sag2010.whRelativeParams
• Phenomena.FillerGap.Studies.Sag2010.fgParams Phenomena.FillerGap.Studies.Sag2010.FGClauseType.theClause = Phenomena.FillerGap.Studies.Sag2010.theClauseParams

Semantic type distinctions (§2.1, example 30)

Each clause type has a distinct semantic type — this is one of Sag's key arguments that F-G constructions are not uniform.

theorem Phenomena.FillerGap.Studies.Sag2010.interrogative_denotes_question : (fgParams FGClauseType.whInterrogative).semanticType = FGSemanticType.question

theorem Phenomena.FillerGap.Studies.Sag2010.exclamative_denotes_fact : (fgParams FGClauseType.whExclamative).semanticType = FGSemanticType.fact

theorem Phenomena.FillerGap.Studies.Sag2010.topicalized_denotes_austinean : (fgParams FGClauseType.topicalized).semanticType = FGSemanticType.austinean

theorem Phenomena.FillerGap.Studies.Sag2010.relative_denotes_modifier : (fgParams FGClauseType.whRelative).semanticType = FGSemanticType.modifier

theorem Phenomena.FillerGap.Studies.Sag2010.theClause_denotes_austinean : (fgParams FGClauseType.theClause).semanticType = FGSemanticType.austinean

Inversion parameter (§2.1, example 28)

Only wh-interrogatives require inversion; topicalization/relatives/exclamatives prohibit it; the-clauses allow it optionally.

theorem Phenomena.FillerGap.Studies.Sag2010.only_interrogative_requires_inversion : (fgParams FGClauseType.whInterrogative).headInversion = InversionRequirement.required ∧ (fgParams FGClauseType.whExclamative).headInversion = InversionRequirement.prohibited ∧ (fgParams FGClauseType.topicalized).headInversion = InversionRequirement.prohibited ∧ (fgParams FGClauseType.whRelative).headInversion = InversionRequirement.prohibited ∧ (fgParams FGClauseType.theClause).headInversion = InversionRequirement.optional

Island status

Topicalization and wh-exclamatives are extraction islands (§5.1 ex. 67, §5.2 ex. 73–74). Wh-interrogatives, relatives, and the-clauses are not.

theorem Phenomena.FillerGap.Studies.Sag2010.topicalized_is_island : (fgParams FGClauseType.topicalized).isIsland = true

theorem Phenomena.FillerGap.Studies.Sag2010.exclamative_is_island : (fgParams FGClauseType.whExclamative).isIsland = true

theorem Phenomena.FillerGap.Studies.Sag2010.interrogative_not_island : (fgParams FGClauseType.whInterrogative).isIsland = false

theorem Phenomena.FillerGap.Studies.Sag2010.relative_not_island : (fgParams FGClauseType.whRelative).isIsland = false

Independence constraints (§2.1 / example 31)

Topicalization requires independence; relatives require embedding.

theorem Phenomena.FillerGap.Studies.Sag2010.topicalized_requires_independence : (fgParams FGClauseType.topicalized).independence = Independence.required

theorem Phenomena.FillerGap.Studies.Sag2010.relative_requires_embedding : (fgParams FGClauseType.whRelative).independence = Independence.prohibited

All fillers are nonverb@cite{hofmeister-sag-2010} §2.1 / example 25: filler daughter is always nonverbal across

all five F-G clause types. This is a constraint on the superordinate filler-head construction (58), not construction-specific.

theorem Phenomena.FillerGap.Studies.Sag2010.all_fillers_nonverbal : ([FGClauseType.whInterrogative, FGClauseType.whExclamative, FGClauseType.topicalized, FGClauseType.whRelative, FGClauseType.theClause].all fun (c : FGClauseType) => (fgParams c).fillerIsNonverbal) = true

Connection to ConstraintType in Islands/Data

@cite{hofmeister-sag-2010} @cite{sag-2010} argues that island constraints are construction-specific GAP restrictions, not universal Subjacency. The topicalization construction has [GAP ⟨⟩] on its mother, making it an absolute extraction island. This matches the ConstraintType classification from Islands/Data.

def Phenomena.FillerGap.Studies.Sag2010.islandConstructions : List FGClauseType

The island constructions in @cite{hofmeister-sag-2010} correspond to specific constraint types in the island classification system. The CNPC (complexNP) is the island tested in @cite{hofmeister-sag-2010}; Sag's topicalization and exclamative islands are additional construction-specific cases.

Equations

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

theorem Phenomena.FillerGap.Studies.Sag2010.island_constructions_are : islandConstructions = [FGClauseType.whExclamative, FGClauseType.topicalized]

Exactly topicalization and wh-exclamatives are F-G island constructions.

Connection to ClauseType in Core/Basic

Sag's semantic types map to the existing ClauseType for the clause types that have direct correspondences.

theorem Phenomena.FillerGap.Studies.Sag2010.interrogative_maps_to_question_clause : (fgParams FGClauseType.whInterrogative).semanticType = FGSemanticType.question ∧ (fgParams FGClauseType.whInterrogative).independence = Independence.either

Wh-interrogatives correspond to matrixQuestion or embeddedQuestion depending on independence.

theorem Phenomena.FillerGap.Studies.Sag2010.topicalized_maps_to_declarative : (fgParams FGClauseType.topicalized).semanticType = FGSemanticType.austinean ∧ (fgParams FGClauseType.topicalized).headInversion = InversionRequirement.prohibited ∧ (fgParams FGClauseType.topicalized).independence = Independence.required

Topicalization corresponds to declarative clauses (austinean semantics, independent, uninverted).

structure Phenomena.FillerGap.Studies.Sag2010.WhWordProfile : Type

Functions of wh-words across construction types.

Each wh-word is classified by which F-G clause types it participates. '+' = full participant, '%' = for some speakers, '-' = excluded.

• form : String
• interrogative : Bool
• exclamative : Bool
• relative : Bool

def Phenomena.FillerGap.Studies.Sag2010.instReprWhWordProfile.repr : WhWordProfile → Nat → Std.Format

Equations

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

instance Phenomena.FillerGap.Studies.Sag2010.instReprWhWordProfile : Repr WhWordProfile

Equations

• Phenomena.FillerGap.Studies.Sag2010.instReprWhWordProfile = { reprPrec := Phenomena.FillerGap.Studies.Sag2010.instReprWhWordProfile.repr }

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

Equations

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

instance Phenomena.FillerGap.Studies.Sag2010.instDecidableEqWhWordProfile : DecidableEq WhWordProfile

Equations

• Phenomena.FillerGap.Studies.Sag2010.instDecidableEqWhWordProfile = Phenomena.FillerGap.Studies.Sag2010.instDecidableEqWhWordProfile.decEq

def Phenomena.FillerGap.Studies.Sag2010.instBEqWhWordProfile.beq : WhWordProfile → WhWordProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.FillerGap.Studies.Sag2010.instBEqWhWordProfile.beq x✝¹ x✝ = false

instance Phenomena.FillerGap.Studies.Sag2010.instBEqWhWordProfile : BEq WhWordProfile

Equations

• Phenomena.FillerGap.Studies.Sag2010.instBEqWhWordProfile = { beq := Phenomena.FillerGap.Studies.Sag2010.instBEqWhWordProfile.beq }

def Phenomena.FillerGap.Studies.Sag2010.whWordProfiles : List WhWordProfile

Equations

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

theorem Phenomena.FillerGap.Studies.Sag2010.no_universal_wh_word : (whWordProfiles.all fun (w : WhWordProfile) => w.interrogative && w.exclamative && w.relative) = false

No wh-word participates in all three construction types uniformly. This supports Sag's claim that 'wh-expression' is not a unitary category.

theorem Phenomena.FillerGap.Studies.Sag2010.how_crosses_interrog_exclam : (List.filter (fun (w : WhWordProfile) => w.interrogative && w.exclamative) whWordProfiles).length ≥ 1

'how' participates in both interrogatives and exclamatives — one of the few wh-words that crosses this boundary (examples 18–20).