The reading of an indeterminate quantifier

An indeterminate quantifier applies its particle's coordination to the values its scope takes on the restrictor, as Kratzer and Shimoyama propose for Japanese. A disjunctive particle takes the supremum, so the quantifier is Quantifier.GQ.some; a conjunctive particle takes the infimum, every; and a negative particle the complement of the supremum, no.

Main definitions

• IndeterminateQuantifier.reading: the particle's coordination over the restrictor.

Main statements

• IndeterminateQuantifier.reading_of_disjunctive, IndeterminateQuantifier.reading_of_conjunctive, IndeterminateQuantifier.reading_of_negative: the readings are some, every and no.

References

• [KS17]
• [Shi06]

def IndeterminateQuantifier.reading (q : IndeterminateQuantifier) : Quantifier.GQ.Family

The reading of an indeterminate quantifier applies its particle's coordination to the values the scope takes on the restrictor.

Equations

• q.reading x✝¹ R S = q.particle.denote (S '' {x : x✝¹ | R x})

@[instance_reducible]

instance IndeterminateQuantifier.instDenotesSetFamily : Semantics.Denotes IndeterminateQuantifier (Set Quantifier.GQ.Family)

An indeterminate quantifier denotes its reading.

Equations

• IndeterminateQuantifier.instDenotesSetFamily = { denote := fun (q : IndeterminateQuantifier) => {q.reading} }

theorem IndeterminateQuantifier.reading_of_disjunctive {q : IndeterminateQuantifier} (h : q.particle.role = Coordinator.Role.disjunctive) : q.reading = Quantifier.GQ.Family.some

Under a disjunctive particle the reading is Quantifier.GQ.some.

theorem IndeterminateQuantifier.reading_of_conjunctive {q : IndeterminateQuantifier} (h : q.particle.role = Coordinator.Role.conjunctive) : q.reading = Quantifier.GQ.Family.every

Under a conjunctive particle the reading is every.

theorem IndeterminateQuantifier.reading_of_negative {q : IndeterminateQuantifier} (h : q.particle.role = Coordinator.Role.negative) : q.reading = Quantifier.GQ.Family.no

Under a negative particle the reading is no.