Typology.ExpressiveModifier

@cite{pesetsky-1987} @cite{chou-2012} @cite{merchant-2002} @cite{hoeksema-napoli-2008} @cite{jackendoff-audring-2020} @cite{chan-shen-2026}

Per-language typological substrate for aggressively non-D-linked (ANDL) wh-modifiers — the-hell, the heck, the fuck, the devil, the dickens, in the world, in God's name (English; @cite{hoeksema-napoli-2008}, @cite{jackendoff-audring-2020}); daodi 到底 (Mandarin; @cite{chou-2012}); ittai (Japanese); ttaeyche (Korean); zum-Teufel (German); etc.

The shared empirical generalization (@cite{pesetsky-1987}): ANDL modifiers have a distributional restriction that bare wh-words do not. Different languages and different ANDL items vary along a small set of typological parameters, formalized here.

Provenance

Moved from Core/Lexical/ExpressiveModifier.lean in the cleanup that dissolved Core/Lexical/. The file's per-language entry-schema + abstract-licensing-predicate shape (Fragment-importable, syntax-framework- neutral) matches Typology/PolarityMarking.lean and Typology/Negation.lean, not the framework-agnostic substrate shape Core/ is for.

Framework commitment. The parasitic/independent dichotomy (ANDLMovementType) is the single typological parameter @cite{chan-shen-2026} isolate as distinguishing English/Singlish the-hell from Mandarin daodi. This is one carve-up among several in the ANDL literature — alternatives exist that classify these items by syntactic category (DP-modifier vs. adverb), by intervention profile, or by perspectival semantics rather than by movement source. The schema is intentionally thin: only the Chan-Shen 2026 dimension is encoded; competing classifications attach as separate predicates in Theories/.

Out of scope (lives in Theories)

This file does not commit to a syntactic framework. It carries no features, no Spec-CP, no Agree, no AttP. A Minimalist analysis (POV features [ud]/[+d], Spec-head Agree, parasitic adjunction) would live in Theories/Syntax/Minimalist/ANDL.lean (planned; not yet present). The semantic analysis (negative attitude, conventional implicature, possible-ignorance presupposition) lives in Theories/Pragmatics/Expressives/ (currently Basic.lean + OutlookMarker.lean) and Theories/Interfaces/SyntaxSemantics/LeftPeriphery.lean. Fragment lexemes import only this file.

inductive Typology.ExpressiveModifier.ANDLMovementType : Type

How an ANDL modifier reaches its scope-taking position.

• parasitic: must adjoin to the wh-phrase; rides along with wh-movement; cannot move on its own. English/Singlish the-hell (@cite{merchant-2002}, @cite{chan-shen-2026}).
• independent: can undergo movement on its own (typically covert) to the scope position. Mandarin daodi (@cite{chou-2012}).

This is the single typological parameter @cite{chan-shen-2026} isolate as distinguishing English/Singlish the-hell from Mandarin daodi.

• parasitic : ANDLMovementType

  Modifier must adjoin to wh-host; moves only as a passenger.

• independent : ANDLMovementType

  Modifier moves on its own to the scope position.

@[implicit_reducible]

instance Typology.ExpressiveModifier.instDecidableEqANDLMovementType : DecidableEq ANDLMovementType

Equations

• Typology.ExpressiveModifier.instDecidableEqANDLMovementType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.ExpressiveModifier.instReprANDLMovementType.repr : ANDLMovementType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.ExpressiveModifier.instReprANDLMovementType : Repr ANDLMovementType

Equations

• Typology.ExpressiveModifier.instReprANDLMovementType = { reprPrec := Typology.ExpressiveModifier.instReprANDLMovementType.repr }

inductive Typology.ExpressiveModifier.ANDLHostPosition : Type

Where an ANDL modifier scopes — its required host position at the end of the derivation. For all currently-attested cases this is matrix scope; the abstraction leaves room for future findings of e.g. embedded-scope ANDLs.

