inductive Phenomena.Polarity.Exceptives.QuantifierType : Type

Type of quantifier for exceptive compatibility.

• universalPositive : QuantifierType
• universalNegative : QuantifierType
• existential : QuantifierType
• proportional : QuantifierType
• numeral : QuantifierType

instance Phenomena.Polarity.Exceptives.instDecidableEqQuantifierType : DecidableEq QuantifierType

Equations

• Phenomena.Polarity.Exceptives.instDecidableEqQuantifierType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Polarity.Exceptives.instBEqQuantifierType.beq : QuantifierType → QuantifierType → Bool

Equations

• Phenomena.Polarity.Exceptives.instBEqQuantifierType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Polarity.Exceptives.instBEqQuantifierType : BEq QuantifierType

Equations

• Phenomena.Polarity.Exceptives.instBEqQuantifierType = { beq := Phenomena.Polarity.Exceptives.instBEqQuantifierType.beq }

def Phenomena.Polarity.Exceptives.instReprQuantifierType.repr : QuantifierType → ℕ → Std.Format

Equations

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

instance Phenomena.Polarity.Exceptives.instReprQuantifierType : Repr QuantifierType

Equations

• Phenomena.Polarity.Exceptives.instReprQuantifierType = { reprPrec := Phenomena.Polarity.Exceptives.instReprQuantifierType.repr }

structure Phenomena.Polarity.Exceptives.ButExceptiveExample : Type

But-exceptive example with grammaticality judgment.

• quantifier : String

  The quantifier used

• quantifierType : QuantifierType

  Type of quantifier

• sentence : String

  The sentence

• grammatical : Bool

  Is it grammatical?

• notes : String

  Notes

def Phenomena.Polarity.Exceptives.instReprButExceptiveExample.repr : ButExceptiveExample → ℕ → Std.Format

Equations

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

instance Phenomena.Polarity.Exceptives.instReprButExceptiveExample : Repr ButExceptiveExample

Equations

• Phenomena.Polarity.Exceptives.instReprButExceptiveExample = { reprPrec := Phenomena.Polarity.Exceptives.instReprButExceptiveExample.repr }

def Phenomena.Polarity.Exceptives.every_but_john : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Exceptives.all_but_mary : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Exceptives.each_but_sue : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Exceptives.no_one_but_john : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Exceptives.none_but_mary : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Exceptives.some_but_john : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Exceptives.a_but_mary : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Exceptives.several_but_sue : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Exceptives.most_but_john : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Exceptives.many_but_mary : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Exceptives.few_but_sue : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Exceptives.two_but_john : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Exceptives.exactly_five_but : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Exceptives.butExceptiveExamples : List ButExceptiveExample

All but-exceptive examples.

Equations

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

def Phenomena.Polarity.Exceptives.predictExceptiveGrammaticality (qt : QuantifierType) : Bool

Predict grammaticality from quantifier type.

The generalization: only universal quantifiers (positive or negative) license but-exceptives.

Equations

• Phenomena.Polarity.Exceptives.predictExceptiveGrammaticality Phenomena.Polarity.Exceptives.QuantifierType.universalPositive = true
• Phenomena.Polarity.Exceptives.predictExceptiveGrammaticality Phenomena.Polarity.Exceptives.QuantifierType.universalNegative = true
• Phenomena.Polarity.Exceptives.predictExceptiveGrammaticality Phenomena.Polarity.Exceptives.QuantifierType.existential = false
• Phenomena.Polarity.Exceptives.predictExceptiveGrammaticality Phenomena.Polarity.Exceptives.QuantifierType.proportional = false
• Phenomena.Polarity.Exceptives.predictExceptiveGrammaticality Phenomena.Polarity.Exceptives.QuantifierType.numeral = false

Exception Uniqueness

@cite{gajewski-2002}

The but-exceptive typically requires that the exception be unique:

✓ "Everyone but John passed" (one exception) ? "Everyone but John and Mary passed" (multiple exceptions)

The multiple-exception case is degraded or requires special interpretation.

structure Phenomena.Polarity.Exceptives.ExceptionCardinalityExample : Type

Data on exception cardinality.

• sentence : String

  The sentence

• numExceptions : ℕ

  Number of exceptions

• acceptability : ℕ

  Acceptability (1-5 scale)

• notes : String

  Notes

