Lechner 2004: Ellipsis in Comparatives

@cite{lechner-2004} @cite{lechner-2001} @cite{bresnan-1973} @cite{kennedy-1999} @cite{merchant-2001}

Winfried Lechner. Ellipsis in Comparatives. Studies in Generative Grammar 72. Berlin/New York: Mouton de Gruyter.

What this file is

The canonical home of the binding diagnostic for phrasal comparatives. Lechner Ch 2 §2.1 ("Disjoint reference effects") establishes that the comparative-deletion site is reconstructed at LF and is therefore visible to Principle C. Lechner's diagnostic is the source of @cite{bhatt-takahashi-2011}'s English binding battery; B&T fn. 4 explicitly says their (11)–(13) are modelled on this work.

This file owns the diagnostic schema (BindingDatum), the two analyses' structural predictions (RAPredictsCoref / DAPredictsCoref), and the language-level realised-availability predicates (realizesReduction / realizesDirect). Downstream study files (BhattTakahashi2011.lean and any future cross-linguistic work) import these and instantiate them on per-paper data.

Lechner's argument (Ch 2 §2.1)

Lechner contrasts two predictions about the CD-site's syntactic reality:

• CD-site is reconstructed at LF (Lechner's view): material inside the CD-site is visible to Principle C. R-expressions inside the CD-site induce disjoint-reference effects.
• CD-site is recovered only in semantics (Kennedy 1999, Lerner & Pinkal): syntactic principles are blind to the CD-site's content.

Lechner's key data points (numbers from Lechner 2004):

• (24) *Mary is prouder of John_i than he_i is. — CD-site is d-proud of John_i. Coreferential reading is unavailable. Under reconstruction this is a Principle C violation; under the semantic view there is no syntactic basis for the deviance.
• (25) Mary is prouder of John_i than he_i believes that I am. — same R-expression-in-CD-site configuration, but coref is licit. Lechner attributes the obviation to Vehicle Change (Fiengo & May 1994) once the CD-site is embedded under a clause boundary.
• (28a/b) John_i is taller than himself_i. (✓) vs. *John_i is taller than him_i. (✗) — phrasal pattern: a c-commanding NP can bind a reflexive remnant but cannot coindex with a pronominal remnant. Together these establish that the matrix subject c-commands into the than-XP at the relevant level.

The schema below abstracts the (24)-style minimal pair into two binary dimensions: whether matrix material c-commands the comparative associate, and whether coreference between that matrix material and an R-expression inside the standard is attested. The (25)-style embedding obviation requires a third dimension (depth of embedding) which is not formalised here; see the closing prose for what would be needed to capture it.

Why this file is not in Theories/

The diagnostic is paper-faithful to Lechner: it instantiates an empirical-data schema and proves which structural analyses are consistent with which language's data. The structural primitives — c-command, the CD-site, Vehicle Change — live in the relevant syntax/ellipsis modules. This file is the empirical bridge between those primitives and downstream study files that consume the schema.

inductive Lechner2004.PhrasalAnalysis : Type

The two competing structural analyses of phrasal comparatives. Lechner Ch 2 §1 introduces both (under different labels) and @cite{bhatt-takahashi-2011} adopts these names.

• Reduction Analysis (RA): phrasal than NP derives from clausal than [NP is Adj] via reduction (gapping, conjunction reduction, TP-ellipsis). The standard sits in a clause-internal position parallel to the matrix associate.
• Direct Analysis (DA): phrasal than NP is genuinely phrasal; the 'than'-PP is external and the standard is its complement.

• reduction : PhrasalAnalysis
• direct : PhrasalAnalysis

@[implicit_reducible]

instance Lechner2004.instDecidableEqPhrasalAnalysis : DecidableEq PhrasalAnalysis

Equations

• Lechner2004.instDecidableEqPhrasalAnalysis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Lechner2004.instReprPhrasalAnalysis : Repr PhrasalAnalysis

Equations

• Lechner2004.instReprPhrasalAnalysis = { reprPrec := Lechner2004.instReprPhrasalAnalysis.repr }

def Lechner2004.instReprPhrasalAnalysis.repr : PhrasalAnalysis → Nat → Std.Format

Equations

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

structure Lechner2004.BindingDatum : Type

A minimal-pair binding datum as used in Lechner's disjoint- reference diagnostic. Two binary dimensions:

• pronCCommandsAssociate — whether some matrix expression c-commands the comparative associate at the relevant level (LF for RA's reconstructed structure; surface for DA's external 'than'-PP).
• corefAttested — whether coreference between that matrix expression and an R-expression inside the standard is reported as grammatical.

citationId records the example number (e.g. "24" for Lechner (24)) so that the relationship between the abstract schema and the concrete paper data is auditable. acceptability records fine-grained judgments where binary corefAttested is too coarse — e.g. for the @cite{bhatt-takahashi-2011} (13b) "(?)mildly deviant" case.

• citationId : String
• acceptability : Features.Acceptability
• pronCCommandsAssociate : Bool
• corefAttested : Bool

def Lechner2004.instDecidableEqBindingDatum.decEq (x✝ x✝¹ : BindingDatum) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Lechner2004.instDecidableEqBindingDatum : DecidableEq BindingDatum

Equations

• Lechner2004.instDecidableEqBindingDatum = Lechner2004.instDecidableEqBindingDatum.decEq

@[implicit_reducible]

instance Lechner2004.instReprBindingDatum : Repr BindingDatum

Equations

• Lechner2004.instReprBindingDatum = { reprPrec := Lechner2004.instReprBindingDatum.repr }

def Lechner2004.instReprBindingDatum.repr : BindingDatum → Nat → Std.Format

Equations

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

def Lechner2004.RAPredictsCoref (d : BindingDatum) : Prop

The Reduction Analysis's structural prediction. The standard occupies a clause-internal position parallel to the associate; matrix material c-commanding the associate also c-commands the standard's R-expression. Coreference is therefore grammatical iff the matrix expression does not c-command the associate.

Equations

• Lechner2004.RAPredictsCoref d = (d.pronCCommandsAssociate = false ↔ d.corefAttested = true)

@[implicit_reducible]

instance Lechner2004.instDecidableRAPredictsCoref (d : BindingDatum) : Decidable (RAPredictsCoref d)

Equations

• Lechner2004.instDecidableRAPredictsCoref d = id inferInstance

def Lechner2004.DAPredictsCoref (d : BindingDatum) : Prop

The Direct Analysis's structural prediction. The 'than'-PP is external and the matrix expression never c-commands into it, regardless of its relation to the associate. Coreference is therefore predicted to be uniformly available.

Equations

• Lechner2004.DAPredictsCoref d = (d.corefAttested = true)

@[implicit_reducible]

instance Lechner2004.instDecidableDAPredictsCoref (d : BindingDatum) : Decidable (DAPredictsCoref d)

Equations

• Lechner2004.instDecidableDAPredictsCoref d = id inferInstance

def Lechner2004.realizesReduction (data : List BindingDatum) : Prop

A language realises the Reduction Analysis (per its binding diagnostic) iff every datum matches RA's biconditional prediction (coref is attested iff the matrix expression does not c-command the associate).

Equations

• Lechner2004.realizesReduction data = ∀ (d : Lechner2004.BindingDatum), d ∈ data → Lechner2004.RAPredictsCoref d

@[implicit_reducible]

instance Lechner2004.instDecidableRealizesReduction (data : List BindingDatum) : Decidable (realizesReduction data)

Equations

• Lechner2004.instDecidableRealizesReduction data = id (List.decidableBAll Lechner2004.RAPredictsCoref data)

def Lechner2004.realizesDirect (data : List BindingDatum) : Prop

A language realises the Direct Analysis (per its binding diagnostic) iff every datum exhibits coreference — DA imposes no structural constraint, so it is consistent with the data exactly when coreference is uniformly attested.

Equations

• Lechner2004.realizesDirect data = ∀ (d : Lechner2004.BindingDatum), d ∈ data → Lechner2004.DAPredictsCoref d

@[implicit_reducible]

instance Lechner2004.instDecidableRealizesDirect (data : List BindingDatum) : Decidable (realizesDirect data)

Equations

• Lechner2004.instDecidableRealizesDirect data = id (List.decidableBAll Lechner2004.DAPredictsCoref data)

structure Lechner2004.HeadAvailability : Type

Per-language record of which analyses are realised by the binding diagnostic. Constructed via headAvailabilityFromBinding from the language's binding data, not stipulated.

• reductionRealized : Bool
• directRealized : Bool

def Lechner2004.instDecidableEqHeadAvailability.decEq (x✝ x✝¹ : HeadAvailability) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Lechner2004.instDecidableEqHeadAvailability : DecidableEq HeadAvailability

Equations

• Lechner2004.instDecidableEqHeadAvailability = Lechner2004.instDecidableEqHeadAvailability.decEq

def Lechner2004.instReprHeadAvailability.repr : HeadAvailability → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Lechner2004.instReprHeadAvailability : Repr HeadAvailability

Equations

• Lechner2004.instReprHeadAvailability = { reprPrec := Lechner2004.instReprHeadAvailability.repr }

def Lechner2004.headAvailabilityFromBinding (data : List BindingDatum) : HeadAvailability

Build a HeadAvailability from binding data by checking consistency against each analysis's structural prediction. This is the anti-stipulation core: per-language head-availability is derived from the data, not asserted. The Bool fields are decide-extracted from the decidable propositions realizesReduction / realizesDirect.

Equations

• Lechner2004.headAvailabilityFromBinding data = { reductionRealized := decide (Lechner2004.realizesReduction data), directRealized := decide (Lechner2004.realizesDirect data) }

def Lechner2004.lechner_24 : BindingDatum

Lechner (24): *Mary is prouder of John_i than he_i is. The matrix pronoun he c-commands the (matrix) associate John; coreference into the CD-site d-proud of John_i is unavailable. Under reconstruction, this is a Principle C violation.

Equations

• Lechner2004.lechner_24 = { citationId := "24", acceptability := Features.Acceptability.unacceptable, pronCCommandsAssociate := true, corefAttested := false }

def Lechner2004.lechner_28a : BindingDatum

Lechner (28a): John_i is taller than himself_i. Phrasal comparative; the matrix subject c-commands into the than-XP and binds the reflexive remnant. Recorded with corefAttested := true because the binding relation is grammatical (reflexive licensing is the dual of disjoint reference for our schema's purposes — binding/coref attested means the c-command relation is real).

Equations

• Lechner2004.lechner_28a = { citationId := "28a", acceptability := Features.Acceptability.ok, pronCCommandsAssociate := false, corefAttested := true }

def Lechner2004.englishLechnerData : List BindingDatum

Lechner's English binding data: the minimal pair from (24) establishing reconstruction-into-CD-site, paired with the (28a) no-c-command control.

Equations

• Lechner2004.englishLechnerData = [Lechner2004.lechner_24, Lechner2004.lechner_28a]

theorem Lechner2004.english_lechner_realizes_reduction : realizesReduction englishLechnerData

Lechner's English data is consistent with RA: the disjoint- reference effect at (24) follows iff the CD-site is reconstructed (RA-style), and (28a)'s no-c-command control permits coref as RA predicts.

theorem Lechner2004.english_lechner_rules_out_direct : ¬realizesDirect englishLechnerData

Lechner's English data is not consistent with DA: DA predicts uniform coref availability, contradicted by (24).