The tree of numbers

This file defines quantifiers on van Benthem's tree of numbers. A conservative quantifier that is invariant under permutations of the universe holds of finite sets A and B according to the two numbers a = |A \ B| and b = |A ∩ B| alone, so it is a set of points (a, b). The points with a + b = n form the n-th row of the tree, the ways of splitting an n-element A.

On this representation inner negation, which negates the scope, swaps the two coordinates, and outer negation is the complement. The four corners of the square of opposition are all, some, no and not all, and the two negations carry each corner to its neighbours.

Van Benthem's postulates of variety, continuity, absence of deadlock and uniformity are each invariant under both negations. That symmetry carries the verification of the postulates, and the proof that the corners are the only quantifiers satisfying them, from all to the other three.

Main definitions

• Quantifier.NumberTree: a quantifier as a relation between |A \ B| and |A ∩ B|.
• Quantifier.NumberTree.innerNeg: inner negation, the swap of the two coordinates.
• Quantifier.NumberTree.all, Quantifier.NumberTree.some, Quantifier.NumberTree.no, Quantifier.NumberTree.notAll: the corners of the square of opposition.
• Quantifier.NumberTree.cardinal: the quantifiers that depend on |A ∩ B| alone.
• Quantifier.NumberTree.row: the points of a row at which a quantifier holds.
• Quantifier.NumberTree.ScopeMonotone, Quantifier.NumberTree.ScopeAntitone: monotonicity in the scope, a step along a row of the tree.
• Quantifier.NumberTree.Asymmetric, Quantifier.NumberTree.StronglyConnected, Quantifier.NumberTree.Euclidean: relational conditions on a quantifier, read off the tree.
• Quantifier.NumberTree.Variety, Quantifier.NumberTree.Cont, Quantifier.NumberTree.Plus, Quantifier.NumberTree.Uniform: the postulates VAR, CONT, PLUS and UNIF.
• Quantifier.NumberTree.ofSizes: the tree of a relation between |A ∩ B| and |A|.
• Quantifier.NumberTree.ofGQ, Quantifier.NumberTree.toGQ: the tree of a generalized quantifier over a finite universe, and the quantifier of a tree, counting with Set.ncard.
• Quantifier.NumberTree.ConstantOnRow, Quantifier.NumberTree.ConstantBelow: a quantifier that does not depend on its scope for a restrictor of a given size, or on either argument on a universe of a given size.

Main results

• Quantifier.NumberTree.Asymmetric.eq_bot, Quantifier.NumberTree.StronglyConnected.eq_top, Quantifier.NumberTree.Euclidean.eq_top: the only asymmetric quantifier is the empty one, the only strongly connected one is the universal one, and a nonempty Euclidean quantifier is universal.
• Quantifier.NumberTree.variety_cont_plus_uniform_iff: the quantifiers satisfying the four postulates are exactly the four corners of the square of opposition.
• Quantifier.NumberTree.ofGQ_iff: a conservative, permutation-invariant generalized quantifier holds of A and B exactly when its tree holds of |A \ B| and |A ∩ B|.
• Quantifier.NumberTree.conservative_toGQ, Quantifier.NumberTree.quantityInvariant_toGQ: the quantifier of a tree is conservative and permutation invariant.
• Quantifier.NumberTree.ScopeMonotone.toGQ, Quantifier.NumberTree.ScopeAntitone.toGQ: the quantifier of a scope-monotone tree is scope monotone, and likewise antitone.
• Quantifier.NumberTree.dependsOn_toGQ_compl_singleton_iff: the quantifier of a tree depends on whether an individual is in its scope iff the individual is in its restrictor and the tree is not constant on the restrictor's row.
• Quantifier.NumberTree.card_powerset_points: there are 2 ^ ((n + 1) * (n + 2) / 2) sets of points in rows 0 to n, the number of conservative, permutation-invariant quantifiers on a universe of n individuals.