instance Phenomena.Polarity.Exceptives.instReprExceptionCardinalityExample : Repr ExceptionCardinalityExample

Equations

• Phenomena.Polarity.Exceptives.instReprExceptionCardinalityExample = { reprPrec := Phenomena.Polarity.Exceptives.instReprExceptionCardinalityExample.repr }

def Phenomena.Polarity.Exceptives.instReprExceptionCardinalityExample.repr : ExceptionCardinalityExample → ℕ → Std.Format

Equations

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

def Phenomena.Polarity.Exceptives.single_exception : ExceptionCardinalityExample

Equations

• Phenomena.Polarity.Exceptives.single_exception = { sentence := "Everyone but John passed", numExceptions := 1, acceptability := 5, notes := "Single exception: fully acceptable" }

def Phenomena.Polarity.Exceptives.two_exceptions : ExceptionCardinalityExample

Equations

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

def Phenomena.Polarity.Exceptives.three_exceptions : ExceptionCardinalityExample

Equations

• Phenomena.Polarity.Exceptives.three_exceptions = { sentence := "Everyone but John, Mary, and Sue passed", numExceptions := 3, acceptability := 2, notes := "Three exceptions: further degraded" }

def Phenomena.Polarity.Exceptives.exceptionCardinalityExamples : List ExceptionCardinalityExample

All exception cardinality examples.

Equations

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

structure Phenomena.Polarity.Exceptives.CrossLinguisticExceptive : Type

Cross-linguistic but-exceptive data.

• language : String

  Language

• exceptiveMorpheme : String

  Exceptive morpheme

• exampleSentence : String

  Example sentence

• gloss : String

  Gloss

• universalConstraint : Bool

  Same universal constraint?

instance Phenomena.Polarity.Exceptives.instReprCrossLinguisticExceptive : Repr CrossLinguisticExceptive

Equations

• Phenomena.Polarity.Exceptives.instReprCrossLinguisticExceptive = { reprPrec := Phenomena.Polarity.Exceptives.instReprCrossLinguisticExceptive.repr }

def Phenomena.Polarity.Exceptives.instReprCrossLinguisticExceptive.repr : CrossLinguisticExceptive → ℕ → Std.Format

Equations

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

def Phenomena.Polarity.Exceptives.english_but : CrossLinguisticExceptive

Equations

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

def Phenomena.Polarity.Exceptives.german_ausser : CrossLinguisticExceptive

Equations

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

def Phenomena.Polarity.Exceptives.french_sauf : CrossLinguisticExceptive

Equations

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

def Phenomena.Polarity.Exceptives.spanish_excepto : CrossLinguisticExceptive

Equations

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

def Phenomena.Polarity.Exceptives.crossLinguisticExamples : List CrossLinguisticExceptive

All cross-linguistic examples.

Equations

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

inductive Phenomena.Polarity.Exceptives.ExceptiveConstruction : Type

Related exceptive-like constructions.

• butExceptive : ExceptiveConstruction
• exceptExceptive : ExceptiveConstruction
• otherThan : ExceptiveConstruction
• besidesExceptive : ExceptiveConstruction

instance Phenomena.Polarity.Exceptives.instDecidableEqExceptiveConstruction : DecidableEq ExceptiveConstruction

Equations

• Phenomena.Polarity.Exceptives.instDecidableEqExceptiveConstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Polarity.Exceptives.instBEqExceptiveConstruction : BEq ExceptiveConstruction

Equations

• Phenomena.Polarity.Exceptives.instBEqExceptiveConstruction = { beq := Phenomena.Polarity.Exceptives.instBEqExceptiveConstruction.beq }

def Phenomena.Polarity.Exceptives.instBEqExceptiveConstruction.beq : ExceptiveConstruction → ExceptiveConstruction → Bool

Equations

• Phenomena.Polarity.Exceptives.instBEqExceptiveConstruction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Polarity.Exceptives.instReprExceptiveConstruction.repr : ExceptiveConstruction → ℕ → Std.Format

Equations

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

instance Phenomena.Polarity.Exceptives.instReprExceptiveConstruction : Repr ExceptiveConstruction

Equations

• Phenomena.Polarity.Exceptives.instReprExceptiveConstruction = { reprPrec := Phenomena.Polarity.Exceptives.instReprExceptiveConstruction.repr }

structure Phenomena.Polarity.Exceptives.ExceptiveConstructionExample : Type

