Bresnan (1973): Syntax of the comparative clause construction in English

Every English comparative is built on a quantifier phrase, a Det of as, too, that, so, -er or -est over a Q drawn from much, many, little, few and enough, so that more is -er much or -er many and taller derives from [[much-er] tall] (Bresnan). Three ordered rules derive the head: -er Encliticizing moves the clitic onto Q and leaves the Det empty; Much Deletion then removes an unprotected much directly before the adjective of its AP, so as much tall becomes as tall while much-er tall survives to become taller; and QP Raising, on the empty Det alone, feeds AP Shift, a more reliable man beside too reliable a man and *a too reliable man. The clause is related to the head by Comparative Formation: every than and as phrase is a full clause from which a constituent nondistinct from the head, a QP, an AP or an NP, is deleted, the remainder positioned to the head's right. The four puzzles of the introduction turn on the identity of the head and of the deleted constituent: whether the clause predicates a man of the standard (A), whether the clause has a partitive to match a partitive head (B), whether the QP is AP-internal so that the synthetic form can arise (C), and whether the identity of a Q with a definite measure phrase is consistent with the privative adjective it modifies (D).

Implementation notes

Each row carries the paper's analysis of its example as features, the Det and Q of the QP and its position, or the head's category and site and the constituent the clause supplies; acceptability is derived from the rules. The anomaly of (242d) is read off the lexical gender of mother and man in the English fragment, privativeness off the polarity of short. QP recursion and QP Shift (1.4), so and such (1.5), of Insertion, Enough Permutation and the ambiguities of 1.8 beyond the homophony of more are not formalized.

References

• [Bre73]
• [Ros67]

The quantifier phrase (1.1–1.3)

inductive Bresnan1973.Particle : Type

The particles of the Det position (108), and the negative-dependent any and no that share it with -er (117)–(127).

• as_ : Particle
• too : Particle
• that_ : Particle
• so : Particle
• any_ : Particle
• no_ : Particle

@[instance_reducible]

instance Bresnan1973.instDecidableEqParticle : DecidableEq Particle

Equations

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

@[instance_reducible]

instance Bresnan1973.instReprParticle : Repr Particle

Equations

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

def Bresnan1973.instReprParticle.repr : Particle → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Bresnan1973.instReprParticle.repr Bresnan1973.Particle.as_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Particle.as_")).group prec✝
• Bresnan1973.instReprParticle.repr Bresnan1973.Particle.too prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Particle.too")).group prec✝
• Bresnan1973.instReprParticle.repr Bresnan1973.Particle.so prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Particle.so")).group prec✝
• Bresnan1973.instReprParticle.repr Bresnan1973.Particle.any_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Particle.any_")).group prec✝
• Bresnan1973.instReprParticle.repr Bresnan1973.Particle.no_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Particle.no_")).group prec✝

inductive Bresnan1973.Clitic : Type

The determiners that encliticize onto Q: -er by (20) and the indefinite superlative -est (223).

• er : Clitic
• est : Clitic

@[instance_reducible]

instance Bresnan1973.instDecidableEqClitic : DecidableEq Clitic

Equations

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

def Bresnan1973.instReprClitic.repr : Clitic → ℕ → Std.Format

Equations

• Bresnan1973.instReprClitic.repr Bresnan1973.Clitic.er prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Clitic.er")).group prec✝
• Bresnan1973.instReprClitic.repr Bresnan1973.Clitic.est prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Clitic.est")).group prec✝

@[instance_reducible]

instance Bresnan1973.instReprClitic : Repr Clitic

Equations

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

structure Bresnan1973.Det : Type

The Det of a QP: a particle, a clitic, or any or no beside -er.

• particle : Option Particle
• clitic : Option Clitic

@[instance_reducible]

instance Bresnan1973.instDecidableEqDet : DecidableEq Det

Equations

• Bresnan1973.instDecidableEqDet = Bresnan1973.instDecidableEqDet.decEq

def Bresnan1973.instDecidableEqDet.decEq (x✝ x✝¹ : Det) : Decidable (x✝ = x✝¹)

Equations