Implementation notes

Variety asks only that the quantifier hold somewhere and fail somewhere. Van Benthem's VAR is stronger in both of its versions, so results assuming Variety apply under VAR. The paper asks for a presence and an absence among the points (0, 0), (1, 0) and (0, 1), and the book's chapter on quantifiers, which restates the tree and the postulates, asks for both in every row below the top.

Continuity, absence of deadlock and uniformity each treat presence and absence of the quantifier alike. Each is stated as a condition on presence (RowConvex, NoDeadlock, Homogeneous) that is imposed on the quantifier and on its complement.

References

• [vB84]
• [vB86]

@[reducible, inline]

abbrev Quantifier.NumberTree : Type

A quantifier on the tree of numbers is a relation between a = |A \ B| and b = |A ∩ B|.

Equations

• Quantifier.NumberTree = (ℕ → ℕ → Prop)

theorem Quantifier.NumberTree.compl_apply {q : NumberTree} {a b : ℕ} : qᶜ a b ↔ ¬q a b

Negations and the square of opposition

def Quantifier.NumberTree.innerNeg (q : NumberTree) : NumberTree

Inner negation negates the scope, which swaps A \ B with A ∩ B.

Equations

• q.innerNeg a b = q b a

@[simp]

theorem Quantifier.NumberTree.innerNeg_apply {q : NumberTree} {a b : ℕ} : q.innerNeg a b ↔ q b a

@[simp]

theorem Quantifier.NumberTree.innerNeg_innerNeg (q : NumberTree) : q.innerNeg.innerNeg = q

theorem Quantifier.NumberTree.innerNeg_compl (q : NumberTree) : qᶜ.innerNeg = q.innerNegᶜ

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatInnerNeg {q : NumberTree} [DecidableRel q] : DecidableRel q.innerNeg

Equations

• Quantifier.NumberTree.instDecidableRelNatInnerNeg a b = Quantifier.NumberTree.instDecidableRelNatInnerNeg._aux_1 a b

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatComplForallForallProp {q : NumberTree} [DecidableRel q] : DecidableRel qᶜ

Equations

• Quantifier.NumberTree.instDecidableRelNatComplForallForallProp a b = { decide := !decide (q a b), reflects_decide := ⋯ }

def Quantifier.NumberTree.all : NumberTree

The quantifier all holds when nothing in A lies outside B.

Equations

• Quantifier.NumberTree.all a x✝ = (a = 0)

def Quantifier.NumberTree.some : NumberTree

The quantifier some holds when something in A lies in B.

Equations

• Quantifier.NumberTree.some x✝ b = (b ≠ 0)

def Quantifier.NumberTree.no : NumberTree

The quantifier no holds when nothing in A lies in B.

Equations

• Quantifier.NumberTree.no x✝ b = (b = 0)

def Quantifier.NumberTree.notAll : NumberTree

The quantifier not all holds when something in A lies outside B.

Equations

• Quantifier.NumberTree.notAll a x✝ = (a ≠ 0)

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatAll : DecidableRel NumberTree.all

Equations

• Quantifier.NumberTree.instDecidableRelNatAll a x✝ = { decide := a.beq 0, reflects_decide := ⋯ }

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatSome : DecidableRel NumberTree.some

Equations

• Quantifier.NumberTree.instDecidableRelNatSome x✝ b = { decide := !decide (b = 0), reflects_decide := ⋯ }

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatNo : DecidableRel NumberTree.no

Equations

• Quantifier.NumberTree.instDecidableRelNatNo x✝ b = { decide := b.beq 0, reflects_decide := ⋯ }

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatNotAll : DecidableRel NumberTree.notAll

Equations

• Quantifier.NumberTree.instDecidableRelNatNotAll a x✝ = { decide := !decide (a = 0), reflects_decide := ⋯ }

