But-Exceptives [VF93]

Empirical patterns for "X but Y" exceptive constructions, anchored on [VF93]'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 Semantics/Quantification/Exceptive.lean. The connection between this file's Fragment-derived predictions and those operators is not yet wired up — TODO.

inductive VonFintel1993.QuantifierType : Type

Type of quantifier for exceptive compatibility.

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

@[implicit_reducible]

instance VonFintel1993.instDecidableEqQuantifierType : DecidableEq QuantifierType

Equations

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

def VonFintel1993.instReprQuantifierType.repr : QuantifierType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance VonFintel1993.instReprQuantifierType : Repr QuantifierType

Equations

• VonFintel1993.instReprQuantifierType = { reprPrec := VonFintel1993.instReprQuantifierType.repr }

structure 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 VonFintel1993.instReprButExceptiveExample : Repr ButExceptiveExample

Equations

• VonFintel1993.instReprButExceptiveExample = { reprPrec := VonFintel1993.instReprButExceptiveExample.repr }

def VonFintel1993.instReprButExceptiveExample.repr : ButExceptiveExample → ℕ → Std.Format

Equations

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

def VonFintel1993.every_but_john : ButExceptiveExample

Equations

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

def VonFintel1993.all_but_mary : ButExceptiveExample

Equations

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

def VonFintel1993.each_but_sue : ButExceptiveExample

Equations

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

def VonFintel1993.no_one_but_john : ButExceptiveExample

Equations

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

def VonFintel1993.none_but_mary : ButExceptiveExample

Equations

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

def VonFintel1993.some_but_john : ButExceptiveExample

Equations

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

def VonFintel1993.a_but_mary : ButExceptiveExample

Equations

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

def VonFintel1993.several_but_sue : ButExceptiveExample

Equations

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

def VonFintel1993.most_but_john : ButExceptiveExample

Equations

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

def VonFintel1993.many_but_mary : ButExceptiveExample

Equations

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

def VonFintel1993.few_but_sue : ButExceptiveExample

Equations

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

def VonFintel1993.two_but_john : ButExceptiveExample

Equations

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

def VonFintel1993.exactly_five_but : ButExceptiveExample

Equations

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

def VonFintel1993.butExceptiveExamples : List ButExceptiveExample

All but-exceptive examples.

Equations

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

def VonFintel1993.predictExceptiveGrammaticality (qt : QuantifierType) : Bool

Predict grammaticality from quantifier type.

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

Equations

• VonFintel1993.predictExceptiveGrammaticality VonFintel1993.QuantifierType.universalPositive = true
• VonFintel1993.predictExceptiveGrammaticality VonFintel1993.QuantifierType.universalNegative = true
• VonFintel1993.predictExceptiveGrammaticality VonFintel1993.QuantifierType.existential = false
• VonFintel1993.predictExceptiveGrammaticality VonFintel1993.QuantifierType.proportional = false
• VonFintel1993.predictExceptiveGrammaticality VonFintel1993.QuantifierType.numeral = false

Exception Uniqueness

[Gaj02]

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 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 VonFintel1993.instReprExceptionCardinalityExample : Repr ExceptionCardinalityExample

Equations

• VonFintel1993.instReprExceptionCardinalityExample = { reprPrec := VonFintel1993.instReprExceptionCardinalityExample.repr }

def VonFintel1993.instReprExceptionCardinalityExample.repr : ExceptionCardinalityExample → ℕ → Std.Format

Equations

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

def VonFintel1993.single_exception : ExceptionCardinalityExample

Equations

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

def VonFintel1993.two_exceptions : ExceptionCardinalityExample

Equations

• VonFintel1993.two_exceptions = { sentence := "Everyone but John and Mary passed", numExceptions := 2, acceptability := 3, notes := "Two exceptions: degraded, requires list interpretation" }

def VonFintel1993.three_exceptions : ExceptionCardinalityExample

Equations

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

def VonFintel1993.exceptionCardinalityExamples : List ExceptionCardinalityExample

All exception cardinality examples.

Equations

• VonFintel1993.exceptionCardinalityExamples = [VonFintel1993.single_exception, VonFintel1993.two_exceptions, VonFintel1993.three_exceptions]

structure 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?

@[implicit_reducible]

instance VonFintel1993.instReprCrossLinguisticExceptive : Repr CrossLinguisticExceptive

Equations

