Table of Contents - 1.2.2. The axioms of propositional calculus

Propositional calculus (Axioms ax-1 through ax-3 and rule ax-mp) can
be thought of as asserting formulas that are universally "true" when their
variables are replaced by any combination of "true" and "false".
Propositional calculus was first formalized by Frege in 1879, using as his
axioms (in addition to rule ax-mp) the wffs ax-1, ax-2, pm2.04,
con3, notnot, and notnotr. Around 1930, Lukasiewicz simplified the
system by eliminating the third (which follows from the first two, as you can
see by looking at the proof of pm2.04) and replacing the last three with
our ax-3. (Thanks to Ted Ulrich for this information.)

The theorems of propositional calculus are also called tautologies.
Tautologies can be proved very simply using truth tables, based on the
true/false interpretation of propositional calculus. To do this, we assign
all possible combinations of true and false to the wff variables and verify
that the result (using the rules described in wi and wn) always
evaluates to true. This is called the semantic approach. Our approach is
called the syntactic approach, in which everything is derived from axioms.
A metatheorem called the Completeness Theorem for Propositional Calculus
shows that the two approaches are equivalent and even provides an algorithm
for automatically generating syntactic proofs from a truth table. Those
proofs, however, tend to be long, since truth tables grow exponentially with
the number of variables, and the much shorter proofs that we show here were
found manually.