theorem Quantifier.NumberTree.innerNeg_all : NumberTree.all.innerNeg = NumberTree.no

theorem Quantifier.NumberTree.innerNeg_some : NumberTree.some.innerNeg = NumberTree.notAll

theorem Quantifier.NumberTree.compl_all : NumberTree.allᶜ = NumberTree.notAll

theorem Quantifier.NumberTree.compl_no : NumberTree.noᶜ = NumberTree.some

def Quantifier.NumberTree.cardinal (s : Set ℕ) : NumberTree

A cardinal quantifier holds according to |A ∩ B| alone, as the numerals do.

Equations

• Quantifier.NumberTree.cardinal s x✝ b = (b ∈ s)

@[simp]

theorem Quantifier.NumberTree.cardinal_apply {a b : ℕ} {s : Set ℕ} : cardinal s a b ↔ b ∈ s

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatCardinalOfDecidablePredMemSet {s : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ s] : DecidableRel (cardinal s)

Equations

• Quantifier.NumberTree.instDecidableRelNatCardinalOfDecidablePredMemSet x✝ b = Quantifier.NumberTree.instDecidableRelNatCardinalOfDecidablePredMemSet._aux_1 x✝ b

theorem Quantifier.NumberTree.cardinal_singleton_zero : cardinal {0} = NumberTree.no

def Quantifier.NumberTree.ofSizes (c : ℕ → ℕ → Prop) : NumberTree

The tree of a relation c between |A ∩ B| and |A| holds at (a, b) when c relates b to a + b, the form in which proportions of the restrictor are stated.

Equations

• Quantifier.NumberTree.ofSizes c a b = c b (a + b)

@[simp]

theorem Quantifier.NumberTree.ofSizes_apply {a b : ℕ} {c : ℕ → ℕ → Prop} : ofSizes c a b ↔ c b (a + b)

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatOfSizes {c : ℕ → ℕ → Prop} [DecidableRel c] : DecidableRel (ofSizes c)

Equations

• Quantifier.NumberTree.instDecidableRelNatOfSizes a b = Quantifier.NumberTree.instDecidableRelNatOfSizes._aux_1 a b

Rows

Row n of the tree lists the ways of splitting n members of A between B and its complement. A point of the row is given by the number of members inside B.

def Quantifier.NumberTree.row (q : NumberTree) [DecidableRel q] (n : ℕ) : Finset (Fin (n + 1))

The points of row n at which a quantifier holds, each given by |A ∩ B|.

Equations

• q.row n = {b : Fin (n + 1) | q (n - ↑b) ↑b}

@[simp]

theorem Quantifier.NumberTree.mem_row {q : NumberTree} [DecidableRel q] {n : ℕ} {b : Fin (n + 1)} : b ∈ q.row n ↔ q (n - ↑b) ↑b

Scope monotonicity

Enlarging the scope B by an element of A moves one individual from A \ B to A ∩ B, a step to the right along a row of the tree.

def Quantifier.NumberTree.ScopeMonotone (q : NumberTree) : Prop

A quantifier is scope monotone when a step right along a row preserves truth.

Equations

• q.ScopeMonotone = ∀ (a b : ℕ), q (a + 1) b → q a (b + 1)

def Quantifier.NumberTree.ScopeAntitone (q : NumberTree) : Prop

A quantifier is scope antitone when a step left along a row preserves truth.

Equations

• q.ScopeAntitone = ∀ (a b : ℕ), q a (b + 1) → q (a + 1) b

theorem Quantifier.NumberTree.ScopeMonotone.compl {q : NumberTree} (h : q.ScopeMonotone) : qᶜ.ScopeAntitone

theorem Quantifier.NumberTree.ScopeAntitone.compl {q : NumberTree} (h : q.ScopeAntitone) : qᶜ.ScopeMonotone

theorem Quantifier.NumberTree.ScopeMonotone.innerNeg {q : NumberTree} (h : q.ScopeMonotone) : q.innerNeg.ScopeAntitone

