The Oxford Biblical Studies Online and Oxford Islamic Studies Online have retired. Content you previously purchased on Oxford Biblical Studies Online or Oxford Islamic Studies Online has now moved to Oxford Reference, Oxford Handbooks Online, Oxford Scholarship Online, or What Everyone Needs to Know®. For information on how to continue to view articles visit the subscriber services page.

Related Content

More Like This

Show all results sharing these subjects:

  • Science and technology
  • Mathematics and Computer Science


Show Summary Details


propositional calculus

Quick Reference

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 for the computer scientist being given below.

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 (∼A), (AB), (AB), (AB), (AB), (IF A THEN B ELSE C)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).

(∼A), (AB), (AB),

(AB), (AB),


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 Γ, AB Γ 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.


Reference entries