von Fintel (1993): Exceptive Constructions

von Fintel gives the English but-phrase of every student but John a least-exception semantics. Plain domain subtraction, reading students but John as the students minus John, neither explains why but occurs only with every and no nor blocks the inference to every student but John and Jill, and adding the requirement that the quantification fail without the subtraction still admits most. On the least-exception semantics the but-phrase instead names the exception set, the least set whose subtraction makes the quantification true (Exceptive.IsExceptionSet), which with every is the restrictor minus the scope and with no their intersection. Free exceptives like except for John carry subtraction with restrictiveness only (Exceptive.Restrictive), which is why they also occur with most.

Main statements

• GuaranteesException: a determiner guarantees an exception set when every false quantification has one. Every and no guarantee one, some never has one, and most has none in the paper's five-student situation though it has one in a two-student limiting case; the paper reads the co-occurrence restriction as a grammaticization of this contrast.
• not_isExceptionSet_of_lt, eq_of_isExceptionSet_ident: the unique least exception blocks the enlargement inference and the conjunction of two but-phrases.
• not_exists_nounModifier: no operation on the restrictor alone yields the but-phrase's truth conditions.
• isExceptionSet_every_of_restrictive: with a universal determiner the free exceptive pragmatically strengthens to the but reading.
• but_predicted, exceptFor_predicted: the paper's exceptive examples, read through the English fragment's determiner denotations, are judged acceptable exactly as the two semantics predict.

Implementation notes

• Restrictor, scope and exception set are predicates ordered pointwise, so the truth conditions are lattice equations and the five-student and two-student models use ⊤ and Fin restrictors.
• The guarantee of an exception set is conditional on a false quantification, the paper's "if there is any at all"; the unconditional version also holds for every and no, whose exception set is then empty (Exceptive.isExceptionSet_every).
• The strengthening of a free exceptive to the but reading takes as hypothesis that the exception set contains only exceptions, the paper's gloss of the uniqueness condition, which pragmatics supplies.
• The determiner any of Horn's paradigm has no reading in the paper or the fragment, so its rows are not predicted; likewise the definite of except for Jane, my relatives and the minimality-based besides, which the paper leaves to further research.
• Not formalized: the two curryings of the but-phrase and the impossibility of an NP-modifier semantics, which is not derivable from every and no alone; the Cooper variable; the rhetorical reading of who but.

TODO

• The paper's footnote on both and neither presumes they "give rise to unique exception sets"; under the library's cardinality-asserting both a false both-quantification has no exception set at all, so which semantics the footnote intends is undetermined and neither claim is stated.

References

• [VF93]
• [KS86]
• [Hoe87]
• [Hor89]

Truth conditions (§1.1, §1.5)

theorem VonFintel1993.isExceptionSet_every_ident_iff {α : Type u_1} {A B : α → Prop} {j : α} : Quantifier.Exceptive.IsExceptionSet Quantifier.GQ.every A (Quantifier.NP.ident j) B ↔ A \ B = Quantifier.NP.ident j

Every student but John attended says that the students who did not attend are John alone, (9) of the paper and the reading of Examples.ex_1a.

theorem VonFintel1993.isExceptionSet_no_ident_iff {α : Type u_1} {A B : α → Prop} {j : α} : Quantifier.Exceptive.IsExceptionSet Quantifier.GQ.no A (Quantifier.NP.ident j) B ↔ A ⊓ B = Quantifier.NP.ident j

No student but John attended says that the students who attended are John alone, (9) of the paper and the reading of Examples.ex_2b.

Consequences of uniqueness (§1.5, §1.7)

theorem VonFintel1993.not_isExceptionSet_of_lt {α : Type u_1} {Q : Quantifier.GQ α} {A C B : α → Prop} (h : Quantifier.Exceptive.IsExceptionSet Q A C B) {C' : α → Prop} (hlt : C < C') : ¬Quantifier.Exceptive.IsExceptionSet Q A C' B

The inference to a but-phrase with a larger exception set (24), Examples.ex_14, is blocked.