theorem Quantifier.NumberTree.ScopeAntitone.innerNeg {q : NumberTree} (h : q.ScopeAntitone) : q.innerNeg.ScopeMonotone

theorem Quantifier.NumberTree.ScopeMonotone.shift {q : NumberTree} (h : q.ScopeMonotone) (k : ℕ) {a b : ℕ} (hq : q (a + k) b) : q a (b + k)

Iterated, a scope-monotone quantifier survives moving k individuals into the scope.

theorem Quantifier.NumberTree.scopeMonotone_ofSizes {c : ℕ → ℕ → Prop} (hc : ∀ (p : ℕ), Monotone fun (x : ℕ) => c x p) : (ofSizes c).ScopeMonotone

A relation closed upwards in |A ∩ B| is scope monotone on the tree.

theorem Quantifier.NumberTree.scopeAntitone_ofSizes {c : ℕ → ℕ → Prop} (hc : ∀ (p : ℕ), Antitone fun (x : ℕ) => c x p) : (ofSizes c).ScopeAntitone

A relation closed downwards in |A ∩ B| is scope antitone on the tree.

theorem Quantifier.NumberTree.scopeMonotone_all : NumberTree.all.ScopeMonotone

theorem Quantifier.NumberTree.scopeAntitone_no : NumberTree.no.ScopeAntitone

theorem Quantifier.NumberTree.scopeMonotone_some : NumberTree.some.ScopeMonotone

theorem Quantifier.NumberTree.scopeAntitone_notAll : NumberTree.notAll.ScopeAntitone

Relational conditions

A condition on the relation Q A B between sets becomes a condition on the tree once the sets are replaced by the sizes of the cells of their Venn diagram.

def Quantifier.NumberTree.Asymmetric (q : NumberTree) : Prop

A quantifier is asymmetric when Q A B excludes Q B A. The two share |A ∩ B|, and |A \ B| and |B \ A| are arbitrary.

Equations

• q.Asymmetric = ∀ (a b c : ℕ), q a c → ¬q b c

def Quantifier.NumberTree.StronglyConnected (q : NumberTree) : Prop

A quantifier is strongly connected when Q A B or Q B A holds of any two sets.

Equations

• q.StronglyConnected = ∀ (a b c : ℕ), q a c ∨ q b c

def Quantifier.NumberTree.Irreflexive (q : NumberTree) : Prop

A quantifier is irreflexive when Q A A never holds.

Equations

• q.Irreflexive = ∀ (n : ℕ), ¬q 0 n

def Quantifier.NumberTree.Euclidean (q : NumberTree) : Prop

A quantifier is Euclidean when Q X Y and Q X Z give Q Y Z. Among the cells of the Venn diagram of X, Y and Z, p counts X ∩ Y ∩ Z, x the rest of X ∩ Y, y the rest of X ∩ Z, s the rest of X, t the rest of Y ∩ Z, and u the rest of Y.

Equations

• q.Euclidean = ∀ (p x y s t u : ℕ), q (y + s) (p + x) → q (x + s) (p + y) → q (x + u) (p + t)

theorem Quantifier.NumberTree.Asymmetric.eq_bot {q : NumberTree} (h : q.Asymmetric) : q = ⊥

The only asymmetric quantifier is the empty one.

theorem Quantifier.NumberTree.StronglyConnected.eq_top {q : NumberTree} (h : q.StronglyConnected) : q = ⊤

The only strongly connected quantifier is the universal one.

theorem Quantifier.NumberTree.Irreflexive.asymmetric {q : NumberTree} (hI : q.Irreflexive) (hT : ∀ (a b c : ℕ), q a c → q b c → q 0 (a + c)) : q.Asymmetric

An irreflexive quantifier for which Q A B and Q B A give Q A A, as transitivity requires, is asymmetric. So there is no strict partial order among the nonempty quantifiers.

