Propositional calculus is the formal basis of logic dealing with the notion and usage of words such as "NOT," "OR," "AND," and "implies." Many systems of propositional calculus have been devised which attempt to achieve consistency, completeness, and independence of axioms. The term "sentential calculus" is sometimes used as a synonym for propositional calculus.

Axioms (or their schemata) and rules of inference define a proof theory, and various equivalent proof theories of propositional calculus can be devised. The following list of axiom schemata of propositional calculus is from Kleene (2002).

In each schema, , , can be replaced by any sentential formula. The following rule called Modus Ponens is the sole rule of inference:

This rule states that if each of and is either an axiom or a theorem formally deduced from axioms by application of inference rules, then is also a formal theorem.

Other rules are derived from Modus Ponens and then used in formal proofs to make proofs shorter and more understandable. These rules serve to directly introduce or eliminate connectives. Modus Ponens is basically -elimination, and the deduction theorem is -introduction.

Sample introduction rules include

Sample elimination rules include

Proof theories based on Modus Ponens are called Hilbert-type whereas those based on introduction and elimination rules as postulated rules are called Gentzen-type. All formal theorems in propositional calculus are tautologies and all tautologies are formally provable. Therefore, proofs can be used to discover tautologies in propositional calculus, and truth tables can be used to discover theorems in propositional calculus.

One can formulate propositional logic using just the NAND operator. The history of that can be found in Wolfram (2002, p. 1151). The shortest such axiom is the Wolfram axiom.

See also

Connective, Deduction Theorem, First-Order Logic, Logic, Modus Ponens, Modus Tollens, P-Symbol, Peano Arithmetic, Predicate Calculus

Portions of this entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha

References

Chang, C.-L. and Lee, R. C.-T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.Cundy, H. and Rollett, A. Mathematical Models, 3rd ed. Stradbroke, England: Tarquin Pub., pp. 254-255, 1989.Kleene, S. C. Mathematical Logic. New York: Dover, 2002.Mendelson, E. "The Propositional Calculus." Ch. 1 in Introduction to Mathematical Logic, 4th ed. London, England: Chapman & Hall, pp. 12-44, 1997.Nidditch, P. H. Propositional Calculus. New York: Free Press of Glencoe, 1962.Wolfram, S. A New Kind of Science. Champaign, IL: Wolfram Media, 1151, 2002.

Referenced on Wolfram|Alpha

Propositional Calculus

Cite this as:

Weisstein, Eric W., with contributions by Alex Sakharov. "Propositional Calculus." From MathWorld--A Wolfram Resource. https://mathworld.wolfram.com/PropositionalCalculus.html

Subject classifications