Home Metamath Proof Explorer < Previous   Next > Related theorems Unicode version

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 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 69, con3 146, notnot2 130, and notnot1 137. 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 69) 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

Detailed syntax breakdown of Axiom ax-1
StepHypRef Expression
1 wph . 2
2 wps . . 3
32, 1wi 3 . 2
41, 3wi 3 1
 Colors of variables: wff set class This axiom is referenced by:  a1i 8  id 15  id1 16  a1d 18  com12OLD 27  imim2OLD 30  pm2.04OLD 70  a1dd 94  pm2.86i 113  pm2.86d 114  pm2.86OLD 116  loolinALT 119  loowoz 120  pm2.21OLD 125  simprimOLD 181  pm2.51 186  pm2.52OLD 189  pm2.61 204  dfbi1gb 238  pm5.4 302  pm4.8 307  biimt 323  a1biOLD 325  olc 375  simpl 437  pm4.45im 532  imbi2 759  pm2.64 831  pm2.74 906  pm2.82 915  oibabs 971  pm5.14 978  pm5.18OLD 984  biort 998  elimantOLD 1009  dedlem0a 1079  dedlem0aOLD 1080  dn1OLD 1099  meredith 1475  pm2.43bgbi 1574  pm2.43cbi 1575  hbim 1643  ax46to4 1654  ax467to4 1660  hbimd 1749  hbequid2 1813  stdpc4 1829  ax11 1865  sbi2 1879  ax11v 1912  ax11eq 2018  ax11el 2019  ax11f 2020  ax11indi 2022  ax11indalem 2023  ax11inda2ALT 2024  ax11inda2 2025  moimv 2080  euim 2082  alral 2404  r19.12 2454  r19.27av 2472  r19.37av 2480  eqvinc 2628  rr19.3v 2640  class2seteq 3640  dvdemo2 3684  dfwe2 4007  ordunisuc2 4065  tfindsg 4080  findsg 4113  abrexex 4929  iotanul 5232  smo11 5275  omex 5966  domtriomlem 6296  domtriomlemOLD 6298  kmlem12 6348  suppsr3 6742  pre-axsup 6807  ltlen 6881  squeeze0 7440  supxrre 7632  iccneg 7922  fsumconst 8694  algcvgblem 9340  basgen2 9760  iscms2 10138  minveclem27 10786  2bornot2b 11014  stcltr2i 12678  mdsl1i 12724  bnj872 13571  bnj1050 13660  bnj1167 13730  hbimtg 14514  tb-ax2 14829  tbw-bijust 14865  tbw-negdf 14866  tbw-ax2 14868  merco1 14880  r19.37 15000  issubcat 15987  inttarcar 16088  a1i4 16151  iccconn 16277  fmfnfm 16422  prtlem1 17054  ax4567to4 17184  ax4567to5 17185  ax4567to6 17186  ax4567to7 17187  atpsub 18185
Copyright terms: Public domain