theorem Quantifier.NumberTree.Euclidean.eq_top {q : NumberTree} (h : q.Euclidean) (hq : ∃ (a : ℕ) (b : ℕ), q a b) : q = ⊤

A nonempty Euclidean quantifier is universal.

The postulates

def Quantifier.NumberTree.Variety (q : NumberTree) : Prop

A quantifier has variety when it holds somewhere and fails somewhere.

Equations

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

def Quantifier.NumberTree.RowConvex (q : NumberTree) : Prop

A quantifier is row-convex when it meets each row of the tree in an uninterrupted stretch.

Equations

• q.RowConvex = ∀ ⦃a₁ b₁ a b a₂ b₂ : ℕ⦄, a₁ + b₁ = a + b → a₂ + b₂ = a + b → a₁ ≤ a → a ≤ a₂ → q a₁ b₁ → q a₂ b₂ → q a b

def Quantifier.NumberTree.Cont (q : NumberTree) : Prop

The postulate CONT asks that both the presence and the absence of the quantifier be uninterrupted along each row.

Equations

• q.Cont = (q.RowConvex ∧ qᶜ.RowConvex)

def Quantifier.NumberTree.NoDeadlock (q : NumberTree) : Prop

A quantifier has no deadlock when adding an individual to A can always keep it true.

Equations

• q.NoDeadlock = ∀ ⦃a b : ℕ⦄, q a b → q (a + 1) b ∨ q a (b + 1)

def Quantifier.NumberTree.Plus (q : NumberTree) : Prop

The postulate PLUS asks that neither the truth nor the falsity of the quantifier reach a deadlock.

Equations

• q.Plus = (q.NoDeadlock ∧ qᶜ.NoDeadlock)

def Quantifier.NumberTree.Homogeneous (q : NumberTree) : Prop

A quantifier is homogeneous when adding an individual to A has the same two outcomes wherever the quantifier holds.

Equations

• q.Homogeneous = ∀ ⦃a₁ b₁ a₂ b₂ : ℕ⦄, q a₁ b₁ → q a₂ b₂ → (q (a₁ + 1) b₁ ↔ q (a₂ + 1) b₂) ∧ (q a₁ (b₁ + 1) ↔ q a₂ (b₂ + 1))

def Quantifier.NumberTree.Uniform (q : NumberTree) : Prop

The postulate UNIF asks that adding an individual have the same outcomes wherever the quantifier holds, and the same outcomes wherever it fails.

Equations

• q.Uniform = (q.Homogeneous ∧ qᶜ.Homogeneous)

theorem Quantifier.NumberTree.Variety.compl {q : NumberTree} (h : q.Variety) : qᶜ.Variety

theorem Quantifier.NumberTree.Cont.compl {q : NumberTree} (h : q.Cont) : qᶜ.Cont

theorem Quantifier.NumberTree.Plus.compl {q : NumberTree} (h : q.Plus) : qᶜ.Plus

theorem Quantifier.NumberTree.Uniform.compl {q : NumberTree} (h : q.Uniform) : qᶜ.Uniform

theorem Quantifier.NumberTree.Variety.innerNeg {q : NumberTree} (h : q.Variety) : q.innerNeg.Variety

theorem Quantifier.NumberTree.RowConvex.innerNeg {q : NumberTree} (h : q.RowConvex) : q.innerNeg.RowConvex

theorem Quantifier.NumberTree.NoDeadlock.innerNeg {q : NumberTree} (h : q.NoDeadlock) : q.innerNeg.NoDeadlock

theorem Quantifier.NumberTree.Homogeneous.innerNeg {q : NumberTree} (h : q.Homogeneous) : q.innerNeg.Homogeneous

theorem Quantifier.NumberTree.Cont.innerNeg {q : NumberTree} (h : q.Cont) : q.innerNeg.Cont

