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.