• Bresnan1973.instDecidableEqDet.decEq { particle := a, clitic := a_1 } { particle := b, clitic := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

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

Equations

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

@[instance_reducible]

instance Bresnan1973.instReprDet : Repr Det

Equations

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

def Bresnan1973.Det.WellFormed (d : Det) : Prop

A clitic shares the Det only with any or no: *as more, *too most (224).

Equations

• d.WellFormed = (d.clitic.isSome = true → ∀ p ∈ d.particle, p = Bresnan1973.Particle.any_ ∨ p = Bresnan1973.Particle.no_)

@[instance_reducible]

instance Bresnan1973.instDecidablePredDetWellFormed : DecidablePred Det.WellFormed

Equations

• Bresnan1973.instDecidablePredDetWellFormed x✝ = id inferInstance

inductive Bresnan1973.Q : Type

The Q position (6): much, little and enough select mass nouns, many and few indefinite plurals, enough both (1.3).

• 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 }

def Bresnan1973.Q.SelectsMass (q : Q) : Prop

The Qs that select mass nouns, and with them adjectives and adverbs.

Equations

• q.SelectsMass = (q = Bresnan1973.Q.much ∨ q = Bresnan1973.Q.little ∨ q = Bresnan1973.Q.enough)

@[instance_reducible]

instance Bresnan1973.instDecidablePredQSelectsMass : DecidablePred Q.SelectsMass

Equations

• Bresnan1973.instDecidablePredQSelectsMass x✝ = id inferInstance

def Bresnan1973.Q.SelectsCount (q : Q) : Prop

The Qs that select indefinite plurals.

Equations

• q.SelectsCount = (q = Bresnan1973.Q.many ∨ q = Bresnan1973.Q.few ∨ q = Bresnan1973.Q.enough)

@[instance_reducible]

instance Bresnan1973.instDecidablePredQSelectsCount : DecidablePred Q.SelectsCount

Equations

• Bresnan1973.instDecidablePredQSelectsCount x✝ = id inferInstance

structure Bresnan1973.QP : Type

A QP (6), (146c): (Det) Q.

• det : Det
• q : Q

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.instDecidableEqQP : DecidableEq QP

Equations

• Bresnan1973.instDecidableEqQP = Bresnan1973.instDecidableEqQP.decEq

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

Equations

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

@[instance_reducible]

instance Bresnan1973.instReprQP : Repr QP

Equations

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

def Bresnan1973.QP.WellFormed (qp : QP) : Prop

(107)–(109): enough is subcategorized for the null Det, *so enough, *enougher; with (224), the closed Det inventory of (4) and (5).

Equations

• qp.WellFormed = (qp.det.WellFormed ∧ (qp.q = Bresnan1973.Q.enough → qp.det = { }))

@[instance_reducible]

instance Bresnan1973.instDecidablePredQPWellFormed : DecidablePred QP.WellFormed

Equations

• Bresnan1973.instDecidablePredQPWellFormed x✝ = id inferInstance

inductive Bresnan1973.Form : Type

The suppletive forms of (7) and (223).

• more : Form
• less : Form
• fewer : Form
• most : Form
• least : Form
• fewest : Form

@[instance_reducible]

instance Bresnan1973.instDecidableEqForm : DecidableEq Form

Equations

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

def Bresnan1973.instReprForm.repr : Form → ℕ → Std.Format

Equations

• Bresnan1973.instReprForm.repr Bresnan1973.Form.more prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Form.more")).group prec✝
• Bresnan1973.instReprForm.repr Bresnan1973.Form.less prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Form.less")).group prec✝
• Bresnan1973.instReprForm.repr Bresnan1973.Form.fewer prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Form.fewer")).group prec✝
• Bresnan1973.instReprForm.repr Bresnan1973.Form.most prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Form.most")).group prec✝
• Bresnan1973.instReprForm.repr Bresnan1973.Form.least prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Form.least")).group prec✝
• Bresnan1973.instReprForm.repr Bresnan1973.Form.fewest prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Form.fewest")).group prec✝

@[instance_reducible]

instance Bresnan1973.instReprForm : Repr Form

Equations

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

def Bresnan1973.suppletion : Clitic → Q → Option Form

(7), (223): a clitic on Q surfaces suppletively, much + -er = more, little + -est = least; enough takes no clitic (107).

Equations

