Expressive wh-modifiers: ANDL typology

[Pes87] [Cho12] [Mer02] [HN08] [JA20] [CS26]

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; [HN08], [JA20]); daodi 到底 (Mandarin; [Cho12]); ittai (Japanese); ttaeyche (Korean); zum-Teufel (German); etc.

The shared empirical generalization ([Pes87]): 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 [CS26] 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 Syntax/Minimalist/ANDL.lean (planned; not yet present). The semantic analysis (negative attitude, conventional implicature, possible-ignorance presupposition) lives in Pragmatics/Expressives/ (currently Basic.lean + OutlookMarker.lean) and Syntax/Minimalist/LeftPeriphery.lean. Fragment lexemes import only this file.

inductive 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 ([Mer02], [CS26]).
• independent: can undergo movement on its own (typically covert) to the scope position. Mandarin daodi ([Cho12]).

This is the single typological parameter [CS26] 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 ExpressiveModifier.instDecidableEqANDLMovementType : DecidableEq ANDLMovementType

Equations

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

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

Equations

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

@[implicit_reducible]

instance ExpressiveModifier.instReprANDLMovementType : Repr ANDLMovementType

Equations

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

inductive 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 ExpressiveModifier.instDecidableEqANDLHostPosition : DecidableEq ANDLHostPosition

Equations

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

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

Equations

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

@[implicit_reducible]

instance ExpressiveModifier.instReprANDLHostPosition : Repr ANDLHostPosition

Equations

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

structure 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.

@[implicit_reducible]

instance ExpressiveModifier.instReprExpressiveWhModifier : Repr ExpressiveWhModifier

Equations

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

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance ExpressiveModifier.instDecidableEqExpressiveWhModifier : DecidableEq ExpressiveWhModifier

Equations

• ExpressiveModifier.instDecidableEqExpressiveWhModifier = ExpressiveModifier.instDecidableEqExpressiveWhModifier.decEq

def 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 ExpressiveModifier.instDecidableLicensed (m : ExpressiveWhModifier) (P : Prop) [Decidable P] : Decidable (Licensed m P)

Equations

• ExpressiveModifier.instDecidableLicensed m P = id inferInstance

theorem 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 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.