Bresnan 1973: Syntax of the Comparative Clause Construction in English

[Bre73] [BP04] [BT11]

Joan W. Bresnan. Syntax of the Comparative Clause Construction in English. Linguistic Inquiry 4(3): 275–343.

Core Contributions

1. QP structure: Every comparative has an underlying QP (Det + Q) where the Q items are much, many, little, few, enough, and the Det position hosts -er, -est, as, too, so, that, or ∅. The surface form more derives from -er + much via suppletion.

2. Morphological derivation: Three ordered rules derive surface forms:

   • -er Encliticizing: Det -er cliticizes onto Q (-er Q → Q-er)
   • Much Deletion: much → ∅ before adjectives/adverbs
   • Suppletion: much-er → more, little-er → less, etc.

3. Comparative Deletion: The than/as clause originates in the Det of QP. An obligatory deletion operation removes a clause constituent "nondistinct" from the head. The clause is then extraposed.

4. All than-clauses are underlyingly clausal: "Phrasal" comparatives like taller than Bill derive from full clauses via maximal deletion. [BP04] reject this view, arguing phrasal comparatives are genuinely phrasal (DA). [BT11] reverses B&P on the basis of Lechner-style binding diagnostics and re-vindicates Bresnan's clausal-source analysis for English (the 3-place '-er' is needed for Hindi-Urdu, not English). See BhattTakahashi2011.bt2011_agrees_with_bresnan_against_bp2004 for the cross-tradition bridge.

5. Subdeletion: When the head is a QP (measure phrase), only a matching QP is deleted from the clause — not an AP or NP. This explains *more than Bill tall (NP ≠ QP identity failure).

6. Privative adjective constraint: *more than five feet short because short rejects definite measure phrases, so the QP identity condition in the clause cannot be satisfied.

What Is Current vs. Historical

Current consensus: The data paradigms, the degree-head inventory (Det → modern Deg°), the more = -er + much decomposition, the measure phrase restriction with negative adjectives, subdeletion commensurability.

Modified but descended: QP → DegP ([Ken99]); comparative deletion → degree operator movement ([Hei01]); QP-AP parallelism → X-bar theory → Minimalist bare phrase structure.

Historical: The construction-specific transformations (AP Shift, QP Raising, Much Deletion, -er Encliticizing), the "all comparatives are clausal" claim, the so → such transformation.

Connection to Kennedy 1999

This file formalizes Bresnan's own proposals: the QP structure, the derivation rules, and the four introductory puzzles that motivated the analysis. Bridge theorems connect the QP inventory to Head and verify suppletion outputs against Fragment formComp entries.

inductive Bresnan1973.ThanClauseType : Type

The two syntactic forms of than-clauses: phrasal "than Bill" vs clausal "than Bill is tall".

• phrasal : ThanClauseType
• clausal : ThanClauseType

@[instance_reducible]

instance Bresnan1973.instDecidableEqThanClauseType : DecidableEq ThanClauseType

Equations

• Bresnan1973.instDecidableEqThanClauseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Bresnan1973.instReprThanClauseType : Repr ThanClauseType

Equations

• Bresnan1973.instReprThanClauseType = { reprPrec := Bresnan1973.instReprThanClauseType.repr }

def Bresnan1973.instReprThanClauseType.repr : ThanClauseType → ℕ → Std.Format

Equations

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

QP Structure (Det + Q)

inductive Bresnan1973.Det : Type

The Det position of the QP: hosts degree/comparison morphemes. This is Bresnan's precursor to the modern Deg° head.

• er : Det
• est : Det
• as_ : Det
• too : Det
• so : Det
• that_ : Det
• any_ : Det
• no_ : Det
• null : Det

@[instance_reducible]

instance Bresnan1973.instDecidableEqDet : DecidableEq Det

Equations

• Bresnan1973.instDecidableEqDet x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bresnan1973.instReprDet.repr : Det → ℕ → Std.Format

Equations

