Axiom ax-1 4

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 ph and ps to the assertion of ph 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 30, con3 94, nega 84, and negb 86. 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 30) 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.

Assertion

Ref	Expression
ax-1	|- (ph -> (ps -> ph))

Detailed syntax breakdown of Axiom ax-1

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		wps	. . 3 wff ps
3	2, 1	wi 3	. 2 wff (ps -> ph)
4	1, 3	wi 3	1 wff (ph -> (ps -> ph))

This axiom is referenced by:  a1i 8  com12 11  a1d 12  imim2 14  pm2.04 30  a1dd 42  id 59  id1 60  pm2.43a 66  pm2.86 69  loolin 72  loowoz 73  pm2.21 76  pm2.51 101  pm2.52 102  pm3.27im 140  biigb 159  pm4.8 162  pm5.4 167  a1bi 197  olc 268  pm4.45im 332  pm2.64 429  pm2.82 576  imbi2 622  oibabs 651  pm5.18 657  pm5.14 662  elimant 681  biimt 728  biort 731  dedlem0a 757  hbim 983  ax46to4 992  ax467to4 998  hbimd 1086  equsal 1134  stdpc4 1168  sb6x 1171  ax11 1203  sbi2 1217  ax11v 1249  ax11eq 1340  ax11el 1341  ax11f 1342  ax11indi 1344  ax11indalem 1345  ax11inda2ALT 1346  ax11inda2 1347  moimv 1396  alral 1668  rgen2a 1675  r19.12 1716  r19.37av 1737  undif4 2296  class2seteq 2703  dvdemo2 2744  ordunisuc2 3078  find 3118  findsg 3120  tfindsg 3125  abrexex 3799  omex 4551  kmlem12 4700  suppsr3 5147  pre-axsup 5214  ltlent 5446  squeeze0 5823  supxrre 5981  ioonegt 6290  iccnegt 6291  fsumconst 6927  basgen2t 7532  iscms2 7876  minveclem27 8437  2bornot2b 8965  stcltr2 10326  mdsl1 10370

Copyright terms: Public domain