theorem VonFintel1993.eq_of_isExceptionSet_ident {α : Type u_1} {Q : Quantifier.GQ α} {A B : α → Prop} {j m : α} (hj : Quantifier.Exceptive.IsExceptionSet Q A (Quantifier.NP.ident j) B) (hm : Quantifier.Exceptive.IsExceptionSet Q A (Quantifier.NP.ident m) B) : j = m

Two but-phrases on one quantifier (28), Examples.ex_28a, name the same exception.

The co-occurrence restrictions (§1.6)

def VonFintel1993.GuaranteesException {α : Type u_1} (Q : Quantifier.GQ α) : Prop

A determiner guarantees an exception set when every false quantification has one, the property von Fintel finds the universal determiners alone to have.

Equations

• VonFintel1993.GuaranteesException Q = ∀ (A B : α → Prop), ¬Q A B → ∃ (C : α → Prop), Quantifier.Exceptive.IsExceptionSet Q A C B

theorem VonFintel1993.guaranteesException_every {α : Type u_1} : GuaranteesException Quantifier.GQ.every

theorem VonFintel1993.guaranteesException_no {α : Type u_1} : GuaranteesException Quantifier.GQ.no

theorem VonFintel1993.not_guaranteesException_some {α : Type u_1} : ¬GuaranteesException Quantifier.GQ.some

Some guarantees no exception, since when nothing in the restrictor is in the scope no subtraction helps.

@[reducible, inline]

abbrev VonFintel1993.attended : Fin 5 → Prop

The five students of (25) are Tom, John, Harry, Bill and Mary in order; only the last two attended (Examples.ex_25a).

Equations

• VonFintel1993.attended x✝ = (3 ≤ x✝)

theorem VonFintel1993.not_isExceptionSet_most (C : Fin 5 → Prop) : ¬Quantifier.Exceptive.IsExceptionSet Quantifier.GQ.most ⊤ C attended

No set of students is the exception set of most students attended in situation (25) (Examples.ex_25b), since excluding any two of the three nonattenders makes it true, so only the empty set lies below every rescuer, and without any exclusion it is false.

theorem VonFintel1993.not_guaranteesException_most : ¬GuaranteesException Quantifier.GQ.most

theorem VonFintel1993.isExceptionSet_most_two : Quantifier.Exceptive.IsExceptionSet Quantifier.GQ.most ⊤ (fun (x : Fin 2) => x = 0) fun (x : Fin 2) => x = 1

In the paper's limiting case, with two students John and Harry of whom only Harry attended, most has the exception set John.

What but operates on (§1.8)

theorem VonFintel1993.not_exists_nounModifier {α : Type u_1} {C : α → Prop} (hC : C ≠ ⊥) : ¬∃ (f : (α → Prop) → α → Prop), ∀ (A B : α → Prop), Quantifier.GQ.every (f A) B ↔ Quantifier.Exceptive.IsExceptionSet Quantifier.GQ.every A C B

The but-phrase cannot be a noun modifier (§1.8). No operation on the restrictor alone yields the exception-set truth conditions with every, since with the whole domain as scope the modified quantification is true while a nonempty C is not the exception set.

Free exceptives (§2)

theorem VonFintel1993.restrictive_most : Quantifier.Exceptive.Restrictive Quantifier.GQ.most ⊤ (fun (x : Fin 5) => x = 0 ∨ x = 1) attended

In the situation of (25), except for Tom and John, most students attended holds where no but-phrase does, so the free exceptive occurs with most (34c).

theorem VonFintel1993.isExceptionSet_every_of_restrictive {α : Type u_1} {A C B : α → Prop} (h : Quantifier.Exceptive.Restrictive Quantifier.GQ.every A C B) (hC : C ≤ A \ B) : Quantifier.Exceptive.IsExceptionSet Quantifier.GQ.every A C B

With every the but reading is the pragmatic strengthening of the free exceptive to an exception set that contains only exceptions (§2.3).

theorem VonFintel1993.isExceptionSet_no_of_restrictive {α : Type u_1} {A C B : α → Prop} (h : Quantifier.Exceptive.Restrictive Quantifier.GQ.no A C B) (hC : C ≤ A ⊓ B) : Quantifier.Exceptive.IsExceptionSet Quantifier.GQ.no A C B

