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, notnot2 84, and notnot1 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.86 69  loolin 72  loowoz 73  pm2.21 76  pm2.51 100  pm2.52 101  pm3.27im 138  dfbi1gb 157  pm4.8 160  pm5.4 165  a1bi 195  olc 266  pm4.45im 330  pm2.64 430  pm2.82 581  imbi2 627  oibabs 657  pm5.18 663  pm5.14 668  elimant 688  biimt 736  biort 739  dedlem0a 765  dn1 779  hbim 1043  ax46to4 1054  ax467to4 1060  hbimd 1146  equsal 1188  hbequid 1206  stdpc4 1222  sb6x 1225  ax11 1256  sbi2 1270  ax11v 1303  ax11eq 1402  ax11el 1403  ax11f 1404  ax11indi 1406  ax11indalem 1407  ax11inda2ALT 1408  ax11inda2 1409  moimv 1458  alral 1738  rgen2a 1745  r19.12 1786  r19.37av 1807  undif4 2378  class2seteq 2809  dvdemo2 2852  ordunisuc2 3198  tfindsg 3213  find 3243  findsg 3245  abrexex 3974  omex 4772  kmlem12 4922  suppsr3 5378  pre-axsup 5445  ltlen 5676  squeeze0 6069  supxrre 6251  iccneg 6534  fsumconst 7241  basgen2 7851  iscms2 8205  minveclem27 8831  2bornot2b 9059  stcltr2i 10483  mdsl1i 10529  issubcat 11299  a1i4 11334  iccconn 11514  fmfnfm 11704

Copyright terms: Public domain