Monadic Boolean algebra

In abstract algebra, a monadic Boolean algebra is an algebraic structure A with signature

⟨·, +, ', 0, 1, ∃⟩ of type ⟨2,2,1,0,0,1⟩,

where ⟨A, ·, +, ', 0, 1⟩ is a Boolean algebra.

The monadic/unary operator ∃ denotes the existential quantifier, which satisfies the identities (using the received prefix notation for ∃):

• ∃0 = 0
• ∃x ≥ x
• ∃(x + y) = ∃x + ∃y
• ∃x∃y = ∃(x∃y).

∃x is the existential closure of x. Dual to ∃ is the unary operator ∀, the universal quantifier, defined as ∀x := (∃x′)′.

A monadic Boolean algebra has a dual definition and notation that take ∀ as primitive and ∃ as defined, so that ∃x := (∀x′)′. (Compare this with the definition of the dual Boolean algebra.) Hence, with this notation, an algebra A has signature ⟨·, +, ', 0, 1, ∀⟩, with ⟨A, ·, +, ', 0, 1⟩ a Boolean algebra, as before. Moreover, ∀ satisfies the following dualized version of the above identities:

1. ∀1 = 1
2. ∀x ≤ x
3. ∀(xy) = ∀x∀y
4. ∀x + ∀y = ∀(x + ∀y).

∀x is the universal closure of x.