Axiom ax-1 3

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."

Propositional calculus (axioms ax-1 3 through ax-3 5 and rule ax-mp 6) 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 6) the wffs ax-1 3, ax-2 4, pm2.04 31, con3 86, nega 78, and negb 79. 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 31) and replacing the last three with our ax-3 5. (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. 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.

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 2	. 2 wff (ψ → φ)
4	1, 3	wi 2	1 wff (φ → (ψ → φ))

This axiom is referenced by:  a1i 7  id 9  id1 10  com12 13  syl1 16  pm2.04 31  pm2.86 63  loolin 66  loowoz 67  pm2.21 71  pm3.27im 121  biigb 129  pm5.4 146  a1bi 172  olc 224  pm4.45im 267  imbi2 473  oibabs 493  pm5.18 497  tbt 541  biimt 549  biort 550  dedlem0a 567  hbim 702  hbimd 787  eqsal 833  eqvin.l1 851  stdpc4 869  sb6x 871  sb6y 872  sbi2 885  ax11a 926  moimv 1044  rgen2 1248  r19.12 1281  r19.37av 1300  undif4 1744  find 2396  findsg 2398  tfindsg 2402  abrexex 2912  omex 3475  kmlem11 3590  suppsr2 4017  suppsr3 4018  axsup 4088  ltlent 4288  stcltr2 5708

metamath.org