• Bresnan1973.suppletion Bresnan1973.Clitic.er Bresnan1973.Q.much = some Bresnan1973.Form.more
• Bresnan1973.suppletion Bresnan1973.Clitic.er Bresnan1973.Q.many = some Bresnan1973.Form.more
• Bresnan1973.suppletion Bresnan1973.Clitic.er Bresnan1973.Q.little = some Bresnan1973.Form.less
• Bresnan1973.suppletion Bresnan1973.Clitic.er Bresnan1973.Q.few = some Bresnan1973.Form.fewer
• Bresnan1973.suppletion Bresnan1973.Clitic.est Bresnan1973.Q.much = some Bresnan1973.Form.most
• Bresnan1973.suppletion Bresnan1973.Clitic.est Bresnan1973.Q.many = some Bresnan1973.Form.most
• Bresnan1973.suppletion Bresnan1973.Clitic.est Bresnan1973.Q.little = some Bresnan1973.Form.least
• Bresnan1973.suppletion Bresnan1973.Clitic.est Bresnan1973.Q.few = some Bresnan1973.Form.fewest
• Bresnan1973.suppletion x✝ Bresnan1973.Q.enough = none

def Bresnan1973.QP.suppletion (qp : QP) : Option Form

The suppletive surface of a QP, if any.

Equations

• qp.suppletion = qp.det.clitic.bind fun (x : Bresnan1973.Clitic) => Bresnan1973.suppletion x qp.q

