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 98, notnot2 87, and notnot1 89. 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.43aOLD 69  pm2.86 72  loolin 75  loowoz 76  pm2.21 79  pm2.51 107  pm2.52 108  pm3.27im 146  dfbi1gb 166  pm4.8 169  pm5.4 174  a1bi 204  olc 275  pm4.45im 339  pm2.64 439  pm2.82 589  imbi2 635  oibabs 665  pm5.18 671  pm5.14 676  elimant 696  biimt 743  biort 746  dedlem0a 772  hbim 1048  ax46to4 1059  ax467to4 1065  hbimd 1151  equsal 1193  hbequid 1211  stdpc4 1227  sb6x 1230  ax11 1261  sbi2 1275  ax11v 1307  ax11eq 1405  ax11el 1406  ax11f 1407  ax11indi 1409  ax11indalem 1410  ax11inda2ALT 1411  ax11inda2 1412  moimv 1461  alral 1739  rgen2a 1746  r19.12 1787  r19.37av 1808  undif4 2377  class2seteq 2790  dvdemo2 2832  ordunisuc2 3172  find 3212  findsg 3214  tfindsg 3219  abrexex 3917  omex 4689  kmlem12 4838  suppsr3 5289  pre-axsup 5356  ltlen 5587  squeeze0 5984  supxrre 6165  iccneg 6433  fsumcons 7128  basgen2 7728  iscms2 8079  minveclem27 8655  2bornot2b 8868  stcltr2i 10286  mdsl1i 10332

Copyright terms: Public domain