Polyadic quantifiers

This file defines three ways of building a quantifier over binary relations from generalized quantifiers over sets. Iteration nests one quantifier in the scope of another, as in every student read some book. Resumption applies one quantifier to pairs, binding both argument places at once, as in the reading of men are usually taller than women that counts pairs of a man and a woman; since it evaluates the quantifier on the universe of pairs, it takes a quantifier given on every universe, a GQ.Family. Branching evaluates two quantifiers independently, neither in the scope of the other, as Hintikka proposed for some relative of each villager and some friend of each townsman hate each other. Peters and Westerståhl treat all three, and de Swart and Sag analyse negative concord as the resumption of no.

A sentence with two quantifiers has two linear scope readings, which are the two orders of iteration.

Main definitions

• Quantifier.Polyadic.iterate: the iteration Q₁x Q₂y R(x, y) of two quantifiers.
• Quantifier.Polyadic.resume: the binary resumption Q⟨x, y⟩ R(x, y) of a quantifier.
• Quantifier.Polyadic.branch: the branching of two quantifiers, witnessed by choice functions.
• Quantifier.Polyadic.surfaceScope, Quantifier.Polyadic.inverseScope: the two linear scope readings of a two-quantifier sentence.

Main results

• Quantifier.Polyadic.iterate_every_some_of_some_every: ∃∀ entails ∀∃, so the two linear readings of an every/some pair are nested.
• Quantifier.Polyadic.resume_no_iff, Quantifier.Polyadic.resume_no_iff_iterate_every_no: the resumption of no is the iteration of no and some, and of every and no.
• Quantifier.Polyadic.iterate_mono, Quantifier.Polyadic.resume_mono: iteration and resumption of scope-upward-monotone quantifiers are monotone in the relation.

TODO

branch states branching with a pair of choice functions. Barwise's formulation for upward-monotone quantifiers instead asks for sets X ⊆ A and Y ⊆ B with Q₁ A X, Q₂ B Y and X × Y ⊆ R; the two should be compared against the sources.

References

• [PW06]
• [Hin96]
• [dSS02]

Iteration and branching

def Quantifier.Polyadic.iterate {α : Type u} (Q₁ Q₂ : GQ α) (A B : α → Prop) (R : α → α → Prop) : Prop

The iteration Q₁x Q₂y R(x, y) nests Q₂ in the scope of Q₁, so that every student read some book is iterate every student some book read.

Equations

• Quantifier.Polyadic.iterate Q₁ Q₂ A B R = Q₁ A fun (x : α) => Q₂ B fun (y : α) => R x y

def Quantifier.Polyadic.branch {α : Type u} (Q₁ Q₂ : GQ α) (A B : α → Prop) (R : α → α → Prop) : Prop

The branching of Q₁ and Q₂ evaluates them independently, neither in the scope of the other. There are choice functions f and g such that Q₁ holds of the x related to their B-witness f x, and Q₂ of the y related to their A-witness g y.

Equations

• Quantifier.Polyadic.branch Q₁ Q₂ A B R = ∃ (f : α → α) (g : α → α), (Q₁ A fun (x : α) => B (f x) ∧ R x (f x)) ∧ Q₂ B fun (y : α) => A (g y) ∧ R (g y) y

theorem Quantifier.Polyadic.iterate_no_no_iff {α : Type u} {A B : α → Prop} {R : α → α → Prop} : iterate GQ.no GQ.no A B R ↔ iterate GQ.every GQ.some A B R

The iteration of no with no is the iteration of every with some, the two negations cancelling.

Resumption

def Quantifier.Polyadic.resume {α : Type u} [Fintype α] (Q : GQ.Family) (A B : α → Prop) (R : α → α → Prop) : Prop

The binary resumption Q⟨x, y⟩ R(x, y) evaluates Q on the universe of pairs, with the pairs in A × B as its restrictor and R as its scope. This is the resumption of Peters and Westerståhl with a product restrictor, de Swart and Sag's type ⟨1, 1, 2⟩.

Equations

• Quantifier.Polyadic.resume Q A B R = Q (α × α) (fun (p : α × α) => A p.1 ∧ B p.2) fun (p : α × α) => R p.1 p.2

theorem Quantifier.Polyadic.resume_some_iff {α : Type u} {A B : α → Prop} {R : α → α → Prop} [Fintype α] : resume GQ.Family.some A B R ↔ iterate GQ.some GQ.some A B R

theorem Quantifier.Polyadic.resume_every_iff {α : Type u} {A B : α → Prop} {R : α → α → Prop} [Fintype α] : resume GQ.Family.every A B R ↔ iterate GQ.every GQ.every A B R

theorem Quantifier.Polyadic.resume_no_iff {α : Type u} {A B : α → Prop} {R : α → α → Prop} [Fintype α] : resume GQ.Family.no A B R ↔ iterate GQ.no GQ.some A B R

The resumption of no is the iteration of no and some, so a negative chain read by resumption denies every pair.

theorem Quantifier.Polyadic.resume_no_iff_iterate_every_no {α : Type u} {A B : α → Prop} {R : α → α → Prop} [Fintype α] : resume GQ.Family.no A B R ↔ iterate GQ.every GQ.no A B R

The resumption of no is also the iteration of every and no.

theorem Quantifier.Polyadic.resume_mono {α : Type u} {A B : α → Prop} {R R' : α → α → Prop} [Fintype α] {Q : GQ.Family} (h : (Q (α × α)).ScopeMonotone) (hR : ∀ (x y : α), R x y → R' x y) : resume Q A B R → resume Q A B R'

The resumption of a quantifier that is scope-upward-monotone on pairs is monotone in the relation.

Scope order

def Quantifier.Polyadic.surfaceScope {α : Type u} (Q₁ Q₂ : GQ α) (A B : α → Prop) (R : α → α → Prop) : Prop

The surface-scope reading of a two-quantifier sentence, on which the first quantifier outscopes the second.

Equations

• Quantifier.Polyadic.surfaceScope Q₁ Q₂ A B R = Quantifier.Polyadic.iterate Q₁ Q₂ A B R

def Quantifier.Polyadic.inverseScope {α : Type u} (Q₁ Q₂ : GQ α) (A B : α → Prop) (R : α → α → Prop) : Prop

The inverse-scope reading of a two-quantifier sentence, on which the second quantifier outscopes the first.

Equations

• Quantifier.Polyadic.inverseScope Q₁ Q₂ A B R = Quantifier.Polyadic.iterate Q₂ Q₁ B A fun (y x : α) => R x y

theorem Quantifier.Polyadic.iterate_every_some_of_some_every {α : Type u} (A B : α → Prop) (R : α → α → Prop) (h : iterate GQ.some GQ.every A B R) : iterate GQ.every GQ.some B A (flip R)

An existential scoping over a universal entails the universal scoping over the existential, so the two linear readings of an every/some pair are nested.

Monotonicity

theorem Quantifier.Polyadic.iterate_mono {α : Type u} {Q₁ Q₂ : GQ α} {A B : α → Prop} {R R' : α → α → Prop} (h₁ : Q₁.ScopeMonotone) (h₂ : Q₂.ScopeMonotone) (hR : ∀ (x y : α), R x y → R' x y) : iterate Q₁ Q₂ A B R → iterate Q₁ Q₂ A B R'

The iteration of two scope-upward-monotone quantifiers is monotone in the relation.