关键词: 布尔代数, 命题逻辑, 不等式, 完备性

Abstract: Deduction systems are important arts of searching technology. This paper gives a new correspondence between the propositional logic and Boolean algebra, where an inequation is corresponding to a Gentzen sequent, so that the inequation is true in every Boolean algebra if and only if the Gentzen sequent is provable. In information retrieval, the information inference can effectively turn into the operation on poset. Precisely, the logical language for the propositional logic contains operators ¬、∧、∨; the terms instead of formulas are defined （a|¬t|t₁∧t₂|t₁∨t₂, where a is an element) and used to represent elements in Boolean algebra. This paper defines an assignment v using Boolean algebra as its domain, and assigns the terms to be the element in Boolean algebra. The sequence Γ→Δ is satisfied if∩_t∈Γt^v≤∪_t∈Δt^v. Finally, this paper gives a Gentzen system to prove the soundness and completeness theorem.

Key words: Boolean algebra, proposition logic, inequation, completeness