With no the but reading is likewise the strengthening of the free exceptive (§2.3).

The paper's examples

inductive VonFintel1993.Marker : Type

The paper opposes two exceptive markers, the but-phrase and free except for.

• but : Marker
• exceptFor : Marker

@[instance_reducible]

instance VonFintel1993.instDecidableEqMarker : DecidableEq Marker

Equations

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

def VonFintel1993.instReprMarker.repr : Marker → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• VonFintel1993.instReprMarker.repr VonFintel1993.Marker.but prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "VonFintel1993.Marker.but")).group prec✝

@[instance_reducible]

instance VonFintel1993.instReprMarker : Repr Marker

Equations

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

inductive VonFintel1993.Determiner : Type

These determiners of the paper's exceptive examples have a reading in the English fragment or the quantification substrate; any, the definite and besides's numeral have none.

• every : Determiner
• no : Determiner
• some : Determiner
• most : Determiner

@[instance_reducible]

instance VonFintel1993.instDecidableEqDeterminer : DecidableEq Determiner

Equations

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

def VonFintel1993.instReprDeterminer.repr : Determiner → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance VonFintel1993.instReprDeterminer : Repr Determiner

Equations

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

noncomputable def VonFintel1993.Determiner.readings : Determiner → Set Quantifier.GQ.Family

A determiner reads as the English fragment's denotations for the words the fragment has and as the quantification substrate's no for no.

Equations

• VonFintel1993.Determiner.every.readings = Semantics.Denotes.denote English.Determiners.QuantityWord.every
• VonFintel1993.Determiner.no.readings = {Quantifier.GQ.Family.no}
• VonFintel1993.Determiner.some.readings = Semantics.Denotes.denote English.Determiners.QuantityWord.some_
• VonFintel1993.Determiner.most.readings = Semantics.Denotes.denote English.Determiners.QuantityWord.most

structure VonFintel1993.Row : Type

A row records an exceptive example of the paper by its marker, its determiner and its printed judgment.

• marker : Marker
• det : Determiner
• judgment : Judgment

@[instance_reducible]

instance VonFintel1993.instDecidableEqRow : DecidableEq Row

Equations

• VonFintel1993.instDecidableEqRow = VonFintel1993.instDecidableEqRow.decEq

def VonFintel1993.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

def VonFintel1993.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance VonFintel1993.instReprRow : Repr Row

Equations

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

def VonFintel1993.Row.ofDatum (ex : Datum) : Option Row

ofDatum reads the marker, the determiner and the judgment off an exceptive example with a tabled determiner.

Equations

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

def VonFintel1993.rows : List Row

rows collects the exceptive rows of the paper's examples.

Equations

• VonFintel1993.rows = List.filterMap VonFintel1993.Row.ofDatum VonFintel1993.Examples.all

theorem VonFintel1993.but_predicted (r : Row) : r ∈ rows → r.marker = Marker.but → (r.judgment = Judgment.acceptable ↔ ∀ q ∈ r.det.readings, ∀ (β : Type) [inst : Fintype β], GuaranteesException (q β))

In Horn's paradigm (10) and the but-sentences (1a), (2b), (22) and (25b), a but-phrase is acceptable with a determiner exactly when its readings guarantee an exception set on every finite domain, the semantic fact the paper takes the co-occurrence restriction to grammaticize.

theorem VonFintel1993.exceptFor_predicted (r : Row) : r ∈ rows → r.marker = Marker.exceptFor → (r.judgment = Judgment.acceptable ↔ ∀ q ∈ r.det.readings, ∃ (β : Type) (x : Fintype β) (A : β → Prop) (C : β → Prop) (B : β → Prop), Quantifier.Exceptive.Restrictive (q β) A C B)

The free exceptives of (1b), (33a), (34a) and (34c) are acceptable with every tabled determiner, each of which admits a restrictive exceptive on some finite domain, as the semantics without the uniqueness condition predicts.