• Bresnan1973.instReprDet.repr Bresnan1973.Det.er prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Det.er")).group prec✝
• Bresnan1973.instReprDet.repr Bresnan1973.Det.est prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Det.est")).group prec✝
• Bresnan1973.instReprDet.repr Bresnan1973.Det.as_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Det.as_")).group prec✝
• Bresnan1973.instReprDet.repr Bresnan1973.Det.too prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Det.too")).group prec✝
• Bresnan1973.instReprDet.repr Bresnan1973.Det.so prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Det.so")).group prec✝
• Bresnan1973.instReprDet.repr Bresnan1973.Det.that_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Det.that_")).group prec✝
• Bresnan1973.instReprDet.repr Bresnan1973.Det.any_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Det.any_")).group prec✝
• Bresnan1973.instReprDet.repr Bresnan1973.Det.no_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Det.no_")).group prec✝
• Bresnan1973.instReprDet.repr Bresnan1973.Det.null prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Det.null")).group prec✝

@[instance_reducible]

instance Bresnan1973.instReprDet : Repr Det

Equations

• Bresnan1973.instReprDet = { reprPrec := Bresnan1973.instReprDet.repr }

inductive Bresnan1973.Q : Type

The Q (quantity) head: much, many, little, few, enough. Bresnan's central claim: these are the deep-structure elements underlying all comparative morphology.

• much : Q
• many : Q
• little : Q
• few : Q
• enough : Q

@[instance_reducible]

instance Bresnan1973.instDecidableEqQ : DecidableEq Q

Equations

• Bresnan1973.instDecidableEqQ x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bresnan1973.instReprQ.repr : Q → ℕ → Std.Format

Equations

• Bresnan1973.instReprQ.repr Bresnan1973.Q.much prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Q.much")).group prec✝
• Bresnan1973.instReprQ.repr Bresnan1973.Q.many prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Q.many")).group prec✝
• Bresnan1973.instReprQ.repr Bresnan1973.Q.little prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Q.little")).group prec✝
• Bresnan1973.instReprQ.repr Bresnan1973.Q.few prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Q.few")).group prec✝
• Bresnan1973.instReprQ.repr Bresnan1973.Q.enough prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Q.enough")).group prec✝

@[instance_reducible]

instance Bresnan1973.instReprQ : Repr Q

Equations

• Bresnan1973.instReprQ = { reprPrec := Bresnan1973.instReprQ.repr }

structure Bresnan1973.QP : Type

The QP: Bresnan's degree phrase structure.

• det : Det
• q : Q

@[instance_reducible]

instance Bresnan1973.instDecidableEqQP : DecidableEq QP

Equations

• Bresnan1973.instDecidableEqQP = Bresnan1973.instDecidableEqQP.decEq

def Bresnan1973.instDecidableEqQP.decEq (x✝ x✝¹ : QP) : Decidable (x✝ = x✝¹)

Equations