• VonFintel1993.instReprCrossLinguisticExceptive = { reprPrec := VonFintel1993.instReprCrossLinguisticExceptive.repr }

def VonFintel1993.instReprCrossLinguisticExceptive.repr : CrossLinguisticExceptive → ℕ → Std.Format

Equations

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

def VonFintel1993.english_but : CrossLinguisticExceptive

Equations

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

def VonFintel1993.german_ausser : CrossLinguisticExceptive

Equations

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

def VonFintel1993.french_sauf : CrossLinguisticExceptive

Equations

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

def VonFintel1993.spanish_excepto : CrossLinguisticExceptive

Equations

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

def VonFintel1993.crossLinguisticExamples : List CrossLinguisticExceptive

All cross-linguistic examples.

Equations

• VonFintel1993.crossLinguisticExamples = [VonFintel1993.english_but, VonFintel1993.german_ausser, VonFintel1993.french_sauf, VonFintel1993.spanish_excepto]

inductive VonFintel1993.ExceptiveConstruction : Type

Related exceptive-like constructions.

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

@[implicit_reducible]

instance VonFintel1993.instDecidableEqExceptiveConstruction : DecidableEq ExceptiveConstruction

Equations

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

@[implicit_reducible]

instance VonFintel1993.instReprExceptiveConstruction : Repr ExceptiveConstruction

Equations

• VonFintel1993.instReprExceptiveConstruction = { reprPrec := VonFintel1993.instReprExceptiveConstruction.repr }

def VonFintel1993.instReprExceptiveConstruction.repr : ExceptiveConstruction → ℕ → Std.Format

Equations

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

structure VonFintel1993.ExceptiveConstructionExample : Type

Comparison of exceptive constructions.

• construction : ExceptiveConstruction

  Construction type

• exampleSentence : String

  Example

• hasUniversalConstraint : Bool

  Same universal constraint?

• notes : String

  Additional notes

def VonFintel1993.instReprExceptiveConstructionExample.repr : ExceptiveConstructionExample → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance VonFintel1993.instReprExceptiveConstructionExample : Repr ExceptiveConstructionExample

Equations

• VonFintel1993.instReprExceptiveConstructionExample = { reprPrec := VonFintel1993.instReprExceptiveConstructionExample.repr }

def VonFintel1993.but_construction : ExceptiveConstructionExample

Equations

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

def VonFintel1993.except_construction : ExceptiveConstructionExample

Equations

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

def VonFintel1993.other_than_construction : ExceptiveConstructionExample

Equations

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

def VonFintel1993.besides_construction : ExceptiveConstructionExample

Equations

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

def VonFintel1993.exceptiveConstructionExamples : List ExceptiveConstructionExample

All exceptive construction examples.

Equations

• VonFintel1993.exceptiveConstructionExamples = [VonFintel1993.but_construction, VonFintel1993.except_construction, VonFintel1993.other_than_construction, VonFintel1993.besides_construction]

def VonFintel1993.qforceToExceptiveType : Quantification.Lexicon.QForce → Option QuantifierType

Map Fragment QForce to Exceptive QuantifierType.

Equations

• VonFintel1993.qforceToExceptiveType Quantification.Lexicon.QForce.universal = some VonFintel1993.QuantifierType.universalPositive
• VonFintel1993.qforceToExceptiveType Quantification.Lexicon.QForce.negative = some VonFintel1993.QuantifierType.universalNegative
• VonFintel1993.qforceToExceptiveType Quantification.Lexicon.QForce.existential = some VonFintel1993.QuantifierType.existential
• VonFintel1993.qforceToExceptiveType Quantification.Lexicon.QForce.proportional = some VonFintel1993.QuantifierType.proportional
• VonFintel1993.qforceToExceptiveType Quantification.Lexicon.QForce.definite = none

theorem VonFintel1993.fragment_exceptive_bridge : English.Determiners.QuantityWord.all.entry.qforce = Quantification.Lexicon.QForce.universal ∧ predictExceptiveGrammaticality QuantifierType.universalPositive = true ∧ English.Determiners.QuantityWord.none_.entry.qforce = Quantification.Lexicon.QForce.negative ∧ predictExceptiveGrammaticality QuantifierType.universalNegative = true ∧ English.Determiners.QuantityWord.some_.entry.qforce = 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 [VF93]. "Every student but John" ✓ vs "*Some student but John" ✗.

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

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