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 576  imbi2 622  oibabs 652  pm5.18 658  pm5.14 663  elimant 682  biimt 729  biort 732  dedlem0a 758  hbim 1004  ax46to4 1014  ax467to4 1020  hbimd 1106  equsal 1147  stdpc4 1181  sb6x 1184  ax11 1214  sbi2 1228  ax11v 1260  ax11eq 1356  ax11el 1357  ax11f 1358  ax11indi 1360  ax11indalem 1361  ax11inda2ALT 1362  ax11inda2 1363  moimv 1412  alral 1684  rgen2a 1691  r19.12 1732  r19.37av 1753  undif4 2315  class2seteq 2725  dvdemo2 2766  ordunisuc2 3105  find 3145  findsg 3147  tfindsg 3152  abrexex 3845  omex 4599  kmlem12 4748  suppsr3 5196  pre-axsup 5263  ltlent 5495  squeeze0 5872  supxrre 6030  ioonegt 6339  iccnegt 6340  fsumconst 6976  basgen2t 7581  iscms2 7928  minveclem27 8502  2bornot2b 8724  stcltr2 10112  mdsl1 10156

Copyright terms: Public domain