theorem Quantifier.NumberTree.Plus.innerNeg {q : NumberTree} (h : q.Plus) : q.innerNeg.Plus

theorem Quantifier.NumberTree.Uniform.innerNeg {q : NumberTree} (h : q.Uniform) : q.innerNeg.Uniform

The square of opposition

The four corners are the only quantifiers with variety that satisfy CONT, PLUS and UNIF.

theorem Quantifier.NumberTree.variety_all : NumberTree.all.Variety

theorem Quantifier.NumberTree.cont_all : NumberTree.all.Cont

theorem Quantifier.NumberTree.plus_all : NumberTree.all.Plus

theorem Quantifier.NumberTree.uniform_all : NumberTree.all.Uniform

theorem Quantifier.NumberTree.variety_cont_plus_uniform_iff {q : NumberTree} : q.Variety ∧ q.Cont ∧ q.Plus ∧ q.Uniform ↔ q = NumberTree.all ∨ q = NumberTree.some ∨ q = NumberTree.no ∨ q = NumberTree.notAll

The quantifiers with variety that satisfy CONT, PLUS and UNIF are exactly all, some, no and not all.

theorem Quantifier.NumberTree.not_uniform_two_le : ¬Uniform fun (x b : ℕ) => 2 ≤ b

The quantifier at least two is not uniform. Adding an individual to A ∩ B leaves it false at (0, 0) and makes it true at (0, 1).

Additivity

def Quantifier.NumberTree.Additive (q : NumberTree) : Prop

A quantifier is additive when its points are closed under coordinatewise addition.

Equations

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

theorem Quantifier.NumberTree.Additive.innerNeg {q : NumberTree} (h : q.Additive) : q.innerNeg.Additive

theorem Quantifier.NumberTree.additive_all : NumberTree.all.Additive

theorem Quantifier.NumberTree.additive_notAll : NumberTree.notAll.Additive

theorem Quantifier.NumberTree.additive_no : NumberTree.no.Additive

theorem Quantifier.NumberTree.additive_some : NumberTree.some.Additive

The tree of a generalized quantifier

A generalized quantifier counts its arguments with Set.ncard, which asks for no decidability; the counts are meaningful when the sets are finite.

def Quantifier.GQ.Quantity {α : Type u_1} (q : GQ α) : Prop

A quantifier has quantity when Q(A, B) depends only on the four cardinalities |A ∩ B|, |A \ B|, |B \ A| and |M \ (A ∪ B)|.

Equations

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

theorem Quantifier.GQ.QuantityInvariant.quantity {α : Type u_1} {Q : GQ α} [Finite α] (hQ : Q.QuantityInvariant) : Q.Quantity

On a finite universe a permutation-invariant quantifier has quantity, since equal cell cardinalities give a permutation carrying each cell of one pair onto the same cell of the other.

theorem Quantifier.GQ.Quantity.quantityInvariant {α : Type u_1} {Q : GQ α} (hQ : Q.Quantity) : Q.QuantityInvariant

A quantifier with quantity is permutation invariant, since a permutation preserves the cardinality of each cell.

theorem Quantifier.GQ.iff_of_ncard_eq {α : Type u_1} {Q : GQ α} {A B A' B' : α → Prop} [Finite α] (hC : Q.Conservative) (hQ : Q.QuantityInvariant) (hd : {x : α | A x ∧ ¬B x}.ncard = {x : α | A' x ∧ ¬B' x}.ncard) (hi : {x : α | A x ∧ B x}.ncard = {x : α | A' x ∧ B' x}.ncard) : Q A B ↔ Q A' B'

A conservative, permutation-invariant quantifier on a finite universe holds of A and B according to |A \ B| and |A ∩ B| alone.

def Quantifier.NumberTree.ofGQ {α : Type u_1} (Q : GQ α) : NumberTree

The tree of a generalized quantifier holds of (a, b) when the quantifier holds of some A and B with |A \ B| = a and |A ∩ B| = b.

