HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
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 4 through ax-3 6 and rule ax-mp 7) 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 7) the wffs ax-1 4, ax-2 5, pm2.04 34, con3 109, notnot2 99, and notnot1 101. 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 34) and replacing the last three with our ax-3 6. (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 3 and wn 2) 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, and the much shorter proofs that we show here were found manually. Truth tables grow exponentially with the number of variables, but it is unknown if the same is true of proofs - an answer to this would resolve the P=NP conjecture in complexity theory. |
| Ref | Expression |
|---|---|
| ax-1 |
  
 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph |
. 2
 | |
| 2 | wps |
. . 3
| |
| 3 | 2, 1 | wi 3 |
. 2
|
| 4 | 1, 3 | wi 3 |
1
|