Cylindric algebras

This file defines cylindric algebras. A cylindric algebra of dimension ι is a Boolean algebra with a cylindrification cyl i for each i : ι and a diagonal element diag i j for each pair of indices. Cylindrification is the algebraic form of existential quantification over the i-th variable and the diagonal is the algebraic form of the equation between the i-th and j-th variables, so cylindric algebras stand to first-order logic with equality as Boolean algebras stand to propositional logic.

Predicates on assignments ι → E form a cylindric algebra, where cyl i p holds of g when p holds of some i-variant of g and diag i j holds of g when g i = g j. The existential quantifiers and identity conditions of the assignment-based dynamic systems are these operations.

Main definitions

• CylindricAlgebra ι A: the cylindrifications and diagonal elements on a Boolean algebra A.
• CylindricAlgebra.cylClosure: cylindrification as a closure operator.
• CylindricAlgebra.dimSet: the dimension set of an element, the indices it depends on.
• CylindricAlgebra.subst: substitution of the j-th variable for the i-th.

Main results

• CylindricAlgebra.disjoint_cyl_comm: cylindrification is conjugate to itself.
• CylindricAlgebra.cyl_sup: cylindrification distributes over joins.
• CylindricAlgebra.subst_compl, CylindricAlgebra.subst_sup, CylindricAlgebra.subst_inf: substitution is a Boolean endomorphism.
• CylindricAlgebra.diag_comm: diagonal elements are symmetric.
• CylindricAlgebra.subst_apply: on predicates, substitution evaluates the predicate at the assignment updated at i with the value at j.
• CylindricAlgebra.dimSet_subset_of_dependsOn: a predicate that depends only on the variables in s has its dimension set inside s.

Implementation notes

CylindricAlgebra ι A is a mixin over [BooleanAlgebra A] rather than an extension of it, as Module R M is over [AddCommMonoid M]: the dimension ι could not be inferred from a parent projection to BooleanAlgebra A.

The concrete algebra is carried both by predicates (ι → E) → Prop with the pointwise Boolean algebra and by Set (ι → E). The set algebra is defined on Set directly rather than transported from the predicate algebra, so that it agrees reducibly with the condition algebra of every register structure (DynamicSemantics.RegisterStructure.cylindricAlgebra) at the canonical one.

References

• [HMT71]

class CylindricAlgebra (ι : Type u_1) (A : Type u_2) [BooleanAlgebra A] : Type (max u_1 u_2)

The cylindrifications cyl i and diagonal elements diag i j of a cylindric algebra of dimension ι on the Boolean algebra A, with the seven axioms of [HMT71].

• cyl : ι → A → A

  Cylindrification along the index i.

• diag : ι → ι → A

  The diagonal element of the indices i and j.

• cyl_bot (i : ι) : cyl i ⊥ = ⊥
• le_cyl (i : ι) (x : A) : x ≤ cyl i x
• cyl_inf_cyl (i : ι) (x y : A) : cyl i (x ⊓ cyl i y) = cyl i x ⊓ cyl i y
• cyl_comm (i j : ι) (x : A) : cyl i (cyl j x) = cyl j (cyl i x)
• diag_self (i : ι) : diag i i = ⊤
• cyl_diag_inf_diag {i j k : ι} (hij : i ≠ j) (hik : i ≠ k) : cyl i (diag j i ⊓ diag i k) = diag j k
• disjoint_cyl_diag_inf {i j : ι} (hij : i ≠ j) (x : A) : Disjoint (cyl i (diag i j ⊓ x)) (cyl i (diag i j ⊓ xᶜ))

Cylindrification

@[simp]

theorem CylindricAlgebra.cyl_top {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] {i : ι} : cyl i ⊤ = ⊤

@[simp]

theorem CylindricAlgebra.cyl_cyl {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] {i : ι} {x : A} : cyl i (cyl i x) = cyl i x