Equations

• Quantifier.NumberTree.ofGQ Q a b = ∃ (A : α → Prop) (B : α → Prop), {x : α | A x ∧ ¬B x}.ncard = a ∧ {x : α | A x ∧ B x}.ncard = b ∧ Q A B

theorem Quantifier.NumberTree.ofGQ_iff {α : Type u_1} {Q : GQ α} [Finite α] (hC : Q.Conservative) (hQ : Q.QuantityInvariant) (A B : α → Prop) : ofGQ Q {x : α | A x ∧ ¬B x}.ncard {x : α | A x ∧ B x}.ncard ↔ Q A B

A conservative, permutation-invariant quantifier on a finite universe holds of A and B exactly when its tree holds of |A \ B| and |A ∩ B|.

def Quantifier.NumberTree.toGQ {α : Type u_1} (q : NumberTree) : GQ α

The quantifier of a tree holds of A and B when the tree holds of |A \ B| and |A ∩ B|.

Equations

• q.toGQ A B = q {x : α | A x ∧ ¬B x}.ncard {x : α | A x ∧ B x}.ncard

theorem Quantifier.NumberTree.toGQ_apply {α : Type u_1} (q : NumberTree) (A B : α → Prop) : q.toGQ A B ↔ q {x : α | A x ∧ ¬B x}.ncard {x : α | A x ∧ B x}.ncard

@[simp]

theorem Quantifier.NumberTree.toGQ_inf {α : Type u_1} (q r : NumberTree) : (q ⊓ r).toGQ = q.toGQ ⊓ r.toGQ

@[simp]

theorem Quantifier.NumberTree.toGQ_compl {α : Type u_1} (q : NumberTree) : qᶜ.toGQ = q.toGQᶜ

@[simp]

theorem Quantifier.NumberTree.toGQ_innerNeg {α : Type u_1} (q : NumberTree) : q.innerNeg.toGQ = q.toGQ.innerNeg

The quantifier of a tree's inner negation is the inner negation of its quantifier.

@[instance_reducible]

instance Quantifier.NumberTree.toGQ.decidable {α : Type u_1} [Fintype α] (q : NumberTree) [DecidableRel q] (A B : α → Prop) [DecidablePred A] [DecidablePred B] : Decidable (q.toGQ A B)

On a finite universe the quantifier of a decidable tree is decidable at decidable arguments.

Equations

• Quantifier.NumberTree.toGQ.decidable q A B = decidable_of_iff (q {x : α | A x ∧ ¬B x}.card {x : α | A x ∧ B x}.card) ⋯

theorem Quantifier.NumberTree.conservative_toGQ {α : Type u_1} (q : NumberTree) : q.toGQ.Conservative

The quantifier of a tree is conservative, since A \ B and A ∩ B see only B ∩ A.

theorem Quantifier.NumberTree.quantity_toGQ {α : Type u_1} (q : NumberTree) : q.toGQ.Quantity

The quantifier of a tree has quantity, depending on two of the four cells.

theorem Quantifier.NumberTree.quantityInvariant_toGQ {α : Type u_1} (q : NumberTree) : q.toGQ.QuantityInvariant

The quantifier of a tree is permutation invariant.

theorem Quantifier.NumberTree.ScopeMonotone.toGQ {α : Type u_1} [Finite α] {q : NumberTree} (h : q.ScopeMonotone) : q.toGQ.ScopeMonotone

The quantifier of a scope-monotone tree is scope monotone, since enlarging B within A moves |A \ B ∩ B'| individuals from A \ B to A ∩ B.

theorem Quantifier.NumberTree.ScopeAntitone.toGQ {α : Type u_1} [Finite α] {q : NumberTree} (h : q.ScopeAntitone) : q.toGQ.ScopeAntitone

The quantifier of a scope-antitone tree is scope antitone.

Counting quantifiers