theorem Bresnan1973.more_ambiguous : ∃ (q : Q) (q' : Q), q.SelectsCount ∧ ¬q.SelectsMass ∧ q'.SelectsMass ∧ ¬q'.SelectsCount ∧ suppletion Clitic.er q = suppletion Clitic.er q'

(232): more intelligent dogs has two sources, the partitive -er many of over the plural, a count Q, and the degree -er much on the adjective, a mass Q, which the suppletion of (7) does not tell apart.

Much Deletion and the simple comparative (1.1)

inductive Bresnan1973.Position : Type

Where a QP stands: as the left branch of its AP (146a), of its NP, the partitive, or of another QP (140a); as a modifier of a VP or S, the adverbial and substantive uses (257), (272); or, in a comparative clause, as a term of an identity with a definite measure phrase, six feet = x much (286a), or with a phrase, two friends = that many friends (287c).

• adjective : Position
• noun : Position
• quantifier : Position
• phrase : Position
• measure : Position
• term : Position

@[instance_reducible]

instance Bresnan1973.instDecidableEqPosition : DecidableEq Position

Equations

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

@[instance_reducible]

instance Bresnan1973.instReprPosition : Repr Position

Equations

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

def Bresnan1973.instReprPosition.repr : Position → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Bresnan1973.instReprPosition.repr Bresnan1973.Position.noun prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Position.noun")).group prec✝
• Bresnan1973.instReprPosition.repr Bresnan1973.Position.term prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Position.term")).group prec✝

def Bresnan1973.Position.InIdentity (p : Position) : Prop

A term of one of the identities of (286)–(287).

Equations

• p.InIdentity = (p = Bresnan1973.Position.measure ∨ p = Bresnan1973.Position.term)

@[instance_reducible]

instance Bresnan1973.instDecidablePredPositionInIdentity : DecidablePred Position.InIdentity

Equations

• Bresnan1973.instDecidablePredPositionInIdentity x✝ = id inferInstance

def Bresnan1973.MuchDeletes (qp : QP) (p : Position) : Prop

(10) Much Deletion, much → ∅ / [… _ A]_AP, ordered after -er Encliticizing (20): an uncliticized much directly before the adjective of its AP deletes, and only there (278); the clitic intervenes in [[much-er] tall], so *as much tall reduces to as tall while more tall survives (21).

Equations

• Bresnan1973.MuchDeletes qp p = (qp.q = Bresnan1973.Q.much ∧ qp.det.clitic = none ∧ p = Bresnan1973.Position.adjective)

@[instance_reducible]

instance Bresnan1973.instDecidableMuchDeletes (qp : QP) (p : Position) : Decidable (MuchDeletes qp p)

Equations

• Bresnan1973.instDecidableMuchDeletes qp p = id inferInstance

def Bresnan1973.Synthetic (qp : QP) (p : Position) : Prop

(21d): the simple comparative taller from the compound [[much-er] tall], so only for the QP that is the left branch of its AP (277).

Equations

• Bresnan1973.Synthetic qp p = (qp.q = Bresnan1973.Q.much ∧ qp.det.clitic = some Bresnan1973.Clitic.er ∧ p = Bresnan1973.Position.adjective)

@[instance_reducible]

instance Bresnan1973.instDecidableSynthetic (qp : QP) (p : Position) : Decidable (Synthetic qp p)

Equations

• Bresnan1973.instDecidableSynthetic qp p = id inferInstance

theorem Bresnan1973.Synthetic.not_muchDeletes {qp : QP} {p : Position} (h : Synthetic qp p) : ¬MuchDeletes qp p

Encliticizing protects much: the compound never loses its Q.

inductive Bresnan1973.Surface : Type

The surface of a QP before what it modifies: Q overt, much deleted, or the synthetic comparative.

• analytic : Surface
• deleted : Surface
• synthetic : Surface

@[instance_reducible]

instance Bresnan1973.instDecidableEqSurface : DecidableEq Surface

Equations

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

def Bresnan1973.instReprSurface.repr : Surface → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bresnan1973.instReprSurface : Repr Surface

Equations

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

def Bresnan1973.Surface.Licit (s : Surface) (qp : QP) (p : Position) : Prop

Much Deletion is obligatory where it applies, and the synthetic form needs the AP-internal compound.

Equations

• s.Licit qp p = ((s = Bresnan1973.Surface.deleted ↔ Bresnan1973.MuchDeletes qp p) ∧ (s = Bresnan1973.Surface.synthetic → Bresnan1973.Synthetic qp p))

@[instance_reducible]

instance Bresnan1973.instDecidableLicit (s : Surface) (qp : QP) (p : Position) : Decidable (s.Licit qp p)

Equations

• Bresnan1973.instDecidableLicit s qp p = id inferInstance

QP Raising and AP Shift (1.6)

def Bresnan1973.QPRaises (qp : QP) : Prop

(205) QP Raising needs the Det of Q empty: after -er Encliticizing, more, less and enough raise (207), while a particle, alone or beside -er, keeps the QP in place (208)–(209).

Equations

• Bresnan1973.QPRaises qp = (qp.det.particle = none)

@[instance_reducible]

instance Bresnan1973.instDecidablePredQPQPRaises : DecidablePred QPRaises

Equations

• Bresnan1973.instDecidablePredQPQPRaises x✝ = id inferInstance

inductive Bresnan1973.Order : Type

The order of the AP and the indefinite article in a predicative NP (111)–(116).

• prearticle : Order
• postarticle : Order

@[instance_reducible]

instance Bresnan1973.instDecidableEqOrder : DecidableEq Order

Equations

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

@[instance_reducible]

instance Bresnan1973.instReprOrder : Repr Order

Equations

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

def Bresnan1973.instReprOrder.repr : Order → ℕ → Std.Format

Equations

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

def Bresnan1973.Order.Licit (o : Order) (qp : QP) : Prop

(206) AP Shift moves the raised AP around the article, a more reliable man; an unraised QP keeps the AP before the article, too reliable a man, *a too reliable man (217)–(218).

Equations

• o.Licit qp = (o = Bresnan1973.Order.postarticle → Bresnan1973.QPRaises qp)

@[instance_reducible]

instance Bresnan1973.instDecidableLicit_1 (o : Order) (qp : QP) : Decidable (o.Licit qp)

Equations

• Bresnan1973.instDecidableLicit_1 o qp = id inferInstance

Comparative Formation (Section 2)

inductive Bresnan1973.Cat : Type

The categories over which the identities of (286)–(287) and deletion under nondistinctness are stated.

• qp : Cat
• ap : Cat
• np : Cat

@[instance_reducible]

instance Bresnan1973.instDecidableEqCat : DecidableEq Cat

Equations

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

@[instance_reducible]

instance Bresnan1973.instReprCat : Repr Cat

Equations

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

def Bresnan1973.instReprCat.repr : Cat → ℕ → Std.Format

Equations

• Bresnan1973.instReprCat.repr Bresnan1973.Cat.qp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Cat.qp")).group prec✝
• Bresnan1973.instReprCat.repr Bresnan1973.Cat.ap prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Cat.ap")).group prec✝
• Bresnan1973.instReprCat.repr Bresnan1973.Cat.np prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bresnan1973.Cat.np")).group prec✝

def Bresnan1973.Cat.Similar (a b : Cat) : Prop

Same or similar categories: QP and AP are interchangeable (1.4), six feet = that tall (286c), while an NP equates with no measure category, *Bill = that much (286b).

Equations

• a.Similar b = (a = b ∨ a = Bresnan1973.Cat.qp ∧ b = Bresnan1973.Cat.ap ∨ a = Bresnan1973.Cat.ap ∧ b = Bresnan1973.Cat.qp)

@[instance_reducible]

instance Bresnan1973.instDecidableRelCatSimilar : DecidableRel Cat.Similar

Equations

• Bresnan1973.instDecidableRelCatSimilar x✝¹ x✝ = id inferInstance

theorem Bresnan1973.Cat.Similar.symm {a b : Cat} : a.Similar b → b.Similar a

structure Bresnan1973.Head : Type

The head of the construction (Section 1): the constituent the clause must match, the position of its governing QP, and the polarity of the adjective that QP modifies, if any.

• cat : Cat
• site : Position
• polarity : Option Polarity

@[instance_reducible]

instance Bresnan1973.instDecidableEqHead : DecidableEq Head

Equations

• Bresnan1973.instDecidableEqHead = Bresnan1973.instDecidableEqHead.decEq

def Bresnan1973.instDecidableEqHead.decEq (x✝ x✝¹ : Head) : Decidable (x✝ = x✝¹)

Equations

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

def Bresnan1973.instReprHead.repr : Head → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Bresnan1973.instReprHead : Repr Head

Equations

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

def Bresnan1973.Head.Privative (h : Head) : Prop

(296): privative adjectives such as short admit no modifier of definite measurement, *five feet short.

Equations

• h.Privative = (h.polarity = some Polarity.negative)

@[instance_reducible]

instance Bresnan1973.instDecidablePredHeadPrivative : DecidablePred Head.Privative

Equations

• Bresnan1973.instDecidablePredHeadPrivative x✝ = id inferInstance

structure Bresnan1973.Supply : Type

What the clause supplies in the head's place: the category of the matching constituent and the position of its QP.

• cat : Cat
• site : Position

def Bresnan1973.instDecidableEqSupply.decEq (x✝ x✝¹ : Supply) : Decidable (x✝ = x✝¹)

Equations

• Bresnan1973.instDecidableEqSupply.decEq { cat := a, site := a_1 } { cat := b, site := 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.instDecidableEqSupply : DecidableEq Supply

Equations

• Bresnan1973.instDecidableEqSupply = Bresnan1973.instDecidableEqSupply.decEq

@[instance_reducible]

instance Bresnan1973.instReprSupply : Repr Supply

Equations

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

def Bresnan1973.instReprSupply.repr : Supply → ℕ → Std.Format

Equations

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

def Bresnan1973.Formation (h : Head) (c : Supply) : Prop

Comparative Formation: something in the clause is deleted under nondistinctness from the head. The clause must supply a constituent of the same or a similar category; a matched QP must be a term of an identity or the adverbial matching an adverbial head, since a left branch of an NP or AP cannot be factored out ((301), [Ros67]); and a Q nondistinct from the modifier of a privative adjective cannot be equated with a definite measure phrase (297).

Equations

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

@[instance_reducible]

instance Bresnan1973.instDecidableFormation (h : Head) (c : Supply) : Decidable (Formation h c)

Equations

• Bresnan1973.instDecidableFormation h c = id inferInstance

theorem Bresnan1973.not_formation_of_np {h : Head} {c : Supply} (hh : h.cat = Cat.qp) (hc : c.cat = Cat.np) : ¬Formation h c

(286b), (287b): no NP is equated with a measure category, so an NP standard never serves a QP head, *John is more than Bill tall.

theorem Bresnan1973.not_formation_of_privative {h : Head} {c : Supply} (hh : h.cat = Cat.qp) (hp : h.Privative) (hc : c.site = Position.measure) : ¬Formation h c

(297): a QP head modifying a privative adjective admits no definite measure in the clause, *more than five feet short.

theorem Bresnan1973.formation_ap_measure (site : Position) (polarity : Option Polarity) : Formation { cat := Cat.ap, site := site, polarity := polarity } { cat := Cat.ap, site := Position.measure }

(296b): with the AP as head the identity holds of the AP, and the definiteness of its Q is not at issue, shorter than five feet.

def Bresnan1973.ContractionLicit (h : Head) : Prop

Tensed-auxiliary contraction is inhibited directly before a removal site (264)–(266): the deleted constituent abuts the copula when the head's QP is AP-internal (274), not when it modifies the sentence (272).

Equations

• Bresnan1973.ContractionLicit h = (h.site ≠ Bresnan1973.Position.adjective)

@[instance_reducible]

instance Bresnan1973.instDecidablePredHeadContractionLicit : DecidablePred ContractionLicit

Equations

• Bresnan1973.instDecidablePredHeadContractionLicit x✝ = id inferInstance

The rows

def Bresnan1973.particleOf : String → Option Particle

Equations

• Bresnan1973.particleOf "as" = some Bresnan1973.Particle.as_
• Bresnan1973.particleOf "too" = some Bresnan1973.Particle.too
• Bresnan1973.particleOf "that" = some Bresnan1973.Particle.that_
• Bresnan1973.particleOf "so" = some Bresnan1973.Particle.so
• Bresnan1973.particleOf "any" = some Bresnan1973.Particle.any_
• Bresnan1973.particleOf "no" = some Bresnan1973.Particle.no_
• Bresnan1973.particleOf x✝ = none

def Bresnan1973.cliticOf : String → Option Clitic

Equations

• Bresnan1973.cliticOf "er" = some Bresnan1973.Clitic.er
• Bresnan1973.cliticOf "est" = some Bresnan1973.Clitic.est
• Bresnan1973.cliticOf x✝ = none

def Bresnan1973.qOf : String → Option Q

Equations

• Bresnan1973.qOf "much" = some Bresnan1973.Q.much
• Bresnan1973.qOf "many" = some Bresnan1973.Q.many
• Bresnan1973.qOf "little" = some Bresnan1973.Q.little
• Bresnan1973.qOf "few" = some Bresnan1973.Q.few
• Bresnan1973.qOf "enough" = some Bresnan1973.Q.enough
• Bresnan1973.qOf x✝ = none

def Bresnan1973.positionOf : String → Option Position

Equations

• Bresnan1973.positionOf "adjective" = some Bresnan1973.Position.adjective
• Bresnan1973.positionOf "noun" = some Bresnan1973.Position.noun
• Bresnan1973.positionOf "quantifier" = some Bresnan1973.Position.quantifier
• Bresnan1973.positionOf "phrase" = some Bresnan1973.Position.phrase
• Bresnan1973.positionOf "measure" = some Bresnan1973.Position.measure
• Bresnan1973.positionOf "term" = some Bresnan1973.Position.term
• Bresnan1973.positionOf x✝ = none

def Bresnan1973.catOf : String → Option Cat

Equations

• Bresnan1973.catOf "qp" = some Bresnan1973.Cat.qp
• Bresnan1973.catOf "ap" = some Bresnan1973.Cat.ap
• Bresnan1973.catOf "np" = some Bresnan1973.Cat.np
• Bresnan1973.catOf x✝ = none

def Bresnan1973.adjectiveOf : String → Option Degree.GradableAdjective

Equations

• Bresnan1973.adjectiveOf "tall" = some English.Adjectives.tall
• Bresnan1973.adjectiveOf "short" = some English.Adjectives.short
• Bresnan1973.adjectiveOf "high" = some English.Adjectives.high
• Bresnan1973.adjectiveOf "long" = some English.Adjectives.long
• Bresnan1973.adjectiveOf x✝ = none

def Bresnan1973.nounOf : String → Option English.Nouns.Noun

Equations

• Bresnan1973.nounOf "man" = some English.Nouns.man
• Bresnan1973.nounOf "father" = some English.Nouns.father
• Bresnan1973.nounOf "mother" = some English.Nouns.mother
• Bresnan1973.nounOf x✝ = none

def Bresnan1973.rows (set : String) : List Datum

The rows of one of the paper's paradigms.

Equations

• Bresnan1973.rows set = List.filter (fun (x : Datum) => decide (x.feature? "set" = some set)) Bresnan1973.Examples.all

def Bresnan1973.qpOf (e : Datum) : Option QP

A row's QP.

Equations

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

def Bresnan1973.positionOfRow (e : Datum) : Option Position

The position of a row's QP.

Equations

• Bresnan1973.positionOfRow e = (e.feature? "position").bind Bresnan1973.positionOf

def Bresnan1973.surfaceOf (e : Datum) : Option Surface

A row's surface form.

Equations

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

def Bresnan1973.orderOf (e : Datum) : Option Order

A row's order of AP and article.

Equations

• Bresnan1973.orderOf e = match e.feature? "order" with | some "prearticle" => some Bresnan1973.Order.prearticle | some "postarticle" => some Bresnan1973.Order.postarticle | x => none

def Bresnan1973.headOf (e : Datum) : Option Head

A row's head.

Equations

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

def Bresnan1973.supplyOf (e : Datum) : Option Supply

What a row's clause supplies.

Equations

• Bresnan1973.supplyOf e = do let cat ← (e.feature? "clause").bind Bresnan1973.catOf let site ← (e.feature? "clause_site").bind Bresnan1973.positionOf pure { cat := cat, site := site }

def Bresnan1973.Starred (e : Datum) : Prop

The paper's star.

Equations

• Bresnan1973.Starred e = (e.judgment = Judgment.ungrammatical)

@[instance_reducible]

instance Bresnan1973.instDecidablePredDatumStarred : DecidablePred Starred

Equations

• Bresnan1973.instDecidablePredDatumStarred x✝ = id inferInstance

def Bresnan1973.Contracted (e : Datum) : Prop

The clause's tensed auxiliary is contracted.

Equations

• Bresnan1973.Contracted e = (e.feature? "contraction" = some "yes")

@[instance_reducible]

instance Bresnan1973.instDecidablePredDatumContracted : DecidablePred Contracted

Equations

• Bresnan1973.instDecidablePredDatumContracted x✝ = id inferInstance

def Bresnan1973.Anomalous (e : Datum) : Prop

The sentence carries an anomalous implication.

Equations

• Bresnan1973.Anomalous e = (e.feature? "anomalous" = some "yes")

@[instance_reducible]

instance Bresnan1973.instDecidablePredDatumAnomalous : DecidablePred Anomalous

Equations

• Bresnan1973.instDecidablePredDatumAnomalous x✝ = id inferInstance

theorem Bresnan1973.det_rows (e : Datum) : e ∈ rows "det" → (¬Starred e ↔ ∃ qp ∈ qpOf e, qp.WellFormed)

(4)–(5), (107), (117)–(119), (224): the Det inventory of the QP.

theorem Bresnan1973.surface_rows (e : Datum) : e ∈ rows "surface" → (¬Starred e ↔ ∃ qp ∈ qpOf e, ∃ p ∈ positionOfRow e, ∃ s ∈ surfaceOf e, s.Licit qp p)

(1)–(19), (84)–(85), (275)–(279): the surface of a QP before what it modifies is acceptable exactly when Much Deletion and simple comparative formation license it; problem (C), the analytic and synthetic comparatives across adjectives, falls under the AP-internal condition.

theorem Bresnan1973.shift_rows (e : Datum) : e ∈ rows "shift" → (¬Starred e ↔ ∃ qp ∈ qpOf e, ∃ o ∈ orderOf e, o.Licit qp)

(111)–(116), (125)–(127), (217)–(218): the AP shifts around the article exactly when the QP raises, on an empty Det.

theorem Bresnan1973.formation_rows (e : Datum) : e ∈ rows "formation" → (¬Starred e ↔ ∃ h ∈ headOf e, ∃ c ∈ supplyOf e, Formation h c ∧ (Contracted e → ContractionLicit h))

(242)–(300): a comparative is acceptable exactly when Comparative Formation finds a nondistinct constituent in the clause and any contraction keeps clear of the removal site: problems (B) and (D), the object and predicate heads of (252)–(255), the positioning of than six feet and than Bill (280)–(283), and the left branch of (300).

theorem Bresnan1973.taller_man_rows (e : Datum) : e ∈ rows "formation" → (Anomalous e ↔ ∃ h ∈ headOf e, h.cat = Cat.np ∧ ∃ s ∈ (e.feature? "standard").bind nounOf, ∃ n ∈ (e.feature? "noun").bind nounOf, s.gender ≠ n.gender)

Problem (A): (242d) implies that my mother is a man because its head is the predicative NP x much tall a man (243), which the clause predicates of the standard; with the AP head of (251), or a standard of the noun's gender, nothing is amiss.