But-Exceptives @cite{von-fintel-1993}

Empirical patterns for "X but Y" exceptive constructions, anchored on @cite{von-fintel-1993}'s observation that but-exceptives require universal quantifiers (positive or negative):

Quantifier	Example	Grammatical
every	"everyone but John"	✓
no	"no one but John"	✓
some	"*someone but John"	✗
many	"*many people but John"	✗
few	"*few people but John"	✗

The but-exceptive subtracts the exception from the quantifier's domain and asserts that without the exception, the claim would be false.

This file provides predictExceptiveGrammaticality : QuantifierType → Bool plus a Fragment-side bridge qforceToExceptiveType that maps Fragment QForce values to QuantifierType, with fragment_exceptive_bridge showing the prediction agrees with the Fragment classification.

The semantic operators (ExcI, ExcE, ExcW, ExcS) live in Theories/Semantics/Quantification/Exceptive.lean. The connection between this file's Fragment-derived predictions and those operators is not yet wired up — TODO.

inductive Phenomena.Polarity.Studies.VonFintel1993.QuantifierType : Type

Type of quantifier for exceptive compatibility.

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

@[implicit_reducible]

instance Phenomena.Polarity.Studies.VonFintel1993.instDecidableEqQuantifierType : DecidableEq QuantifierType

Equations

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

@[implicit_reducible]

instance Phenomena.Polarity.Studies.VonFintel1993.instReprQuantifierType : Repr QuantifierType

Equations

• Phenomena.Polarity.Studies.VonFintel1993.instReprQuantifierType = { reprPrec := Phenomena.Polarity.Studies.VonFintel1993.instReprQuantifierType.repr }

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

Equations

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

structure Phenomena.Polarity.Studies.VonFintel1993.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

@[implicit_reducible]

instance Phenomena.Polarity.Studies.VonFintel1993.instReprButExceptiveExample : Repr ButExceptiveExample

Equations

• Phenomena.Polarity.Studies.VonFintel1993.instReprButExceptiveExample = { reprPrec := Phenomena.Polarity.Studies.VonFintel1993.instReprButExceptiveExample.repr }

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

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.every_but_john : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.all_but_mary : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.each_but_sue : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.no_one_but_john : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.none_but_mary : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.some_but_john : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.a_but_mary : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.several_but_sue : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.most_but_john : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.many_but_mary : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.few_but_sue : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.two_but_john : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.exactly_five_but : ButExceptiveExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.butExceptiveExamples : List ButExceptiveExample

All but-exceptive examples.

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.predictExceptiveGrammaticality (qt : QuantifierType) : Bool

Predict grammaticality from quantifier type.

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

Equations

• Phenomena.Polarity.Studies.VonFintel1993.predictExceptiveGrammaticality Phenomena.Polarity.Studies.VonFintel1993.QuantifierType.universalPositive = true
• Phenomena.Polarity.Studies.VonFintel1993.predictExceptiveGrammaticality Phenomena.Polarity.Studies.VonFintel1993.QuantifierType.universalNegative = true
• Phenomena.Polarity.Studies.VonFintel1993.predictExceptiveGrammaticality Phenomena.Polarity.Studies.VonFintel1993.QuantifierType.existential = false
• Phenomena.Polarity.Studies.VonFintel1993.predictExceptiveGrammaticality Phenomena.Polarity.Studies.VonFintel1993.QuantifierType.proportional = false
• Phenomena.Polarity.Studies.VonFintel1993.predictExceptiveGrammaticality Phenomena.Polarity.Studies.VonFintel1993.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.Studies.VonFintel1993.ExceptionCardinalityExample : Type

Data on exception cardinality.

• sentence : String

  The sentence

• numExceptions : ℕ

  Number of exceptions

• acceptability : ℕ

  Acceptability (1-5 scale)

• notes : String

  Notes

@[implicit_reducible]

instance Phenomena.Polarity.Studies.VonFintel1993.instReprExceptionCardinalityExample : Repr ExceptionCardinalityExample

Equations

• Phenomena.Polarity.Studies.VonFintel1993.instReprExceptionCardinalityExample = { reprPrec := Phenomena.Polarity.Studies.VonFintel1993.instReprExceptionCardinalityExample.repr }

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

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.single_exception : ExceptionCardinalityExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.two_exceptions : ExceptionCardinalityExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.three_exceptions : ExceptionCardinalityExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.exceptionCardinalityExamples : List ExceptionCardinalityExample

All exception cardinality examples.

Equations

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

structure Phenomena.Polarity.Studies.VonFintel1993.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?

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

Equations

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

@[implicit_reducible]