def Quantifier.NumberTree.points (n : ℕ) : Finset ((_ : ℕ) × ℕ × ℕ)

The points of rows 0 to n of the tree, each given with its row.

Equations

• Quantifier.NumberTree.points n = (Finset.range (n + 1)).sigma Finset.antidiagonal

theorem Quantifier.NumberTree.card_points (n : ℕ) : (points n).card = (n + 1) * (n + 2) / 2

theorem Quantifier.NumberTree.card_powerset_points (n : ℕ) : (points n).powerset.card = 2 ^ ((n + 1) * (n + 2) / 2)

The conservative, permutation-invariant quantifiers on a universe of n individuals are the sets of points in rows 0 to n of the tree.

Constant rows and the individuals a quantifier depends on

def Quantifier.NumberTree.ConstantOnRow (q : NumberTree) (n : ℕ) : Prop

A quantifier is constant on the n-th row when whether it holds of an n-element restrictor does not depend on the scope.

Equations

• q.ConstantOnRow n = ∀ (a b a' b' : ℕ), a + b = n → a' + b' = n → (q a b ↔ q a' b')

def Quantifier.NumberTree.ConstantBelow (q : NumberTree) (n : ℕ) : Prop

A quantifier is constant on rows 0 to n when, on a universe of n individuals, it does not depend on its arguments at all.

Equations

• q.ConstantBelow n = ∀ (a b a' b' : ℕ), a + b ≤ n → a' + b' ≤ n → (q a b ↔ q a' b')

theorem Quantifier.NumberTree.not_constantOnRow_iff {q : NumberTree} {n : ℕ} : ¬q.ConstantOnRow n ↔ ∃ (a : ℕ) (b : ℕ), a + b + 1 = n ∧ ¬(q (a + 1) b ↔ q a (b + 1))

A row is constant unless two adjacent points of it differ.

theorem Quantifier.NumberTree.not_constantBelow_iff {q : NumberTree} {n : ℕ} : ¬q.ConstantBelow n ↔ ∃ (a : ℕ) (b : ℕ), a + b + 1 ≤ n ∧ (¬(q (a + 1) b ↔ q a b) ∨ ¬(q a (b + 1) ↔ q a b))

Rows 0 to n are constant unless two adjacent points among them differ.

theorem Quantifier.NumberTree.toGQ_some_iff {α : Type u_1} [Finite α] {A B : α → Prop} : NumberTree.some.toGQ A B ↔ ∃ (x : α), A x ∧ B x

theorem Quantifier.NumberTree.toGQ_no_iff {α : Type u_1} [Finite α] {A B : α → Prop} : NumberTree.no.toGQ A B ↔ ¬∃ (x : α), A x ∧ B x

theorem Quantifier.NumberTree.toGQ_all_iff {α : Type u_1} [Finite α] {A B : α → Prop} : NumberTree.all.toGQ A B ↔ ∀ (x : α), A x → B x

theorem Quantifier.NumberTree.dependsOn_toGQ_compl_singleton_iff {q : NumberTree} {α : Type u_1} [Finite α] (A : α → Prop) (e : α) : DependsOn (q.toGQ A) {e}ᶜ ↔ A e → q.ConstantOnRow {x : α | A x}.ncard

The quantifier of a tree depends on whether an individual is in its scope only if the individual is in its restrictor and the tree is not constant on the restrictor's row.

theorem Quantifier.NumberTree.exists_not_dependsOn_toGQ_restrictor_iff {q : NumberTree} {α : Type u_1} [Finite α] (e : α) : (∃ (B : α → Prop), ¬DependsOn (fun (A : α → Prop) => q.toGQ A B) {e}ᶜ) ↔ ¬q.ConstantBelow (Nat.card α)

The quantifier of a tree, as a function of its restrictor, depends for some scope on whether an individual is in the restrictor iff the tree is not constant below the size of the universe.