A system of symbolic logic, designed to study propositions. A proposition is a statement that is true or false. There are many alternative but equivalent definitions of propositional calculus, one of the more useful definitions for the computer scientist being given here.

The only terms of the propositional calculus are the two symbols T and F (standing for true and false) together with variables for logical propositions, which are denoted by small letters p,q,r,…; these symbols are basic and indivisible and are thus called atomic formulas.

The propositional calculus is based on the study of well-formed formulas, or wff for short. New wff of the form

are formed from given wff A, B, and C using logical connectives; respectively they are called negation, disjunction, conjunction, implication, equivalence, and conditional. If 〈atf〉 denotes the class of atomic formulas, then the class of wff 〈wff〉, can be described in BNF notation (see fig. 1).

Proofs and theorems within the propositional calculus are conducted in a formal and rigorous manner: certain basic axioms are assumed and certain rules of inference are followed. In particular these rules must deal with the various connectives.

The rules of inference are stated using a form such as

The rule should be interpreted to mean that on the assumption that α‎ is true, it can be deduced that β‎ is then true. Logicians often use the notation α‎|-β‎. In writing the rules it is convenient to employ a notation such asΓ‎ is some set of wff whose truth has been established; A and B are some other wff highlighted for the purposes of the rule; ⇒ denotes implication (to avoid confusion with the symbol ⊃). For example, the rules for the introduction and elimination respectively of the ∧ connective are shown in Fig. 2.