instance Phenomena.Polarity.Studies.VonFintel1993.instReprCrossLinguisticExceptive : Repr CrossLinguisticExceptive

Equations

• Phenomena.Polarity.Studies.VonFintel1993.instReprCrossLinguisticExceptive = { reprPrec := Phenomena.Polarity.Studies.VonFintel1993.instReprCrossLinguisticExceptive.repr }

def Phenomena.Polarity.Studies.VonFintel1993.english_but : CrossLinguisticExceptive

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.german_ausser : CrossLinguisticExceptive

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.french_sauf : CrossLinguisticExceptive

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.spanish_excepto : CrossLinguisticExceptive

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.crossLinguisticExamples : List CrossLinguisticExceptive

All cross-linguistic examples.

Equations

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

inductive Phenomena.Polarity.Studies.VonFintel1993.ExceptiveConstruction : Type

Related exceptive-like constructions.

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

@[implicit_reducible]

instance Phenomena.Polarity.Studies.VonFintel1993.instDecidableEqExceptiveConstruction : DecidableEq ExceptiveConstruction

Equations

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

@[implicit_reducible]

instance Phenomena.Polarity.Studies.VonFintel1993.instReprExceptiveConstruction : Repr ExceptiveConstruction

Equations

• Phenomena.Polarity.Studies.VonFintel1993.instReprExceptiveConstruction = { reprPrec := Phenomena.Polarity.Studies.VonFintel1993.instReprExceptiveConstruction.repr }

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

Equations

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

structure Phenomena.Polarity.Studies.VonFintel1993.ExceptiveConstructionExample : Type

Comparison of exceptive constructions.

• construction : ExceptiveConstruction

  Construction type

• exampleSentence : String

  Example

• hasUniversalConstraint : Bool

  Same universal constraint?

• notes : String

  Additional notes

@[implicit_reducible]

instance Phenomena.Polarity.Studies.VonFintel1993.instReprExceptiveConstructionExample : Repr ExceptiveConstructionExample

Equations

• Phenomena.Polarity.Studies.VonFintel1993.instReprExceptiveConstructionExample = { reprPrec := Phenomena.Polarity.Studies.VonFintel1993.instReprExceptiveConstructionExample.repr }

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

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.but_construction : ExceptiveConstructionExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.except_construction : ExceptiveConstructionExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.other_than_construction : ExceptiveConstructionExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.besides_construction : ExceptiveConstructionExample

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.exceptiveConstructionExamples : List ExceptiveConstructionExample

All exceptive construction examples.

Equations

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

def Phenomena.Polarity.Studies.VonFintel1993.qforceToExceptiveType : Theories.Semantics.Quantification.Lexicon.QForce → Option QuantifierType

Map Fragment QForce to Exceptive QuantifierType.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Polarity.Studies.VonFintel1993.qforceToExceptiveType Theories.Semantics.Quantification.Lexicon.QForce.definite = none

theorem Phenomena.Polarity.Studies.VonFintel1993.fragment_exceptive_bridge : Quantification.Inventory.QuantityWord.all.entry.qforce = Theories.Semantics.Quantification.Lexicon.QForce.universal ∧ predictExceptiveGrammaticality QuantifierType.universalPositive = true ∧ Quantification.Inventory.QuantityWord.none_.entry.qforce = Theories.Semantics.Quantification.Lexicon.QForce.negative ∧ predictExceptiveGrammaticality QuantifierType.universalNegative = true ∧ Quantification.Inventory.QuantityWord.some_.entry.qforce = Theories.Semantics.Quantification.Lexicon.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.Studies.VonFintel1993.universal_qforce_partition : ((List.map (fun (x : Quantification.Inventory.QuantityWord) => x.entry.qforce) [Quantification.Inventory.QuantityWord.all, Quantification.Inventory.QuantityWord.none_]).all fun (q : Theories.Semantics.Quantification.Lexicon.QForce) => q == Theories.Semantics.Quantification.Lexicon.QForce.universal || q == Theories.Semantics.Quantification.Lexicon.QForce.negative) = true ∧ ((List.map (fun (x : Quantification.Inventory.QuantityWord) => x.entry.qforce) [Quantification.Inventory.QuantityWord.some_, Quantification.Inventory.QuantityWord.few, Quantification.Inventory.QuantityWord.half, Quantification.Inventory.QuantityWord.most]).all fun (q : Theories.Semantics.Quantification.Lexicon.QForce) => q != Theories.Semantics.Quantification.Lexicon.QForce.universal && q != Theories.Semantics.Quantification.Lexicon.QForce.negative) = true

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