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).
 |
(1)
|
 |
(2)
|
 |
(3)
|
 |
(4)
|
 |
(5)
|
 |
(6)
|
 |
(7)
|
 |
(8)
|
 |
(9)
|
 |
(10)
|
In each schema, 
,
,
can be replaced by any sentential formula.
The following rule called Modus Ponens is the sole
rule of inference:
 |
(11)
|
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
 |
(12)
|
Sample elimination rules include
 |
(13)
|
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.