theorem CylindricAlgebra.cyl_mono {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] {i : ι} : Monotone (cyl i)

theorem CylindricAlgebra.cyl_le_cyl {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] {i : ι} {x y : A} (h : x ≤ y) : cyl i x ≤ cyl i y

def CylindricAlgebra.cylClosure {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] (i : ι) : ClosureOperator A

Cylindrification along i as a closure operator. Its closed elements are the elements that do not depend on the i-th variable.

Equations

• CylindricAlgebra.cylClosure i = ClosureOperator.mk' (CylindricAlgebra.cyl i) ⋯ ⋯ ⋯

@[simp]

theorem CylindricAlgebra.cylClosure_apply {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] {i : ι} {x : A} : (cylClosure i) x = cyl i x

@[simp]

theorem CylindricAlgebra.cyl_eq_bot {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] {i : ι} {x : A} : cyl i x = ⊥ ↔ x = ⊥

theorem CylindricAlgebra.cyl_cyl_inf {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] (i : ι) (x y : A) : cyl i (cyl i x ⊓ y) = cyl i x ⊓ cyl i y

@[simp]

theorem CylindricAlgebra.cyl_compl_cyl {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] {i : ι} {x : A} : cyl i (cyl i x)ᶜ = (cyl i x)ᶜ

The complement of a cylinder is a cylinder.

theorem CylindricAlgebra.disjoint_cyl_comm {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] {i : ι} {x y : A} : Disjoint (cyl i x) y ↔ Disjoint x (cyl i y)

Cylindrification is conjugate to itself.

theorem CylindricAlgebra.cyl_sup {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] (i : ι) (x y : A) : cyl i (x ⊔ y) = cyl i x ⊔ cyl i y

Dimension sets

def CylindricAlgebra.dimSet {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] (x : A) : Set ι

The dimension set of x is the set of indices along which cylindrification moves x. For a formula these are its free variables.

Equations

• CylindricAlgebra.dimSet x = {i : ι | CylindricAlgebra.cyl i x ≠ x}

theorem CylindricAlgebra.notMem_dimSet {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] {i : ι} {x : A} : i ∉ dimSet x ↔ cyl i x = x

theorem CylindricAlgebra.notMem_dimSet_cyl {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] {i : ι} {x : A} : i ∉ dimSet (cyl i x)

@[simp]

theorem CylindricAlgebra.dimSet_compl {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] (x : A) : dimSet xᶜ = dimSet x

theorem CylindricAlgebra.dimSet_inf_subset {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] (x y : A) : dimSet (x ⊓ y) ⊆ dimSet x ∪ dimSet y

theorem CylindricAlgebra.dimSet_sup_subset {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] (x y : A) : dimSet (x ⊔ y) ⊆ dimSet x ∪ dimSet y

theorem CylindricAlgebra.dimSet_cyl_subset {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] (i : ι) (x : A) : dimSet (cyl i x) ⊆ dimSet x \ {i}

Diagonal elements and substitution

theorem CylindricAlgebra.cyl_diag {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] {i j : ι} (h : i ≠ j) : cyl i (diag i j) = ⊤

theorem CylindricAlgebra.dimSet_diag_subset {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] (i j : ι) : dimSet (diag i j) ⊆ {i, j}

def CylindricAlgebra.subst {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] [DecidableEq ι] (i j : ι) (x : A) : A

Substitution of the j-th variable for the i-th constrains the two to agree and then forgets the i-th. Substituting a variable for itself does nothing.

Equations

• CylindricAlgebra.subst i j x = if i = j then x else CylindricAlgebra.cyl i (CylindricAlgebra.diag i j ⊓ x)

@[simp]

theorem CylindricAlgebra.subst_self {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] [DecidableEq ι] (i : ι) (x : A) : subst i i x = x

theorem CylindricAlgebra.subst_of_ne {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] {i j : ι} [DecidableEq ι] (h : i ≠ j) (x : A) : subst i j x = cyl i (diag i j ⊓ x)

