Polyadic Quantifiers

@cite{peters-westerstahl-2006} @cite{hintikka-1996}

Three mechanisms for building polyadic (multi-sorted) quantifiers from monadic (type ⟨1,1⟩) ones:

1. Iteration: Q₁x Q₂y R(x,y) — nested quantification
2. Resumption: Qx R(x,x) — a single quantifier on the diagonal
3. Branching: Hintikka's partially ordered quantifiers

These capture the semantic content of multi-quantifier sentences at the model-theoretic level, complementing linglib's syntactic scope mechanisms in Semantics/Composition/Scope.lean and QuantifierComposition.lean.

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

Iteration: Q₁x Q₂y R(x,y). Nested quantification where Q₂ is in the scope of Q₁.

"Every student read some book" = iterate(every, student, some, book)(read) = every(student, λx. some(book, λy. read(x,y)))

@cite{peters-westerstahl-2006} Ch 10.

Equations

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

def Core.Quantification.Polyadic.resume {α : Type u_1} (Q : GQ α) (A : α → Prop) (R : α → α → Prop) : Prop

Resumption: one quantifier binding two argument positions.

"Most students like themselves" = resume(most, student)(like) = most(student, λx. like(x,x))

Resumption only accesses the diagonal of R. @cite{peters-westerstahl-2006} Ch 10.

Equations

• Core.Quantification.Polyadic.resume Q A R = Q A fun (x : α) => R x x

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

Branching (Hintikka) quantifier: Q₁ and Q₂ are evaluated independently (neither is in the scope of the other).

The Skolem-function characterization: there exist choice functions witnessing both quantifiers simultaneously.

"Some relative of each villager and some friend of each townsman hate each other" — the two quantifiers don't scope over each other.

Simplified Barwise (1979) version: branch(Q₁, A, Q₂, B)(R) ↔ ∃f g. Q₁(A, λx. R(x, f(x))) ∧ Q₂(B, λy. R(g(y), y))

@cite{hintikka-1996} @cite{peters-westerstahl-2006} Ch 10.

Equations

• Core.Quantification.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

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

Surface scope = iterate(Q₁, A, Q₂, B)(R). Inverse scope = iterate(Q₂, B, Q₁, A)(flip R). These are the two "linear" readings of a two-quantifier sentence. @cite{peters-westerstahl-2006} Ch 10.

Equations

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

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

Equations

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

theorem Core.Quantification.Polyadic.iterate_mono_in_R {α : Type u_1} (Q₁ Q₂ : GQ α) (A B : α → Prop) (R R' : α → α → Prop) (h₁ : ScopeUpwardMono Q₁) (h₂ : ScopeUpwardMono Q₂) (hR : ∀ (x y : α), R x y → R' x y) (hIt : iterate Q₁ Q₂ A B R) : iterate Q₁ Q₂ A B R'

Iteration preserves scope monotonicity: if both Q₁ and Q₂ are Mon↑, then iterate(Q₁, A, Q₂, B) is monotone in R (pointwise). @cite{peters-westerstahl-2006} Ch 10.

theorem Core.Quantification.Polyadic.resume_mono_in_R {α : Type u_1} (Q : GQ α) (A : α → Prop) (R R' : α → α → Prop) (hUp : ScopeUpwardMono Q) (hR : ∀ (x : α), R x x → R' x x) (hRes : resume Q A R) : resume Q A R'

Resumption preserves scope monotonicity.