### Abstract

A range of algebras between lattices and Boolean algebras generalise the notion of a complement. We develop a hierarchy of these pseudo-complemented algebras that includes Stone algebras. Independently of this theory we study filters based on partial orders. Both theories are combined to prove Chen and Grätzer's construction theorem for Stone algebras. The latter involves extensive reasoning about algebraic structures in addition to reasoning in algebraic structures.

### License

BSD License

### Topics

- Mathematics/Order

### Session Stone_Algebras

- Lattice_Basics
- P_Algebras
- Filters
- Stone_Construction

### Used by

- A Hierarchy of Algebras for Boolean Subsets
- Stone Relation Algebras

## Cite

×

Stone_Algebras-AFP

    @article{Stone_Algebras-AFP,
      author  = {Walter Guttmann},
      title   = {Stone Algebras},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Stone_Algebras.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 28, 2019 : Isabelle2019
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Sep 6, 2016 : Isabelle2016