theorem CylindricAlgebra.subst_sup {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] [DecidableEq ι] (i j : ι) (x y : A) : subst i j (x ⊔ y) = subst i j x ⊔ subst i j y

theorem CylindricAlgebra.subst_compl {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] [DecidableEq ι] (i j : ι) (x : A) : subst i j xᶜ = (subst i j x)ᶜ

Substitution commutes with complement. Off the diagonal, this is the content of the seventh cylindric axiom.

theorem CylindricAlgebra.subst_inf {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] [DecidableEq ι] (i j : ι) (x y : A) : subst i j (x ⊓ y) = subst i j x ⊓ subst i j y

@[simp]

theorem CylindricAlgebra.subst_top {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] [DecidableEq ι] (i j : ι) : subst i j ⊤ = ⊤

@[simp]

theorem CylindricAlgebra.subst_bot {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] [DecidableEq ι] (i j : ι) : subst i j ⊥ = ⊥

theorem CylindricAlgebra.subst_eq_self {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] {i : ι} {x : A} [DecidableEq ι] (h : i ∉ dimSet x) (j : ι) : subst i j x = x

Substitution for a variable that x does not depend on leaves x unchanged.

theorem CylindricAlgebra.diag_comm {ι : Type u_1} {A : Type u_2} [BooleanAlgebra A] [CylindricAlgebra ι A] (i j : ι) : diag i j = diag j i

The cylindric algebra of predicates on assignments

@[instance_reducible]

instance CylindricAlgebra.instForallForallProp {ι : Type u_1} {E : Type u_3} [DecidableEq ι] : CylindricAlgebra ι ((ι → E) → Prop)

Predicates on assignments form a cylindric algebra, in which cyl i p holds of g when p holds of some i-variant of g, and diag i j holds of g when g i = g j.

Equations

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

@[simp]

theorem CylindricAlgebra.cyl_apply {ι : Type u_1} {i : ι} {E : Type u_3} [DecidableEq ι] {p : (ι → E) → Prop} {g : ι → E} : cyl i p g ↔ ∃ (e : E), p (Function.update g i e)

@[simp]

theorem CylindricAlgebra.diag_apply {ι : Type u_1} {i j : ι} {E : Type u_3} [DecidableEq ι] {g : ι → E} : diag i j g ↔ g i = g j

theorem CylindricAlgebra.subst_apply {ι : Type u_1} {i j : ι} {E : Type u_3} [DecidableEq ι] {p : (ι → E) → Prop} {g : ι → E} : subst i j p g ↔ p (Function.update g i (g j))

Substituting the j-th variable for the i-th evaluates the predicate at the assignment whose i-th value is overwritten by its j-th value.

theorem CylindricAlgebra.dimSet_subset_of_dependsOn {ι : Type u_1} {E : Type u_3} [DecidableEq ι] {p : (ι → E) → Prop} {s : Set ι} (hp : DependsOn p s) : dimSet p ⊆ s

A predicate that depends only on the variables in s is fixed by cylindrification along every index outside s.

@[instance_reducible]

instance CylindricAlgebra.instSetPi {ι : Type u_1} {E : Type u_3} [DecidableEq ι] : CylindricAlgebra ι (Set (ι → E))

Sets of assignments form the cylindric set algebra of [HMT71], the algebra of predicates under Set's order.

Equations

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

@[simp]

theorem CylindricAlgebra.mem_cyl {ι : Type u_1} {i : ι} {E : Type u_3} [DecidableEq ι] {t : Set (ι → E)} {g : ι → E} : g ∈ cyl i t ↔ ∃ (e : E), Function.update g i e ∈ t

@[simp]

theorem CylindricAlgebra.mem_diag {ι : Type u_1} {i j : ι} {E : Type u_3} [DecidableEq ι] {g : ι → E} : g ∈ diag i j ↔ g i = g j