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 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	⊢ (φ → (ψ → φ))

Detailed syntax breakdown of Axiom ax-1

Step	Hyp	Ref	Expression
1		wph	. 2 wff φ
2		wps	. . 3 wff ψ
3	2, 1	wi 3	. 2 wff (ψ → φ)
4	1, 3	wi 3	1 wff (φ → (ψ → φ))

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 577  imbi2 623  oibabs 653  pm5.18 659  pm5.14 664  elimant 683  biimt 730  biort 733  dedlem0a 759  hbim 1005  ax46to4 1016  ax467to4 1022  hbimd 1108  equsal 1149  stdpc4 1183  sb6x 1186  ax11 1217  sbi2 1231  ax11v 1263  ax11eq 1361  ax11el 1362  ax11f 1363  ax11indi 1365  ax11indalem 1366  ax11inda2ALT 1367  ax11inda2 1368  moimv 1417  alral 1689  rgen2a 1696  r19.12 1737  r19.37av 1758  undif4 2321  class2seteq 2731  dvdemo2 2772  ordunisuc2 3115  find 3155  findsg 3157  tfindsg 3162  abrexex 3862  omex 4619  kmlem12 4768  suppsr3 5216  pre-axsup 5283  ltlent 5515  squeeze0 5892  supxrre 6050  ioonegt 6359  iccnegt 6360  fsumconst 6996  basgen2t 7601  iscms2 7956  minveclem27 8531  2bornot2b 8759  stcltr2 10175  mdsl1 10219

Copyright terms: Public domain