• Bresnan1973.instDecidableEqQP.decEq { det := a, q := a_1 } { det := b, q := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Bresnan1973.instReprQP : Repr QP

Equations

• Bresnan1973.instReprQP = { reprPrec := Bresnan1973.instReprQP.repr }

def Bresnan1973.instReprQP.repr : QP → ℕ → Std.Format

Equations

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

Bridge: QP → Head

def Bresnan1973.Det.toHead : Det → Degree.Head

Map Bresnan's QP Det to the modern DegP type classification. The Det determines the comparison type; Q determines mass/count.

Equations

• Bresnan1973.Det.er.toHead = Degree.Head.comparative
• Bresnan1973.Det.est.toHead = Degree.Head.superlative
• Bresnan1973.Det.as_.toHead = Degree.Head.equative
• Bresnan1973.Det.too.toHead = Degree.Head.excessive
• Bresnan1973.Det.null.toHead = Degree.Head.sufficiency
• Bresnan1973.Det.so.toHead = Degree.Head.excessive
• Bresnan1973.Det.that_.toHead = Degree.Head.excessive
• Bresnan1973.Det.any_.toHead = Degree.Head.comparative
• Bresnan1973.Det.no_.toHead = Degree.Head.comparative

theorem Bresnan1973.head_comparative_from_er : Det.er.toHead = Degree.Head.comparative

The modern Head inventory is recoverable from Bresnan's Det.

theorem Bresnan1973.head_equative_from_as : Det.as_.toHead = Degree.Head.equative

theorem Bresnan1973.head_superlative_from_est : Det.est.toHead = Degree.Head.superlative

theorem Bresnan1973.head_excessive_from_too : Det.too.toHead = Degree.Head.excessive

Morphological Derivation

def Bresnan1973.suppletion : QP → Option String

Suppletion: the surface form resulting from -er/-est Encliticizing onto Q. Returns none for regular (non-suppletive) combinations.

Rule (7): -er much → more, -er many → more, -er little → less Rule (223): -est much → most, -est many → most, etc.

Equations

• Bresnan1973.suppletion { det := Bresnan1973.Det.er, q := Bresnan1973.Q.much } = some "more"
• Bresnan1973.suppletion { det := Bresnan1973.Det.er, q := Bresnan1973.Q.many } = some "more"
• Bresnan1973.suppletion { det := Bresnan1973.Det.er, q := Bresnan1973.Q.little } = some "less"
• Bresnan1973.suppletion { det := Bresnan1973.Det.er, q := Bresnan1973.Q.few } = some "fewer"
• Bresnan1973.suppletion { det := Bresnan1973.Det.est, q := Bresnan1973.Q.much } = some "most"
• Bresnan1973.suppletion { det := Bresnan1973.Det.est, q := Bresnan1973.Q.many } = some "most"
• Bresnan1973.suppletion { det := Bresnan1973.Det.est, q := Bresnan1973.Q.little } = some "least"
• Bresnan1973.suppletion { det := Bresnan1973.Det.est, q := Bresnan1973.Q.few } = some "fewest"
• Bresnan1973.suppletion x✝ = none

theorem Bresnan1973.more_from_er_much : suppletion { det := Det.er, q := Q.much } = some "more"

more derives from -er + much (or -er + many).

theorem Bresnan1973.more_from_er_many : suppletion { det := Det.er, q := Q.many } = some "more"

theorem Bresnan1973.less_from_er_little : suppletion { det := Det.er, q := Q.little } = some "less"

theorem Bresnan1973.most_from_est_much : suppletion { det := Det.est, q := Q.much } = some "most"

most derives from -est + much.

def Bresnan1973.Q.selectsMass : Q → Bool

Q selects mass vs count nouns. much selects mass nouns and can also modify adjectives/adverbs (after Much Deletion). many selects count nouns only. This predicts *much people, *many bread.

Equations

• Bresnan1973.Q.much.selectsMass = true
• Bresnan1973.Q.little.selectsMass = true
• Bresnan1973.Q.enough.selectsMass = true
• x✝.selectsMass = false

def Bresnan1973.Q.selectsCount : Q → Bool

Equations

• Bresnan1973.Q.many.selectsCount = true
• Bresnan1973.Q.few.selectsCount = true
• Bresnan1973.Q.enough.selectsCount = true
• x✝.selectsCount = false

def Bresnan1973.Q.canModifyAdjective : Q → Bool

much and little (but not many and few) can modify adjectives and adverbs — they are the Qs that undergo Much Deletion.

This predicts: as much tall → as tall (Much Deletion), but *as many tall (no deletion rule for many before A).

Equations

• Bresnan1973.Q.much.canModifyAdjective = true
• Bresnan1973.Q.little.canModifyAdjective = true
• Bresnan1973.Q.enough.canModifyAdjective = true
• x✝.canModifyAdjective = false

def Bresnan1973.muchDeletionApplies (q : Q) (adjFollows : Bool) : Bool

Much Deletion: much → ∅ / [... ___ A]_AP. Applies only to Qs that can modify adjectives, and only when an adjective or adverb immediately follows.

Equations

• Bresnan1973.muchDeletionApplies q adjFollows = (q.canModifyAdjective && adjFollows)

Introductory Puzzles (A)–(D)

structure Bresnan1973.PuzzleDatum : Type

An acceptability judgment with structural explanation.

• sentence : String
• acceptable : Bool
• head : String

  What is the head of the comparative construction?

• deletedConstituent : String

  What is deleted from the than-clause?

• explanation : String

  Why is the identity condition satisfied or not?

def Bresnan1973.instReprPuzzleDatum.repr : PuzzleDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bresnan1973.instReprPuzzleDatum : Repr PuzzleDatum

Equations

• Bresnan1973.instReprPuzzleDatum = { reprPrec := Bresnan1973.instReprPuzzleDatum.repr }

def Bresnan1973.puzzleA : List PuzzleDatum

Puzzle (A): "I've never seen a man taller than my father/mother."

(i) and (ii) are roughly synonymous; (iii) and (iv) are not. (i) "a man taller than my father" — head: AP [x much tall] (ii) "a taller man than my father" — head: AP [x much tall] (iii) "a man taller than my mother" — head: AP [x much tall] (iv) "a taller man than my mother" — head: NP [a man x much tall]

In (iv), the head is the entire predicative NP. The deleted constituent in the clause must match this NP — but "my mother is [x much tall] a man" implies my mother is a man. Hence the anomaly.

Equations

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

def Bresnan1973.puzzleB : List PuzzleDatum

Puzzle (B): "Jack eats caviar more than he eats mush / sleeps."

(a,c) are grammatical; (d) is not. The deleted constituent is an adverbial QP modifier of the VP.

In (d), *Jack eats more caviar than he sleeps is bad because more is a partitive QP embedded in the direct object NP. The matching partitive QP in the clause requires an NP — but sleep is intransitive, so no matching partitive is available.

Equations

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

def Bresnan1973.puzzleC : List PuzzleDatum

Puzzle (C): "I am more angry today than I was yesterday / than sad."

The acceptability of angrier (synthetic) vs more angry (analytic) follows from what is deleted and what survives. When the comparison is across adjectives (angry vs sad), the comparative must be more angry (analytic) because more is a sentence modifier, not within the AP. Simple comparative formation (producing angrier) cannot apply because more and sad are not within the same AP.

Equations

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

def Bresnan1973.puzzleD : List PuzzleDatum

Puzzle (D): "*Mary is more than five feet short" vs "Mary is shorter than five feet."

[Ken99] explains this via positive/negative extent boundedness. Bresnan's syntactic explanation: short rejects definite measure phrase modifiers (*How short is he? — five feet short), so the QP identity condition in the clause cannot be satisfied.

Bridge: this connects to Kennedy1999.measurePhraseAbsoluteRows and AdmitsMeasurePhrase in MeasurePhrase.lean.

Equations

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

Comparative Deletion (Identity Condition)

inductive Bresnan1973.DeletionTarget : Type

The syntactic category of the constituent deleted from the than-clause. Bresnan's key insight: the deleted element must be "nondistinct" (same syntactic category) from the head.

This is the 1973 precursor to modern identity conditions in ellipsis (e-GIVENness in [Mer01]; SIC in Anand, Hardt & McCloskey 2021).

• qp : DeletionTarget
• ap : DeletionTarget
• np : DeletionTarget

@[instance_reducible]

instance Bresnan1973.instDecidableEqDeletionTarget : DecidableEq DeletionTarget

Equations

• Bresnan1973.instDecidableEqDeletionTarget x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bresnan1973.instReprDeletionTarget.repr : DeletionTarget → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bresnan1973.instReprDeletionTarget : Repr DeletionTarget

Equations

• Bresnan1973.instReprDeletionTarget = { reprPrec := Bresnan1973.instReprDeletionTarget.repr }

def Bresnan1973.identityHolds (head clause : DeletionTarget) : Bool

The identity condition: deletion succeeds only when the clause constituent and the head have the same syntactic category.

"Nondistinctness" in Bresnan's terms — the deleted constituent must be featurally nondistinct from the head.

Equations

• Bresnan1973.identityHolds head clause = (head == clause)

theorem Bresnan1973.subdeletion_identity_holds : identityHolds DeletionTarget.ap DeletionTarget.ap = true

Subdeletion: "The table is longer than the door is wide."

Head = AP (-er much long), deleted = AP (x much wide). Both are APs, so identity holds. The dimensions (length vs width) need not match — only the syntactic category.

This connects to subcomparativeExamples in Kennedy1999.lean and subcomparative in Intervals.lean.

theorem Bresnan1973.np_qp_identity_fails : identityHolds DeletionTarget.qp DeletionTarget.np = false

*John is more than Bill tall fails: head = QP (-er much), but the matching constituent in the clause is an NP (Bill = that much). NP ≠ QP, so the identity condition fails.

All Than-Clauses Are Underlyingly Clausal

inductive Bresnan1973.BresnanThanClauseAnalysis : Type

Bresnan's strongest syntactic claim: ALL comparatives are underlyingly clausal. What appears as a "phrasal" comparative ("taller than Bill") is derived from a full clause by maximal deletion.

[BP04] rejected this view in favor of a "genuinely phrasal" Direct Analysis. [BT11] subsequently reversed B&P on the basis of binding diagnostics and re-vindicates Bresnan's clausal-source analysis for English (cross-tradition bridge: BhattTakahashi2011.bt2011_agrees_with_bresnan_against_bp2004). Both analyses yield the same truth conditions for simple comparatives (proved in ThanClause.phrasal_clausal_equivalence), so the disagreement is purely syntactic.

• partialDeletion : BresnanThanClauseAnalysis

  Full clause with partial deletion: "than Bill is [x much tall]" → "than Bill is" (deletion of AP)

• maximalDeletion : BresnanThanClauseAnalysis

  Full clause with maximal deletion: "than Bill is [x much tall]" → "than Bill" (deletion of AP + copula stranding)

@[instance_reducible]

instance Bresnan1973.instDecidableEqBresnanThanClauseAnalysis : DecidableEq BresnanThanClauseAnalysis

Equations

• Bresnan1973.instDecidableEqBresnanThanClauseAnalysis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Bresnan1973.instReprBresnanThanClauseAnalysis.repr : BresnanThanClauseAnalysis → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bresnan1973.instReprBresnanThanClauseAnalysis : Repr BresnanThanClauseAnalysis

Equations

• Bresnan1973.instReprBresnanThanClauseAnalysis = { reprPrec := Bresnan1973.instReprBresnanThanClauseAnalysis.repr }

def Bresnan1973.bresnanAnalysisOf : ThanClauseType → BresnanThanClauseAnalysis

Under Bresnan's analysis, the modern phrasal type is just maximalDeletion of an underlying clause.

Equations

• Bresnan1973.bresnanAnalysisOf Bresnan1973.ThanClauseType.clausal = Bresnan1973.BresnanThanClauseAnalysis.partialDeletion
• Bresnan1973.bresnanAnalysisOf Bresnan1973.ThanClauseType.phrasal = Bresnan1973.BresnanThanClauseAnalysis.maximalDeletion

Privative Adjective Measure Phrase Constraint

def Bresnan1973.admitsDefiniteMeasure (polarity : Core.Order.ScalePolarity) : Bool

Whether an adjective admits definite measure phrase modification ("five feet tall" ✓ vs "*five feet short" ✗).

Bresnan observes this as a syntactic fact; [Ken99] derives it from extent boundedness (positive extents are bounded, negative extents are not). Both predict the same distribution.

Equations

• Bresnan1973.admitsDefiniteMeasure Core.Order.ScalePolarity.positive = true
• Bresnan1973.admitsDefiniteMeasure Core.Order.ScalePolarity.negative = false

theorem Bresnan1973.positive_admits_measure : admitsDefiniteMeasure Core.Order.ScalePolarity.positive = true

Positive adjectives admit measure phrases.

theorem Bresnan1973.negative_rejects_measure : admitsDefiniteMeasure Core.Order.ScalePolarity.negative = false

Negative adjectives reject measure phrases.

structure Bresnan1973.MeasurePhraseConstraintDatum : Type

Bridge to Kennedy 1999: Bresnan's syntactic observation and Kennedy's semantic explanation make the same prediction for simple cases.

Bresnan: short syntactically rejects definite measure QPs, so the identity condition in comparative deletion cannot be satisfied.

Kennedy: negative extents are unbounded, so equating them with bounded measure phrases is semantically undefined.

The predictions diverge for less short than five feet (Bresnan predicts OK via little-based QP; Kennedy predicts OK via comparative semantics).

• adjective : String
• polarity : Core.Order.ScalePolarity
• measurePhraseOk : Bool
• comparativeMeasureOk : Bool

  "more than N units Adj" acceptable?

@[instance_reducible]

instance Bresnan1973.instReprMeasurePhraseConstraintDatum : Repr MeasurePhraseConstraintDatum

Equations

• Bresnan1973.instReprMeasurePhraseConstraintDatum = { reprPrec := Bresnan1973.instReprMeasurePhraseConstraintDatum.repr }

def Bresnan1973.instReprMeasurePhraseConstraintDatum.repr : MeasurePhraseConstraintDatum → ℕ → Std.Format

Equations

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

def Bresnan1973.measurePhraseConstraintData : List MeasurePhraseConstraintDatum

Equations

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

theorem Bresnan1973.measurePhrase_polarity_correlation (d : MeasurePhraseConstraintDatum) : d ∈ measurePhraseConstraintData → d.polarity = Core.Order.ScalePolarity.negative → d.measurePhraseOk = false

Among Bresnan's dimensional adjectives, measure phrase acceptability correlates with positive polarity.

This is the formal content behind puzzle (D) and connects to Kennedy1999.measurePhraseAbsoluteRows.

Det Inventory Paradigms

structure Bresnan1973.DetQParadigmEntry : Type

Bresnan's paradigms (4) and (5): the Det items form a closed class that combine with both much and little (mass) / many and few (count).

Paradigm (4): as/too/that/so/-er + much/little + mass noun Paradigm (5): as/too/that/so/-er + many/few + count noun

The last row in each paradigm undergoes suppletion: -er much → more, -er little → less, -er many → more, -er few → fewer.

• det : Det
• q : Q
• surfaceForm : String
• isSuppletive : Bool

  Does this undergo suppletion?

def Bresnan1973.instReprDetQParadigmEntry.repr : DetQParadigmEntry → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bresnan1973.instReprDetQParadigmEntry : Repr DetQParadigmEntry

Equations

• Bresnan1973.instReprDetQParadigmEntry = { reprPrec := Bresnan1973.instReprDetQParadigmEntry.repr }

def Bresnan1973.massParadigm : List DetQParadigmEntry

Equations

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

theorem Bresnan1973.massParadigm_suppletion_consistent (e : DetQParadigmEntry) : e ∈ massParadigm → e.isSuppletive = true → suppletion { det := e.det, q := e.q } = some e.surfaceForm

Verify: every suppletive entry in the paradigm matches the suppletion function.

def Bresnan1973.countParadigm : List DetQParadigmEntry

Equations

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

theorem Bresnan1973.countParadigm_suppletion_consistent (e : DetQParadigmEntry) : e ∈ countParadigm → e.isSuppletive = true → suppletion { det := e.det, q := e.q } = some e.surfaceForm

Verify: every suppletive entry in the count paradigm matches the suppletion function.

QP Well-Formedness

def Bresnan1973.QP.isWellFormed (qp : QP) : Bool

enough requires a null Det — *so enough, *too enough, *as enough, *enougher are all impossible (Bresnan p. 286).

This is formalized as a well-formedness predicate on QPs.

Equations

• qp.isWellFormed = match qp.q with | Bresnan1973.Q.enough => qp.det == Bresnan1973.Det.null | x => true

theorem Bresnan1973.enough_requires_null_det (d : Det) : d ≠ Det.null → { det := d, q := Q.enough }.isWellFormed = false

theorem Bresnan1973.enough_null_wellformed : { det := Det.null, q := Q.enough }.isWellFormed = true

QP-AP Parallelism

inductive Bresnan1973.BarCategory : Type

Bresnan's "archicategory" X̄ unifies QP and AP: both have left-recursive specifier + head structure.

QP → (QP) QP, QP → (Det) Q AP → (AP) AP, AP → (Adv) A

This is a direct precursor to X-bar theory (Jackendoff 1977) and ultimately to the Minimalist bare phrase structure. The modern counterpart is the shared structure of DegP and AdjP as functional and lexical projections in the extended AP.

Structural rule from Bresnan (145): X̄ → (X̄) X̄ (recursive expansion) X̄ → (Spec, X̄) X̄ (specifier + head)

• qp : BarCategory
• ap : BarCategory
• np : BarCategory

@[instance_reducible]

instance Bresnan1973.instDecidableEqBarCategory : DecidableEq BarCategory

Equations

• Bresnan1973.instDecidableEqBarCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Bresnan1973.instReprBarCategory : Repr BarCategory

Equations

• Bresnan1973.instReprBarCategory = { reprPrec := Bresnan1973.instReprBarCategory.repr }

def Bresnan1973.instReprBarCategory.repr : BarCategory → ℕ → Std.Format

Equations

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

Comparative Semantics Bridge

theorem Bresnan1973.simple_comparative_consensus {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ μ a > μ b

Bresnan's analysis is primarily syntactic, but the truth conditions it derives are compatible with the modern degree-semantic consensus.

For a simple adjectival comparative "A is taller than B":

• Bresnan: head = AP [-er much tall], clause deletes matching AP [x much tall]
• Kennedy: μ(A) > μ(B) where μ = height
• Heim: max({d | height(A) ≥ d}) > max({d | height(B) ≥ d})

All three yield the same truth conditions for simple cases.