**Description: **Axiom *Simp*. Axiom
A1 of [Margaris] p. 49. One of the 3 axioms
of
propositional calculus. The 3 axioms are also given as Definition 2.1 of
[Hamilton] p. 28. This axiom is called
*Simp* or "the principle of
simplification" in *Principia Mathematica* (Theorem *2.02 of
[WhiteheadRussell] p. 100)
because "it enables us to pass from the joint
assertion of and to
the assertion of simply."
*General remarks*: Propositional calculus (axioms ax-1 5
through ax-3 7
and rule ax-mp 8) 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 8)
the wffs
ax-1 5, ax-2 6, pm2.04 75, con3 550,
notnot2 718, and notnot1 541. 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 75) and replacing the last three with our ax-3 7.
(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 4 and wn 3)
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. |