命题演算(propositional calculus)
命题与其逻辑关联的形式系统。命题演算是谓词演算的反面，运用尚未分机的简单命题而不是谓词来当成基本（原子）单元。单纯（原子）命题是用小写的罗马字母表示，复合（分子）命题则用标准符号@8(logicAnd.jpg代表「与」，@8(logicOr.jpg代表「或」，代表「若……则」，@8(logicNon.jpg代表「否」。作为形式系统，命题演算专注於确定从公理所能证明的式子（复合命题形式）。命题之间的有效推论是从可证明的公式得来，因为AB只有当B是A的逻辑上的必然结果才能证明。命题演算在没有式子存在情况是符合的。A且@8(logicNon.jpgA是可以证明的。加入无法证明的式子作为新的公理会引起矛盾，道理上也很完备。再者，要决定给定式子能否在系统内证明已有常规可循。
English version：
propositional calculus
Formal system of propositions and their logical relationships. As opposed to the predicate calculus, the propositional calculus employs simple, unanalyzed propositions rather than predicates as its atomic units. Simple (atomic) propositions are denoted by lowercase Roman letters (e.g., p, q), and compound (molecular) propositions are formed using the standard symbols ∧ for “and,” ∨ for “or,” for “if . . . then,” and ¬ for “not.” As a formal system, the propositional calculus is concerned with determining which formulas (compound proposition forms) are provable from the axioms. Valid inferences among propositions are reflected by the provable formulas, because (for any formulas A and B) A B is provable if and only if B is a logical consequence of A. The propositional calculus is consistent in that there exists no formula A in it such that both A and ¬ A are provable. It is also complete in the sense that the addition of any unprovable formula as a new axiom would introduce a contradiction. Further, there exists an effective procedure for deciding whether a given formula is provable in the system. See also logic, predicate calculus, laws of thought.