Comparison of exceptive constructions.

• construction : ExceptiveConstruction

  Construction type

• exampleSentence : String

  Example

• hasUniversalConstraint : Bool

  Same universal constraint?

• notes : String

  Additional notes

instance Phenomena.Polarity.Exceptives.instReprExceptiveConstructionExample : Repr ExceptiveConstructionExample

Equations

• Phenomena.Polarity.Exceptives.instReprExceptiveConstructionExample = { reprPrec := Phenomena.Polarity.Exceptives.instReprExceptiveConstructionExample.repr }

def Phenomena.Polarity.Exceptives.instReprExceptiveConstructionExample.repr : ExceptiveConstructionExample → ℕ → Std.Format

Equations

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

def Phenomena.Polarity.Exceptives.but_construction : ExceptiveConstructionExample

Equations

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

def Phenomena.Polarity.Exceptives.except_construction : ExceptiveConstructionExample

Equations

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

def Phenomena.Polarity.Exceptives.other_than_construction : ExceptiveConstructionExample

Equations

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

def Phenomena.Polarity.Exceptives.besides_construction : ExceptiveConstructionExample

Equations

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

def Phenomena.Polarity.Exceptives.exceptiveConstructionExamples : List ExceptiveConstructionExample

All exceptive construction examples.

Equations

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

def Phenomena.Polarity.Exceptives.qforceToExceptiveType : Fragments.English.Determiners.QForce → Option QuantifierType

Map Fragment QForce to Exceptive QuantifierType.

Equations

• Phenomena.Polarity.Exceptives.qforceToExceptiveType Fragments.English.Determiners.QForce.universal = some Phenomena.Polarity.Exceptives.QuantifierType.universalPositive
• Phenomena.Polarity.Exceptives.qforceToExceptiveType Fragments.English.Determiners.QForce.negative = some Phenomena.Polarity.Exceptives.QuantifierType.universalNegative
• Phenomena.Polarity.Exceptives.qforceToExceptiveType Fragments.English.Determiners.QForce.existential = some Phenomena.Polarity.Exceptives.QuantifierType.existential
• Phenomena.Polarity.Exceptives.qforceToExceptiveType Fragments.English.Determiners.QForce.proportional = some Phenomena.Polarity.Exceptives.QuantifierType.proportional
• Phenomena.Polarity.Exceptives.qforceToExceptiveType Fragments.English.Determiners.QForce.definite = none

theorem Phenomena.Polarity.Exceptives.fragment_exceptive_bridge : Fragments.English.Determiners.QuantityWord.all.entry.qforce = Fragments.English.Determiners.QForce.universal ∧ predictExceptiveGrammaticality QuantifierType.universalPositive = true ∧ Fragments.English.Determiners.QuantityWord.none_.entry.qforce = Fragments.English.Determiners.QForce.negative ∧ predictExceptiveGrammaticality QuantifierType.universalNegative = true ∧ Fragments.English.Determiners.QuantityWord.some_.entry.qforce = Fragments.English.Determiners.QForce.existential ∧ predictExceptiveGrammaticality QuantifierType.existential = false

Universal quantifiers in the Fragment license but-exceptives; existential quantifiers don't. This connects Fragment metadata to the empirical generalization in @cite{von-fintel-1993}. "Every student but John" ✓ vs "*Some student but John" ✗.

theorem Phenomena.Polarity.Exceptives.universal_qforce_partition : ((List.map (fun (x : Fragments.English.Determiners.QuantityWord) => x.entry.qforce) [Fragments.English.Determiners.QuantityWord.all, Fragments.English.Determiners.QuantityWord.none_]).all fun (q : Fragments.English.Determiners.QForce) => q == Fragments.English.Determiners.QForce.universal || q == Fragments.English.Determiners.QForce.negative) = true ∧ ((List.map (fun (x : Fragments.English.Determiners.QuantityWord) => x.entry.qforce) [Fragments.English.Determiners.QuantityWord.some_, Fragments.English.Determiners.QuantityWord.few, Fragments.English.Determiners.QuantityWord.half, Fragments.English.Determiners.QuantityWord.most]).all fun (q : Fragments.English.Determiners.QForce) => q != Fragments.English.Determiners.QForce.universal && q != Fragments.English.Determiners.QForce.negative) = true

Only the two QForce.universal/.negative quantity words license exceptives; the remaining four (existential, proportional) do not.