Number-Tree Quantifiers

@cite{van-benthem-1984} @cite{van-benthem-1986}

The number-tree representation of conservative, quantity-invariant GQs. Under CONSERV + QUANT, a quantifier's truth value depends only on a = |A ∩ B| and b = |A \ B|, yielding a function ℕ → ℕ → Bool.

Includes impossibility theorems (§10), the Square of Opposition uniqueness theorem (§10e), the GQ→NumberTreeGQ bridge (§10f), and counting quantifiers (§11).

@[reducible, inline]

abbrev Core.Quantification.NumberTreeGQ : Type

Number-tree representation of a conservative, quantity-invariant GQ. Under CONSERV + QUANT, a quantifier's truth value depends only on a = |A ∩ B| and b = |A \ B| (§2, "tree of numbers"). This is inherently cross-domain: any (a, b) pair is realizable in some universe of size ≥ a + b.

Equations

• Core.Quantification.NumberTreeGQ = (ℕ → ℕ → Bool)

def Core.Quantification.NumberTreeGQ.Variety (q : NumberTreeGQ) : Prop

Variety for number-tree quantifiers: Q is non-trivial.

Equations

• q.Variety = ((∃ (a : ℕ) (b : ℕ), q a b = true) ∧ ∃ (a : ℕ) (b : ℕ), q a b = false)

theorem Core.Quantification.NumberTreeGQ.no_asymmetric (q : NumberTreeGQ) (hVar : q.Variety) (hAsym : ∀ (a b c : ℕ), q a b = true → q a c = false) : False

Thm 3.2.1: No asymmetric CONSERV+QUANT quantifiers exist.

On the number tree, asymmetry means: for all a b c, q(a, b) → ¬q(a, c) — because |A ∩ B| = a and |B \ A| = c is free (any c is realizable in a large enough universe).

Proof: Set c = b. Then q(a, b) → ¬q(a, b), so q is identically false. Contradicts Variety.

theorem Core.Quantification.NumberTreeGQ.no_strict_partial_order (q : NumberTreeGQ) (hVar : q.Variety) (hIrrefl : ∀ (n : ℕ), q n 0 = false) (hTrans : ∀ (a b c : ℕ), q a b = true → q a c = true → q (a + b) 0 = true) : False

§3.2 consequence: No strict partial order quantifiers.

On the number tree, irreflexivity is ∀ n, q(n, 0) = false (since Q(A,A) has |A ∩ A| = n, |A \ A| = 0). Transitivity (with C = A in the 3-set diagram) gives: q(a, b) ∧ q(a, c) → q(a+b, 0).

Proof: From transitivity, q(a, b) → q(a, c) → q(a+b, 0). From irreflexivity, q(a+b, 0) = false. So q(a, b) → q(a, c) = false — number-tree asymmetry. Apply no_asymmetric.

theorem Core.Quantification.NumberTreeGQ.no_euclidean (q : NumberTreeGQ) (hVar : q.Variety) (hEuc : ∀ (p q_ r s t u : ℕ), q (p + q_) (r + s) = true → q (p + r) (q_ + s) = true → q (p + t) (q_ + u) = true) : False

Thm 3.2.3: No Euclidean CONSERV+QUANT quantifiers exist.

On the number tree (3-set Venn diagram with 7 free size parameters p, q, r, s, t, u plus one more), the Euclidean property becomes: q(p+q_, r+s) ∧ q(p+r, q_+s) → q(p+t, q_+u) for all p q_ r s t u.

Proof (4 steps):

1. From Variety witness q(α, β) = true, set p=α, q_=0, r=0, s=β: q(α+t, u) for all t, u. So q(a, b) = true for a ≥ α.
2. If α = 0, step 1 gives q ≡ true, contradicting Variety. If α > 0: pair q(α, 2α) and q(2α, α) (both from step 1) with p=0, q_=α, r=2α, s=0: get q(t, α+u) for all t, u. Combined: q(a, b) = true when a ≥ α or b ≥ α.
3. q(0, α) (from step 2) and q(α, 0) (from step 1) with p=0, q_=0, r=α, s=0: get q(t, u) for all t, u.
4. Contradicts Variety.

