ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-1 GIF version

Axiom ax-1 5
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 5 through ax-3 7 and rule ax-mp 8) 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 8) the wffs ax-1 5, ax-2 6, pm2.04 75, con3 550, notnot2 718, and notnot1 541. 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 75) and replacing the last three with our ax-3 7. (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 4 and wn 3) 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, since truth tables grow exponentially with the number of variables, and the much shorter proofs that we show here were found manually.

Ref Expression
ax-1 (φ → (ψφ))

Detailed syntax breakdown of Axiom ax-1
StepHypRef Expression
1 wph . 2 wff φ
2 wps . . 3 wff ψ
32, 1wi 4 . 2 wff (ψφ)
41, 3wi 4 1 wff (φ → (ψφ))
Colors of variables: wff set class
This axiom is referenced by:  a1i  10  id  18  id1  19  a1d  21  a1dd  41  jarr  90  pm2.86i  91  pm2.86d  92  pm5.1im  161  biimt  229  pm5.4  237  pm4.45im  316  pm2.51  560  pm4.8  602  pm2.53  617  imorri  644  pm2.64  689  pm2.82  700  biort  714  oibabs  806  pm5.14  832  dedlem0a  887  oplem1  899  meredith  1250  a9wa9lem6  1410  a9wa9lem6OLD  1411  a9wa9lem7  1412  ax46to4  1450  ax467to4  1456  stdpc4  1619  ax11  1655  sbi2  1669  ax11v  1703  ax11eq  1810  ax11el  1811  ax11f  1812  ax11indi  1814  ax11indalem  1815  ax11inda2ALT  1816  ax11inda2  1817  moimv  1872  euim  1874
  Copyright terms: Public domain W3C validator