The Boolean Algebra Logic: The Soundness and Completeness Theorem

A sound and complete Gentzen-typed deduction system is given for a Boolean algebra logic, where the logical connective - is missed and an assignment is a function from the propositional variables to a Boolean algebra. A correspondence between the quotient of formulas under the valid equivalences of formulas and lattices is given, corresponding to the correspondence between the quotient of formulas under the classical valid equivalences of formulas and Boolean algebras.