def Core.Quantification.NumberTreeGQ.allNT : NumberTreeGQ

"all" on the number tree: Q(A,B) iff A ⊆ B iff |A\B| = 0.

Equations

• Core.Quantification.NumberTreeGQ.allNT x✝ b = (b == 0)

def Core.Quantification.NumberTreeGQ.someNT : NumberTreeGQ

"some" on the number tree: Q(A,B) iff A∩B ≠ ∅ iff |A∩B| ≥ 1.

Equations

• Core.Quantification.NumberTreeGQ.someNT a x✝ = decide (a ≥ 1)

def Core.Quantification.NumberTreeGQ.noNT : NumberTreeGQ

"no" on the number tree: Q(A,B) iff A∩B = ∅ iff |A∩B| = 0.

Equations

• Core.Quantification.NumberTreeGQ.noNT a x✝ = (a == 0)

def Core.Quantification.NumberTreeGQ.notAllNT : NumberTreeGQ

"not all" on the number tree: Q(A,B) iff A ⊄ B iff |A\B| ≥ 1.

Equations

• Core.Quantification.NumberTreeGQ.notAllNT x✝ b = decide (b ≥ 1)

def Core.Quantification.NumberTreeGQ.Additive (q : NumberTreeGQ) : Prop

Additive: (a,b) ∈ Q and (a',b') ∈ Q implies (a+a', b+b') ∈ Q. p.460: all, some, no, not all are additive. Additivity means Q's truth set is closed under componentwise addition in the number tree.

Equations

• q.Additive = ∀ (a b a' b' : ℕ), q a b = true → q a' b' = true → q (a + a') (b + b') = true

theorem Core.Quantification.NumberTreeGQ.allNT_additive : allNT.Additive

theorem Core.Quantification.NumberTreeGQ.someNT_additive : someNT.Additive

theorem Core.Quantification.NumberTreeGQ.noNT_additive : noNT.Additive

theorem Core.Quantification.NumberTreeGQ.notAllNT_additive : notAllNT.Additive

def Core.Quantification.NumberTreeGQ.RightCont (q : NumberTreeGQ) : Prop

Right continuity on the number tree (CONT): on each diagonal a+b = n, the true points form a contiguous interval. §4.3: all right-monotone quantifiers are continuous. "precisely one" is continuous but non-monotone.

Equations

• q.RightCont = ∀ (n a₁ a₂ a : ℕ), a₁ ≤ a → a ≤ a₂ → a₂ ≤ n → q a₁ (n - a₁) = true → q a₂ (n - a₂) = true → q a (n - a) = true

def Core.Quantification.NumberTreeGQ.LeftCont (q : NumberTreeGQ) : Prop

Left continuity on the number tree: on each diagonal, the false points (absence) also form a contiguous interval. §4.3: equivalent to right continuity of ¬Q.

Equations

• q.LeftCont = ∀ (n a₁ a₂ a : ℕ), a₁ ≤ a → a ≤ a₂ → a₂ ≤ n → q a₁ (n - a₁) = false → q a₂ (n - a₂) = false → q a (n - a) = false

def Core.Quantification.NumberTreeGQ.Plus (q : NumberTreeGQ) : Prop

PLUS (§7): adding one individual to the situation cannot create a "dead end." Both presence and absence must be extensible in at least one direction.

• For + positions: q(a+1,b) or q(a,b+1) is true.
• For − positions: q(a+1,b) or q(a,b+1) is false.

Equations

• q.Plus = ((∀ (a b : ℕ), q a b = true → q (a + 1) b = true ∨ q a (b + 1) = true) ∧ ∀ (a b : ℕ), q a b = false → q (a + 1) b = false ∨ q a (b + 1) = false)

def Core.Quantification.NumberTreeGQ.Uniform (q : NumberTreeGQ) : Prop

UNIF (§7): the addition experiment (a,b) → (a+1,b) and (a,b) → (a,b+1) always yields the same pattern for positions of the same truth value. The experiment result depends only on whether Q holds, not on where in the tree we are.