• matrixScope : ANDLHostPosition

  Modifier must reach matrix scope (English, Mandarin, Singlish).

• embeddedScopeOk : ANDLHostPosition

  Modifier permits embedded scope. (Currently unattested; placeholder.)

@[implicit_reducible]

instance Typology.ExpressiveModifier.instDecidableEqANDLHostPosition : DecidableEq ANDLHostPosition

Equations

• Typology.ExpressiveModifier.instDecidableEqANDLHostPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.ExpressiveModifier.instReprANDLHostPosition.repr : ANDLHostPosition → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.ExpressiveModifier.instReprANDLHostPosition : Repr ANDLHostPosition

Equations

• Typology.ExpressiveModifier.instReprANDLHostPosition = { reprPrec := Typology.ExpressiveModifier.instReprANDLHostPosition.repr }

structure Typology.ExpressiveModifier.ExpressiveWhModifier : Type

A theory-neutral lexical entry for an ANDL (aggressively non-D-linked) wh-modifier. Carries phonological form, gloss, and the typological parameters that determine licensing.

Theory-specific analyses (POV features, conventional implicature, perspectival semantics) attach as separate predicates in Theories/.

• form : String

  Written form.

• gloss : String

  Gloss (English description).

• movementType : ANDLMovementType

  Whether the modifier moves parasitically on the wh-phrase or independently.

• hostPosition : ANDLHostPosition

  Required scope position.

def Typology.ExpressiveModifier.instReprExpressiveWhModifier.repr : ExpressiveWhModifier → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.ExpressiveModifier.instReprExpressiveWhModifier : Repr ExpressiveWhModifier

Equations

• Typology.ExpressiveModifier.instReprExpressiveWhModifier = { reprPrec := Typology.ExpressiveModifier.instReprExpressiveWhModifier.repr }

@[implicit_reducible]

instance Typology.ExpressiveModifier.instDecidableEqExpressiveWhModifier : DecidableEq ExpressiveWhModifier

Equations

• Typology.ExpressiveModifier.instDecidableEqExpressiveWhModifier = Typology.ExpressiveModifier.instDecidableEqExpressiveWhModifier.decEq

def Typology.ExpressiveModifier.instDecidableEqExpressiveWhModifier.decEq (x✝ x✝¹ : ExpressiveWhModifier) : Decidable (x✝ = x✝¹)

Equations

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

def Typology.ExpressiveModifier.Licensed (m : ExpressiveWhModifier) (whHostReachesScope : Prop) : Prop

Theory-neutral licensing: an ANDL modifier with required scope at matrix is licensed iff some element (the modifier itself, or its wh-host) reaches the scope position.

Parameters:

• m — the ANDL lexeme
• whHostReachesScope — does the wh-phrase reach matrix scope under the strategy in question? (e.g., WhInterpMechanism.ReachesSpecCP)

The predicate is the disjunction: licensed iff host reaches scope OR (modifier moves independently to matrix scope on its own). Specific theories instantiate whHostReachesScope with their own structural primitives.

Equations

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

@[implicit_reducible]

instance Typology.ExpressiveModifier.instDecidableLicensed (m : ExpressiveWhModifier) (P : Prop) [Decidable P] : Decidable (Licensed m P)

Equations

• Typology.ExpressiveModifier.instDecidableLicensed m P = id inferInstance

theorem Typology.ExpressiveModifier.parasitic_licensed_iff_host_reaches {m : ExpressiveWhModifier} (h : m.movementType = ANDLMovementType.parasitic) (P : Prop) : Licensed m P ↔ P

For a parasitic modifier (the-hell-type), licensing reduces to the wh-host reaching scope.

theorem Typology.ExpressiveModifier.independent_matrix_always_licensed {m : ExpressiveWhModifier} (hMov : m.movementType = ANDLMovementType.independent) (hHost : m.hostPosition = ANDLHostPosition.matrixScope) (P : Prop) : Licensed m P

For an independent modifier (daodi-type) with matrix scope, licensing holds regardless of whether the host reaches scope.