Equations

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

theorem Core.Quantification.NumberTreeGQ.allNT_rightCont : allNT.RightCont

theorem Core.Quantification.NumberTreeGQ.someNT_rightCont : someNT.RightCont

theorem Core.Quantification.NumberTreeGQ.noNT_rightCont : noNT.RightCont

theorem Core.Quantification.NumberTreeGQ.notAllNT_rightCont : notAllNT.RightCont

theorem Core.Quantification.NumberTreeGQ.allNT_plus : allNT.Plus

theorem Core.Quantification.NumberTreeGQ.someNT_plus : someNT.Plus

theorem Core.Quantification.NumberTreeGQ.noNT_plus : noNT.Plus

theorem Core.Quantification.NumberTreeGQ.notAllNT_plus : notAllNT.Plus

theorem Core.Quantification.NumberTreeGQ.allNT_uniform : allNT.Uniform

theorem Core.Quantification.NumberTreeGQ.someNT_uniform : someNT.Uniform

theorem Core.Quantification.NumberTreeGQ.noNT_uniform : noNT.Uniform

theorem Core.Quantification.NumberTreeGQ.notAllNT_uniform : notAllNT.Uniform

structure Core.Quantification.NumberTreeGQ.SixPostulates (q : NumberTreeGQ) : Prop

The six postulates that §7 uses to characterize the Square of Opposition.

• variety : q.Variety
• cont : q.RightCont
• lcont : q.LeftCont
• plus : q.Plus
• uniform : q.Uniform

theorem Core.Quantification.NumberTreeGQ.square_uniqueness (q : NumberTreeGQ) (h : q.SixPostulates) : q = allNT ∨ q = someNT ∨ q = noNT ∨ q = notAllNT

@cite{van-benthem-1986} Thm 7.1: On the finite sets, the only CONSERV+QUANT quantifiers satisfying VAR, CONT, PLUS, and UNIF are precisely the four corners of the logical Square of Opposition: all, some, no, and not all.

Proof strategy: UNIF reduces every cell's truth value to four experiment booleans (tr, tu, fr, fu). PLUS eliminates 12 of the 16 combinations; CONT and VAR eliminate 2 more (via path inconsistencies). The 4 survivors each determine exactly one quantifier, proved via grid_ext.

noncomputable def Core.Quantification.toNumberTree {α : Type u_1} [Fintype α] (q : GQ α) : NumberTreeGQ

Extract the number-tree representation of a CONSERV+QUANT quantifier. Under conservativity and quantity-invariance, Q(A,B) depends only on |A ∩ B| and |A \ B|. This definition picks a canonical witness pair for each (a,b) coordinate.

For (a,b) realizable in the domain (a + b ≤ |α|), the value is determined by any witness; for unrealizable pairs, we default to false.

Equations

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

theorem Core.Quantification.toNumberTree_spec {α : Type u_1} [Fintype α] [DecidableEq α] (q : GQ α) (hCons : Conservative q) (hQ : QuantityInvariant q) (A B : α → Bool) : q A B = toNumberTree q {x : α | (A x && B x) = true}.card {x : α | (A x && !B x) = true}.card

The number-tree representation faithfully reflects the GQ on realizable coordinates: for any A, B, the GQ's truth value equals the number-tree value at (|A∩B|, |A\B|).

Proof: A and B themselves witness the existential in toNumberTree, so the dite takes the positive branch. The chosen witness pair has matching |A∩B| and |A\B| cardinalities, so gq_depends_on_card (via cell-preserving bijection) gives q A B = q A_chosen B_chosen.

def Core.Quantification.conservativeQuantifierCount (n : ℕ) : ℕ

Thm 5.4: On a finite set with n individuals, there are exactly 2^((n+1)(n+2)/2) conservative quantifiers (satisfying QUANT). The tree of numbers has (n+1)(n+2)/2 points at levels a + b ≤ n.

Equations

• Core.Quantification.conservativeQuantifierCount n = 2 ^ ((n + 1) * (n + 2) / 2)