HomeHome Metamath Proof Explorer < Wrap   Next >
Browser slow? Try the
Unicode version.

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12110

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-9056)
  Hilbert Space Explorer  Hilbert Space Explorer
(9057-10644)
  Users' Mathboxes  Users' Mathboxes
(10645-12110)
 

Table of Contents
Pre-logic
    Dummy link theorem for assisting proof development   dummylink 1
Propositional calculus
    Recursively define primitive wffs for propositional calculus   wn 2
    The axioms of propositional calculus   ax-1 4
    Logical implication   a1i 8
    Logical negation   con4i 74
    Logical equivalence   wb 144
    Logical disjunction and conjunction   wo 220
    Miscellaneous theorems of propositional calculus   pm5.1 679
    Abbreviated conjunction and disjunction of three wff's   w3o 779
Other axiomatizations of classical propositional calculus
    Derive the Lukasiewicz axioms from Meredith's sole axiom   meredith 930
    Derive the standard axioms from the Lukasiewicz axioms   luklem1 947
    Logical 'nand' (Sheffer stroke)   wnand 958
    Derive Nicod's axiom from the standard axioms   nic-justlem 960
    Derive the Lukasiewicz axioms from Nicod's axiom   nic-imp 970
Predicate calculus axiomatization
    The axioms of predicate calculus   wal 989
    Derive ax-4, ax-5o, and ax-6o   ax4 1007
Predicate calculus without distinct variables
    "Pure" predicate calculus ax-4, ax-5o, ax-6o, ax-gen   wex 1015
    Equality   ax9o 1157
    Axioms ax-10 and ax-11   ax10o 1175
    Substitution (without distinct variables)   wsbc 1206
    Theorems using axiom ax-11   equs5a 1233
Predicate calculus with distinct variables
    The axiom of quantifier introduction ax-17   a4imv 1243
    Derive the axiom of distinct variables ax-16   ax16 1245
    Derive the original axiom of variable substitution ax-11o   ax11o 1253
    Theorems without distinct variables that use axiom ax-11o   ax11b 1256
    Predicate calculus with distinct variables (cont.)   ax11v 1302
    More substitution theorems   sbhb 1366
    Existential uniqueness   weu 1418
ZF Set Theory - start with the Axiom of Extensionality
    Introduce the Axiom of Extensionality   ax-ext 1499
    Class abstractions (a.k.a. class builders)   cab 1504
    Negated equality and membership   wne 1627
    Restricted quantification   wral 1690
    The universal class   cvv 1856
    Russell's Paradox   ru 1983
    Proper substitution of classes for sets   sbhypf 1984
    Proper substitution of classes for sets into classes   csb 2050
    Define basic set operations and relations   cdif 2095
    Subclasses and subsets   dfss2 2109
    The difference, union, and intersection of two classes   difeq1 2204
    The empty set   c0 2331
    "Weak deduction theorem" for set theory   cif 2414
    Power classes   cpw 2457
    Unordered and ordered pairs   csn 2466
    The union of a class   cuni 2568
    The intersection of a class   cint 2599
    Indexed union and intersection   ciun 2632
    Binary relations   wbr 2691
    Ordered-pair class abstractions (class builders)   copab 2739
    Transitive classes   wtr 2753
ZF Set Theory - add the Axiom of Replacement
    Introduce the Axiom of Replacement   ax-rep 2766
    Derive the Axiom of Separation   axsep 2775
    Derive the Null Set Axiom   zfnuleu 2780
    Theorems requiring subset and intersection existence   nalset 2785
    Theorems requiring empty set existence   class2set 2807
ZF Set Theory - add the Axiom of Power Sets
    Introduce the Axiom of Power Sets   ax-pow 2817
    Derive the Axiom of Pairing   zfpair 2852
    Ordered pair theorem   opth1 2861
    Ordered-pair class abstractions (cont.)   opabid 2886
    Power class of union and intersection   pwin 2902
    Epsilon and identity relations   cep 2907
    Partial and complete ordering   wpo 2915
    Founded and well-ordering relations   wfr 2944
    Ordinals   word 2973
ZF Set Theory - add the Axiom of Union
    Introduce the Axiom of Union   ax-un 3088
    Ordinals (continued)   ordon 3140
    Transfinite induction   tfi 3206
    The natural numbers (i.e. finite ordinals)   com 3217
    Peano's postulates   peano1 3236
    Finite induction (for finite ordinals)   find 3242
    Functions and relations   cxp 3248
    Operations   co 4019
    "Maps to" notation   cmpt 4130
    First and second members of an ordered pair   c1st 4136
    Cantor's Theorem   canth 4203
    Miscellaneous ordinal theorems (that depend on functions and relations)   iunon 4205
    Transfinite recursion   tfrlem1 4210
    Recursive definition generator   crdg 4230
    Finite recursion   frfnom 4250
    Abian's "most fundamental" fixed point theorem   abianfplem 4260
    Ordinal arithmetic   c1o 4262
    Natural number arithmetic   nna0 4361
    Equivalence relations and classes   wer 4396
    The mapping operation   cm 4461
    Infinite Cartesian products   cixp 4486
    Equinumerosity   cen 4503
    Schroeder-Bernstein Theorem   sbthlem1 4590
    Pigeonhole Principle   phplem1 4653
    Finite sets   onomeneq 4663
    Supremum   csup 4714
ZF Set Theory - add the Axiom of Regularity
    Introduce the Axiom of Regularity   ax-reg 4734
    Axiom of Infinity equivalents   inf0 4749
ZF Set Theory - add the Axiom of Infinity
    Introduce the Axiom of Infinity   ax-inf 4765
    Existence of omega (the set of natural numbers)   omex 4770
    Rank   cr1 4785
    Scott's trick; collection principle; Hilbert's epsilon   scottex 4860
    Axiom of Choice equivalents   aceq1 4873
ZFC Set Theory - add the Axiom of Choice
    Introduce the Axiom of Choice   ax-ac 4888
    AC equivalents: well ordering, Zorn's lemma   numthlem 4927
    Cardinal numbers   ccrd 4957
    Cofinality   cflem 5053
    Cardinal number arithmetic   ccda 5065
    ZFC Axioms with no distinct variable requirements   nd1 5090
Real and complex numbers
    Dedekind-cut construction of real and complex numbers   cnpi 5124
    Real and complex number postulates   axaddopr 5417
    Real and complex numbers - basic operations   cmin 5444
    Some deductions from the field axioms for complex numbers   addcl 5453
    Addition   add12 5488
    Subtraction   cnegexlem1 5497
    Multiplication   mulid2 5569
    Infinity and the extended real number system   cpnf 5635
    Restate the ordering postulates with extended real "less than"   axlttri 5655
    Ordering on reals   lttr 5660
    Ordering on the extended reals   elxr 5687
    Ordering on reals (cont.)   eqle 5723
    Reciprocals   ixi 5835
    Division   df-div 5853
    Ordering on reals (cont.)   elimgt0 5947
    Natural numbers (as a subset of complex numbers)   df-n 6068
    Principle of mathematical induction   nnind 6080
    Natural numbers (cont.)   nn1suc 6082
    Decimal representation of numbers   c2 6105
    Some properties of specific numbers   2p2e4 6145
    Positive reals (as a subset of complex numbers)   df-rp 6189
    Completeness Axiom and Suprema   lbreu 6211
    Supremum on the extended reals   xrsupexmnf 6240
    Nonnegative integers (as a subset of complex numbers)   df-n0 6266
    Integers (as a subset of complex numbers)   df-z 6302
    Well-ordering principle for bounded-below sets of integers   uzwo3lem1 6386
    Rational numbers (as a subset of complex numbers)   df-q 6393
    The floor (greatest integer) function   cfl 6419
    The modulo (remainder) operation   cmo 6456
    Monotonic sequences   monoord 6480
    Real number intervals   cioo 6481
    Upper partititions of integers   cuz 6542
    Finite intervals of integers   cfz 6593
    The infinite sequence builder "seq1"   om2uz0i 6656
    The "shift" operation   cshi 6703
    Superior limit (lim sup)   clsp 6720
    Infinite sequence builders "seq" and "seq0"   cseqz 6724
    Integer powers   cexp 6761
    Discriminant   discrlem1 6855
    More natural number properties   nnsqcli 6859
    Ordered pair theorem for nonnegative integers   nn0le2msqi 6862
    Square root   csqr 6868
    Irrationality of square root of 2   sqr2irrlem1 6923
    Imaginary and complex number properties   irec 6930
    Real and imaginary parts; conjugate; absolute value   cre 6946
    Factorial function   cfa 7132
    The binomial coefficient operation   cbc 7157
    Limits   cli 7175
    Finite and infinite sums   csu 7180
    Finite sums (cont.)   dffsum 7199
    The binomial theorem   binomlem1 7267
    Limits (cont.)   clm1i 7278
    Infinite sums (cont.)   dfisum 7393
    Miscellaneous converging sequences   reccnv 7420
    Arithmetic series   arisumilem 7427
    Geometric series   expcnvlem1 7429
    Ratio test for infinite series convergence   cvgratlem1ALT 7450
    The product of two finite sums   fsum0diaglem1 7459
    Continuous complex functions   ccncf 7465
    Intermediate value theorem   ivthlem1 7484
    The exponential, sine, and cosine functions   ce 7496
    e is irrational   eirrlem1 7592
    The exponential, sine, and cosine functions (cont.)   abspef01tlubi 7601
Axiom of dependent choice
Cardinality and cardinal arithmetic (cont.)
    Countability of integers and rationals   nn0ennn 7707
    Infinite primes theorem   unbenlem 7714
    The reals are uncountable   ruclem1 7720
    Cardinal arithmetic (cont.)   infxpidmlem1 7762
    Continuum Hypothesis   gch-kn 7797
Topology
    Topological spaces   ctop 7798
    Bases for topologies   isbasisg 7821
    Subbases for topologies   subbas 7854
    Examples of topologies   subtop 7856
    Closure and interior   ccld 7868
    Neighborhoods   cnei 7920
    Limit points   clp 7948
    Continuity   ccn 7960
    Hausdorff spaces   cha 7989
Metric spaces
    Basic metric space properties   cme 7997
    Metric space balls   blfval 8043
    Open sets of a metric space   opnfval 8065
    Continuity in metric spaces   metcnpf 8092
    Examples of metric spaces   cnmetdval 8111
    Convergence and completeness   clm 8128
    Examples of complete metric spaces   cncms 8207
    Baire's Category Theorem   bcthlem1 8208
Group theory
    Definitions and basic properties for groups   cgr 8242
    Definition and basic properties of Abelian groups   cabl 8333
    Subgroups   csubg 8349
    Examples of groups   grpsn 8359
    Examples of Abelian groups   ablsn 8360
    Group homomorphism   ghgrpilem1 8368
Ring theory
    Definition and basic properties   cring 8374
    Examples of rings   cnring 8398
Division Rings
    Definition and basic properties   cdrng 8400
Star Fields
    Definition and basic properties   csfld 8403
Complex vector spaces
    Definition and basic properties   cvc 8405
    Examples of complex vector spaces   cnvc 8443
Normed complex vector spaces
    Definition and basic properties   cnv 8444
    Examples of normed complex vector spaces   cnnv 8548
    Induced metric of a normed complex vector space   imsval 8557
    Inner product   cip 8597
    Subspaces   css 8628
Operators on complex vector spaces
    Definitions and basic properties   clno 8649
Inner product (pre-Hilbert) spaces
    Definition and basic properties   cphl 8721
    Examples of pre-Hilbert spaces   cnph 8728
    Properties of pre-Hilbert spaces   isph 8731
Complex Banach spaces
    Definition and basic properties   cbn 8773
    Examples of complex Banach spaces   cnbn 8780
    Uniform Boundedness Theorem   ubthlem1 8781
    Minimizing Vector Theorem   minveclem1 8799
Complex Hilbert spaces
    Definition and basic properties   chl 8843
    Standard axioms for a complex Hilbert space   hlex 8856
    Examples of complex Hilbert spaces   cnhl 8874
    Subspaces   ssphl 8875
    Hellinger-Toeplitz Theorem   htthlem1 8876
Posets and lattices
    Definition and basic properties   cps 8889
Real and complex numbers (cont.)
    The exponential, sine, and cosine functions (cont.)   sincolem 8926
    Properties of pi = 3.14159...   pilem1 8932
    Mapping of the exponential function   efgh 8984
    The natural logarithm on complex numbers   clog 9015
ZFC Set Theory plus the Tarksi-Grothendieck Axiom
    Introduce the Tarksi-Grothendieck Axiom   ax-groth 9043
Humor
    April Fool's theorem   avril1 9052
Hilbert Space Explorer
    Preliminary ZFC lemmas   df-hnorm 9106
    Derive the Hilbert space axioms from ZFC set theory   axhilex 9120
    Introduce the vector space axioms for a Hilbert space   ax-hilex 9138
    Vector operations   hvmulex 9150
    Inner product postulates for a Hilbert space   ax-hfi 9216
    Inner product   his5 9223
    Norms   dfhnorm2 9258
    Relate Hilbert space to normed complex vector spaces   hilabl 9297
    Bunjakovaskij-Cauchy-Schwarz inequality   bcsiALT 9316
    Cauchy sequences and limits   hcau 9321
    Derivation of the completeness axiom from ZF set theory   hilmet 9331
    Completeness postulate for a Hilbert space   ax-hcompl 9341
    Relate Hilbert space to ZFC pre-Hilbert and Hilbert spaces   hhcms 9342
    Subspaces   df-sh 9346
    Closed subspaces   df-ch 9362
    Orthocomplements   df-oc 9394
    Projection theorem   projlem1 9456
    Projectors   df-pj 9507
    Orthomodular law   omlsilem 9514
    Projectors (cont.)   pjtheu2i 9520
    Subspace sum, span, lattice join, lattice supremum   df-shsum 9543
    Hilbert lattice operations   sh0le 9634
    Span (cont.) and one-dimensional subspaces   spansn0 9734
    Operator sum, difference, and scalar multiplication   df-hosum 9776
    Commutes relation for Hilbert lattice elements   df-cm 9796
    Foulis-Holland theorem   fh1 9831
    Quantum Logic Explorer axioms   qlax1i 9840
    Orthogonal subspaces   osumlem1 9850
    Orthoarguesian laws 5OA and 3OA   5oalem1 9871
    Projectors (cont.)   pjorthi 9886
    Mayet's equation E_3   mayete3i 9945
    Zero and identity operators   df-h0op 9948
    Operations on Hilbert space operators   hoaddcl 9958
    Linear, continuous, bounded, Hermitian, unitary operators and norms   df-nmop 10039
    Linear and continuous functionals and norms   df-nmfn 10045
    Adjoint   df-adjh 10049
    Dirac bra-ket notation   df-bra 10050
    Positive operators   df-leop 10052
    Eigenvectors, eigenvalues, spectrum   df-eigvec 10053
    Theorems about operators and functionals   nmopval 10056
    Riesz lemma   riesz3i 10268
    Adjoints (cont.)   cnlnadjlem1 10273
    Quantum computation error bound theorem   unierri 10310
    Dirac bra-ket notation (cont.)   branmfn 10311
    Positive operators (cont.)   leopg 10329
    Projectors as operators   pjhmopi 10347
    States on a Hilbert lattice   df-st 10414
    Godowski's equation   golem1 10473
    Covering relation; modular pairs   df-cv 10481
    Atoms   df-at 10540
    Superposition principle   superpos 10556
    Atoms, exchange and covering properties, atomicity   chcv1 10557
    Irreducibility   irredlem1 10593
    Atoms (cont.)   atcvat3i 10599
    Modular symmetry   mdsymlem1 10606
Mathboxes for user contributions
    Mathbox guidelines   mathbox 10645
Mathbox for Stefan Allan
Mathbox for Paul Chapman
    Miscellaneous theorems   lemul2aALT 10649
    Group homomorphism and isomorphism   cghom 10657
    Symmetry groups and Cayley's Theorem   csymgrp 10678
Mathbox for Jeff Hoffman
    Inferences for finite induction on generic function values   fveleq 10694
    gdc.mm   nnssi2 10698
Mathbox for Frédéric Liné
    Propositional and predicate calculus   ahypfmbi 10705
    General Set theory   ntunte 10719
    Lattice (algebraic definition)   clatalg 10814
    Currying   ccur1 10827
    Finite intersection stuff using function fi   cfi 10831
    Order theory   ccha 10839
    Operation properties   ccm1 10867
    Groups and related structures   rrisgrp 10878
    Fields and Rings of various species   relrng 10919
    R-modules and K-vector spaces   cvec 10936
    Real vector spaces   cvr 10938
    Matrices   cmat 10942
    Affine spaces   raffsp 10950
    Intervals of reals and of extended reals   iooirrsa 10952
    Topology   empntop 10967
    Continuous functions   cnrsfin 10972
    Homeomorphisms   chomeosm 10979
    Initial and final topologies   csubsp 11018
    Filters   cfil 11033
    Limits   cflim1 11060
    Separated spaces: T0, T1, T2 (Hausdorff) ...   ct0 11068
    Compactness   ccomp 11078
    Connectedness   ccon 11090
    Standard topology on RR   clicls 11104
    Standard topology of intervals of RR   stoi 11111
    Pre-calculus and Cartesian geometry   dmse1 11112
    Directed multi graphs   cmgra 11128
    Category and deductive system underlying "structure"   calg 11131
    Deductive systems   cded 11154
    Categories   ccat 11172
    Homsets   chom 11202
    Monomorphisms, Epimorphisms, Isomorphisms   cepi 11220
    Functors   cfunc 11247
    Subcategories   csubc 11259
    Tarski's classes and ranks   csubcl 11276
    Planar incidence geometry   cplig 11279
Mathbox for Jeff Hankins
    Miscellany   3syld 11286
    Ordinal isomorphism, Hartog's theorem   ordiso 11386
    Basic topological facts   fibas 11413
    Subspaces of metric space topologies   subtopmetlem 11457
    Topology of the real numbers   reconnlem1 11459
    First- and second-countability, refinements   c1stc 11468
    Neighborhood bases determine topologies   neibastop1 11498
    Lattice structure of topologies   topmtcl 11505
    Filter bases   cfbas 11512
    Ultrafilters   cufil 11540
    Filter limits   cfilmap 11558
    Directed sets, nets   cdir 11636
    Group actions   cga 11660
Mathbox for Jeff Madsen
    Logic and set theory   sylancr 11676
    Real and complex numbers; integers   fimaxre 11749
    Sequences and sums   sdclem1 11768
    Topology   unopn 11791
    Metric spaces   metf1o 11800
    Intervals   iccsplit 11812
    Continuous maps and homeomorphisms   constcncf 11837
    Topological limits   ctlm 11855
    Product topologies   ctx 11863
    Boundedness   ctotbnd 11879
    Isometries   cismty 11894
    Heine-Borel Theorem   heiborlem1 11904
    Banach Fixed Point Theorem   bfplem1 11947
    Euclidean space   recms 11959
    Intervals (continued)   ismrer1 11973
    Path homotopy   cphtpy 11978
Mathbox for Norm Megill
    Axioms for quantum logic system Q3   ax-q1 11998
    Preliminary lemmas to justify definitions   qsyl 12012
    Definitions   df-qora 12016
    Basic theorems   q2th 12020
Mathbox for Steve Rodriguez
    Hypergraphs   chgra 12084
    Examples of hypergraphs   emhgrat 12094
    Pseudographs   cpgra 12096
    Simple graphs   csgra 12099
Mathbox for Alan Sare

Statement List for Metamath Proof Explorer - 1-100 - Page 1 of 122
TypeLabelDescription
Statement
 
Pre-logic
 
Dummy link theorem for assisting proof development
 
Theoremdummylink 1 (Note: This theorem will never appear in a completed proof and can be ignored if you are using this database to learn logic - please start with the next statement, wn 2.)

This is a technical theorem to assist proof development. It provides a temporary way to add an independent subproof to a proof under development, for later assignment to a normal proof step.

The Metamath program's Proof Assistant requires proofs to be developed backwards from the conclusion with no gaps, and it has no mechanism that lets the user to work on isolated subproofs. This theorem provides a workaround for this limitation. It can be inserted at any point in a proof to allow an independent subproof to be developed on the side, for later use as part of the final proof.

Instructions: (1) Assign this theorem to any unknown step in the proof. Typically, the last unknown step is the most convenient, since 'assign last' can be used. This step will be replicated in hypothesis dummylink.1, from where the development of the main proof can continue. (2) Develop the independent subproof backwards from hypothesis dummylink.2. If desired, use a 'let' command to pre-assign the conclusion of the independent subproof to dummylink.2. (3) After the independent subproof is complete, use 'improve all' to assign it automatically to an unknown step in the main proof that matches it. (4) After the entire proof is complete, use 'minimize */n/b/e 3syl,we?,wsb' to clean up (discard) all dummylink references automatically.

This theorem was originally designed to assist importing partially completed Proof Worksheets from Mel O'Cat's mmj2 Proof Assistant GUI, but it can also be useful on its own. Interestingly, this "theorem" - or more precisely, inference - requires no axioms for its proof.

|- ph   &   |- ps   =>   |- ph
 
Propositional calculus
 
Recursively define primitive wffs for propositional calculus
 
Syntaxwn 2 If ph is a wff, so is -. ph or "not ph." Part of the recursive definition of a wff (well-formed formula). In classical logic (which is our logic), a wff is interpreted as either true or false. So if ph is true, then -. ph is false; if ph is false, then -. ph is true. Traditionally, Greek letters are used to represent wffs, and we follow this convention. In propositional calculus, we define only wffs built up from other wffs, i.e. there is no starting or "atomic" wff. Later, in predicate calculus, we will extend the basic wff definition by including atomic wffs (weq 992 and wel 994).
wff -. ph
 
Syntaxwi 3 If ph and ps are wff's, so is (ph -> ps) or "ph implies ps." Part of the recursive definition of a wff. The resulting wff is (interpreted as) false when ph is true and ps is false; it is true otherwise. (Think of the truth table for an OR gate with input ph connected through an inverter.) The left-hand wff is called the antecedent, and the right-hand wff is called the consequent. In the case of (ph -> (ps -> ch)), the middle ps may be informally called either an antecedent or part of the consequent depending on context.
wff (ph -> ps)
 
The axioms of propositional calculus
 
Axiomax-1 4 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 ph and ps to the assertion of ph 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.

|- (ph -> (ps -> ph))
 
Axiomax-2 5 Axiom Frege. Axiom A2 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. It "distributes" an antecedent over two consequents. This axiom was part of Frege's original system and is known as Frege in the literature. It is also proved as Theorem *2.77 of [WhiteheadRussell] p. 108. The other direction of this axiom also turns out to be true, as demonstrated by pm5.41 167.
|- ((ph -> (ps -> ch)) -> ((ph -> ps) -> (ph -> ch)))
 
Axiomax-3 6 Axiom Transp. Axiom A3 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. It swaps or "transposes" the order of the consequents when negation is removed. An informal example is that the statement "if there are no clouds in the sky, it is not raining" implies the statement "if it is raining, there are clouds in the sky." This axiom is called Transp or "the principle of transposition" in Principia Mathematica (Theorem *2.17 of [WhiteheadRussell] p. 103). We will also use the term "contraposition" for this principle, although the reader is advised that in the field of philosophical logic, "contraposition" has a different technical meaning.
|- ((-. ph -> -. ps) -> (ps -> ph))
 
Axiomax-mp 7 Rule of Modus Ponens. The postulated inference rule of propositional calculus. See e.g. Rule 1 of [Hamilton] p. 73. The rule says, "if ph is true, and ph implies ps, then ps must also be true." This rule is sometimes called "detachment," since it detaches the minor premise from the major premise.

Note: In some web page displays such as the Statement List, the symbols "&" and "=>" informally indicate the relationship between the hypotheses and the assertion (conclusion), abbreviating the English words "and" and "implies." They are not part of the formal language.

|- ph   &   |- (ph -> ps)   =>   |- ps
 
Logical implication
 
Theorema1i 8 Inference derived from axiom ax-1 4. See a1d 12 for an explanation of our informal use of the terms "inference" and "deduction." See also the comment in syld 27.
|- ph   =>   |- (ps -> ph)
 
Theorema2i 9 Inference derived from axiom ax-2 5.
|- (ph -> (ps -> ch))   =>   |- ((ph -> ps) -> (ph -> ch))
 
Theoremsyl 10 An inference version of the transitive laws for implication imim2 14 and imim1 15, which Russell and Whitehead call "the principle of the syllogism...because...the syllogism in Barbara is derived from them" (quote after Theorem *2.06 of [WhiteheadRussell] p. 101). Some authors call this law a "hypothetical syllogism."

(A bit of trivia: this is the most commonly referenced assertion in our database. In second place is ax-mp 7, followed by visset 1858, bitri 171, imp 348, and ex 371. The Metamath program command 'show usage' shows the number of references.)

|- (ph -> ps)   &   |- (ps -> ch)   =>   |- (ph -> ch)
 
Theoremcom12 11 Inference that swaps (commutes) antecedents in an implication.
|- (ph -> (ps -> ch))   =>   |- (ps -> (ph -> ch))
 
Theorema1d 12 Deduction introducing an embedded antecedent. (The proof was revised by Stefan Allan, 20-Mar-2006.)

Naming convention: We often call a theorem a "deduction" and suffix its label with "d" whenever the hypotheses and conclusion are each prefixed with the same antecedent. This allows us to use the theorem in places where (in traditional textbook formalizations) the standard Deduction Theorem would be used; here ph would be replaced with a conjunction (df-an 223) of the hypotheses of the would-be deduction. By contrast, we tend to call the simpler version with no common antecedent an "inference" and suffix its label with "i"; compare theorem a1i 8. Finally, a "theorem" would be the form with no hypotheses; in this case the "theorem" form would be the original axiom ax-1 4. We usually show the theorem form without a suffix on its label (e.g. pm2.43 63 vs. pm2.43i 64 vs. pm2.43d 65). When an inference is converted to a theorem by eliminating an "is a set" hypothesis, we sometimes suffix the theorem form with "g" (for "more general") as in uniex 3092 vs. uniexg 3093.

|- (ph -> ps)   =>   |- (ph -> (ch -> ps))
 
Theorema2d 13 Deduction distributing an embedded antecedent.
|- (ph -> (ps -> (ch -> th)))   =>   |- (ph -> ((ps -> ch) -> (ps -> th)))
 
Theoremimim2 14 A closed form of syllogism (see syl 10). Theorem *2.05 of [WhiteheadRussell] p. 100.
|- ((ph -> ps) -> ((ch -> ph) -> (ch -> ps)))
 
Theoremimim1 15 A closed form of syllogism (see syl 10). Theorem *2.06 of [WhiteheadRussell] p. 100.
|- ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))
 
Theoremimim1i 16 Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent.
|- (ph -> ps)   =>   |- ((ps -> ch) -> (ph -> ch))
 
Theoremimim2i 17 Inference adding common antecedents in an implication.
|- (ph -> ps)   =>   |- ((ch -> ph) -> (ch -> ps))
 
Theoremimim12i 18 Inference joining two implications.
|- (ph -> ps)   &   |- (ch -> th)   =>   |- ((ps -> ch) -> (ph -> th))
 
Theoremimim3i 19 Inference adding three nested antecedents.
|- (ph -> (ps -> ch))   =>   |- ((th -> ph) -> ((th -> ps) -> (th -> ch)))
 
Theorem3syl 20 Inference chaining two syllogisms.
|- (ph -> ps)   &   |- (ps -> ch)   &   |- (ch -> th)   =>   |- (ph -> th)
 
Theoremsyl5 21 A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise.
|- (ph -> (ps -> ch))   &   |- (th -> ps)   =>   |- (ph -> (th -> ch))
 
Theoremsyl6 22 A syllogism rule of inference. The second premise is used to replace the consequent of the first premise.
|- (ph -> (ps -> ch))   &   |- (ch -> th)   =>   |- (ph -> (ps -> th))
 
Theoremsyl7 23 A syllogism rule of inference. The second premise is used to replace the third antecedent of the first premise.
|- (ph -> (ps -> (ch -> th)))   &   |- (ta -> ch)   =>   |- (ph -> (ps -> (ta -> th)))
 
Theoremsyl8 24 A syllogism rule of inference. The second premise is used to replace the consequent of the first premise.
|- (ph -> (ps -> (ch -> th)))   &   |- (th -> ta)   =>   |- (ph -> (ps -> (ch -> ta)))
 
Theoremimim2d 25 Deduction adding nested antecedents.
|- (ph -> (ps -> ch))   =>   |- (ph -> ((th -> ps) -> (th -> ch)))
 
Theoremmpd 26 A modus ponens deduction.
|- (ph -> ps)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> ch)
 
Theoremsyld 27 Syllogism deduction. (The proof was shortened by O'Cat, 19-Feb-2008.)

Notice that syld 27 can be obtained from syl 10 by replacing each hypothesis and conclusion ta by (ph -> ta). In general, this process will always yield a new propositional calculus theorem because of something called the Deduction Theorem for propositional calculus.

|- (ph -> (ps -> ch))   &   |- (ph -> (ch -> th))   =>   |- (ph -> (ps -> th))
 
Theoremimim1d 28 Deduction adding nested consequents.
|- (ph -> (ps -> ch))   =>   |- (ph -> ((ch -> th) -> (ps -> th)))
 
Theoremimim12d 29 Deduction combining antecedents and consequents.
|- (ph -> (ps -> ch))   &   |- (ph -> (th -> ta))   =>   |- (ph -> ((ch -> th) -> (ps -> ta)))
 
Theorempm2.04 30 Swap antecedents. Theorem *2.04 of [WhiteheadRussell] p. 100.
|- ((ph -> (ps -> ch)) -> (ps -> (ph -> ch)))
 
Theorempm2.83 31 Theorem *2.83 of [WhiteheadRussell] p. 108.
|- ((ph -> (ps -> ch)) -> ((ph -> (ch -> th)) -> (ph -> (ps -> th))))
 
Theoremcom23 32 Commutation of antecedents. Swap 2nd and 3rd.
|- (ph -> (ps -> (ch -> th)))   =>   |- (ph -> (ch -> (ps -> th)))
 
Theoremcom13 33 Commutation of antecedents. Swap 1st and 3rd.
|- (ph -> (ps -> (ch -> th)))   =>   |- (ch -> (ps -> (ph -> th)))
 
Theoremcom3l 34 Commutation of antecedents. Rotate left.
|- (ph -> (ps -> (ch -> th)))   =>   |- (ps -> (ch -> (ph -> th)))
 
Theoremcom3r 35 Commutation of antecedents. Rotate right.
|- (ph -> (ps -> (ch -> th)))   =>   |- (ch -> (ph -> (ps -> th)))
 
Theoremcom34 36 Commutation of antecedents. Swap 3rd and 4th.
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (ph -> (ps -> (th -> (ch -> ta))))
 
Theoremcom24 37 Commutation of antecedents. Swap 2nd and 4th.
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (ph -> (th -> (ch -> (ps -> ta))))
 
Theoremcom14 38 Commutation of antecedents. Swap 1st and 4th.
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (th -> (ps -> (ch -> (ph -> ta))))
 
Theoremcom4l 39 Commutation of antecedents. Rotate left. (The proof was shortened by O'Cat, 15-Aug-2004.)
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (ps -> (ch -> (th -> (ph -> ta))))
 
Theoremcom4t 40 Commutation of antecedents. Rotate twice.
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (ch -> (th -> (ph -> (ps -> ta))))
 
Theoremcom4r 41 Commutation of antecedents. Rotate right.
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (th -> (ph -> (ps -> (ch -> ta))))
 
Theorema1dd 42 Deduction introducing a nested embedded antecedent. (The proof was shortened by O'Cat, 15-Jan-2008.)
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> (th -> ch)))
 
Theoremmp2 43 A double modus ponens inference.
|- ph   &   |- ps   &   |- (ph -> (ps -> ch))   =>   |- ch
 
Theoremmpi 44 A nested modus ponens inference. (The proof was shortened by Stefan Allan, 20-Mar-2006.)
|- ps   &   |- (ph -> (ps -> ch))   =>   |- (ph -> ch)
 
Theoremmpii 45 A doubly nested modus ponens inference.
|- ch   &   |- (ph -> (ps -> (ch -> th)))   =>   |- (ph -> (ps -> th))
 
Theoremmpdd 46 A nested modus ponens deduction.
|- (ph -> (ps -> ch))   &   |- (ph -> (ps -> (ch -> th)))   =>   |- (ph -> (ps -> th))
 
Theoremmpid 47 A nested modus ponens deduction.
|- (ph -> ch)   &   |- (ph -> (ps -> (ch -> th)))   =>   |- (ph -> (ps -> th))
 
Theoremmpdi 48 A nested modus ponens deduction. (The proof was shortened by O'Cat, 15-Jan-2008.)
|- (ps -> ch)   &   |- (ph -> (ps -> (ch -> th)))   =>   |- (ph -> (ps -> th))
 
Theoremmpcom 49 Modus ponens inference with commutation of antecedents.
|- (ps -> ph)   &   |- (ph -> (ps -> ch))   =>   |- (ps -> ch)
 
Theoremsyldd 50 Nested syllogism deduction.
|- (ph -> (ps -> (ch -> th)))   &   |- (ph -> (ps -> (th -> ta)))   =>   |- (ph -> (ps -> (ch -> ta)))
 
Theoremsylcom 51 Syllogism inference with commutation of antecedents. (The proof was shortened by O'Cat, 2-Feb-2006 and shortened further by Stefan Allan, 23-Feb-2006.)
|- (ph -> (ps -> ch))   &   |- (ps -> (ch -> th))   =>   |- (ph -> (ps -> th))
 
Theoremsyl5com 52 Syllogism inference with commuted antecedents.
|- (ph -> (ps -> ch))   &   |- (th -> ps)   =>   |- (th -> (ph -> ch))
 
Theoremsyl6com 53 Syllogism inference with commuted antecedents.
|- (ph -> (ps -> ch))   &   |- (ch -> th)   =>   |- (ps -> (ph -> th))
 
Theoremsyli 54 Syllogism inference with common nested antecedent.
|- (ps -> (ph -> ch))   &   |- (ch -> (ph -> th))   =>   |- (ps -> (ph -> th))
 
Theoremsyl5d 55 A nested syllogism deduction. (The proof was shortened by Josh Purinton, 29-Dec-2000 and shortened further by O'Cat, 2-Feb-2006.)
|- (ph -> (ps -> (ch -> th)))   &   |- (ph -> (ta -> ch))   =>   |- (ph -> (ps -> (ta -> th)))
 
Theoremsyl6d 56 A nested syllogism deduction. (The proof was shortened by Josh Purinton, 29-Dec-2000 and shortened further by O'Cat, 2-Feb-2006.)
|- (ph -> (ps -> (ch -> th)))   &   |- (ph -> (th -> ta))   =>   |- (ph -> (ps -> (ch -> ta)))
 
Theoremsyl9 57 A nested syllogism inference with different antecedents. (The proof was shortened by Josh Purinton, 29-Dec-2000.)
|- (ph -> (ps -> ch))   &   |- (th -> (ch -> ta))   =>   |- (ph -> (th -> (ps -> ta)))
 
Theoremsyl9r 58 A nested syllogism inference with different antecedents.
|- (ph -> (ps -> ch))   &   |- (th -> (ch -> ta))   =>   |- (th -> (ph -> (ps -> ta)))
 
Theoremid 59 Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see id1 60. (The proof was shortened by Stefan Allan, 20-Mar-2006.)
|- (ph -> ph)
 
Theoremid1 60 Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. This version is proved directly from the axioms for demonstration purposes. This proof is a popular example in the literature and is identical, step for step, to the proofs of Theorem 1 of [Margaris] p. 51, Example 2.7(a) of [Hamilton] p. 31, Lemma 10.3 of [BellMachover] p. 36, and Lemma 1.8 of [Mendelson] p. 36. It is also "Our first proof" in Hirst and Hirst's A Primer for Logic and Proof p. 16 (PDF p. 22) at http://www.mathsci.appstate.edu/~jlh/primer/hirst.pdf. For a shorter version of the proof that takes advantage of previously proved theorems, see id 59.
|- (ph -> ph)
 
Theoremidd 61 Principle of identity with antecedent.
|- (ph -> (ps -> ps))
 
Theorempm2.27 62 This theorem, called "Assertion," can be thought of as closed form of modus ponens ax-mp 7. Theorem *2.27 of [WhiteheadRussell] p. 104.
|- (ph -> ((ph -> ps) -> ps))
 
Theorempm2.43 63 Absorption of redundant antecedent. Also called the "Contraction" or "Hilbert" axiom. Theorem *2.43 of [WhiteheadRussell] p. 106. (The proof was shortened by O'Cat, 15-Aug-2004.)
|- ((ph -> (ph -> ps)) -> (ph -> ps))
 
Theorempm2.43i 64 Inference absorbing redundant antecedent. (The proof was shortened by O'Cat, 28-Nov-2008.)
|- (ph -> (ph -> ps))   =>   |- (ph -> ps)
 
Theorempm2.43d 65 Deduction absorbing redundant antecedent. (The proof was shortened by O'Cat, 28-Nov-2008.)
|- (ph -> (ps -> (ps -> ch)))   =>   |- (ph -> (ps -> ch))
 
Theorempm2.43a 66 Inference absorbing redundant antecedent. (The proof was shortened by O'Cat, 28-Nov-2008.)
|- (ps -> (ph -> (ps -> ch)))   =>   |- (ps -> (ph -> ch))
 
Theorempm2.43b 67 Inference absorbing redundant antecedent.
|- (ps -> (ph -> (ps -> ch)))   =>   |- (ph -> (ps -> ch))
 
Theoremsylc 68 A syllogism inference combined with contraction.
|- (ph -> (ps -> ch))   &   |- (th -> ph)   &   |- (th -> ps)   =>   |- (th -> ch)
 
Theorempm2.86 69 Converse of axiom ax-2 5. Theorem *2.86 of [WhiteheadRussell] p. 108.
|- (((ph -> ps) -> (ph -> ch)) -> (ph -> (ps -> ch)))
 
Theorempm2.86i 70 Inference based on pm2.86 69.
|- ((ph -> ps) -> (ph -> ch))   =>   |- (ph -> (ps -> ch))
 
Theorempm2.86d 71 Deduction based on pm2.86 69.
|- (ph -> ((ps -> ch) -> (ps -> th)))   =>   |- (ph -> (ps -> (ch -> th)))
 
Theoremloolin 72 The Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. (Contributed by O'Cat, 12-Aug-2004.)
|- (((ph -> ps) -> (ps -> ph)) -> (ps -> ph))
 
Theoremloowoz 73 An alternate for the Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz, due to Barbara Wozniakowska, Reports on Mathematical Logic 10, 129-137 (1978). (Contributed by O'Cat, 8-Aug-2004.)
|- (((ph -> ps) -> (ph -> ch)) -> ((ps -> ph) -> (ps -> ch)))
 
Logical negation
 
Theoremcon4i 74 Inference rule derived from axiom ax-3 6.
|- (-. ph -> -. ps)   =>   |- (ps -> ph)
 
Theoremcon4d 75 Deduction derived from axiom ax-3 6.
|- (ph -> (-. ps -> -. ch))   =>   |- (ph -> (ch -> ps))
 
Theorempm2.21 76 From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law.
|- (-. ph -> (ph -> ps))
 
Theorempm2.21i 77 A contradiction implies anything. Inference from pm2.21 76.
|- -. ph   =>   |- (ph -> ps)
 
Theorempm2.21d 78 A contradiction implies anything. Deduction from pm2.21 76.
|- (ph -> -. ps)   =>   |- (ph -> (ps -> ch))
 
Theorempm2.24 79 Theorem *2.24 of [WhiteheadRussell] p. 104.
|- (ph -> (-. ph -> ps))
 
Theorempm2.24ii 80 A contradiction implies anything. Inference from pm2.24 79.
|- ph   &   |- -. ph   =>   |- ps
 
Theorempm2.18 81 Proof by contradiction. Theorem *2.18 of [WhiteheadRussell] p. 103. Also called the Law of Clavius.
|- ((-. ph -> ph) -> ph)
 
Theorempeirce 82 Peirce's axiom. This odd-looking theorem is the "difference" between an intuitionistic system of propositional calculus and a classical system and is not accepted by intuitionists. When Peirce's axiom is added to an intuitionistic system, the system becomes equivalent to our classical system ax-1 4 through ax-3 6. A curious fact about this theorem is that it requires ax-3 6 for its proof even though the result has no negation connectives in it.
|- (((ph -> ps) -> ph) -> ph)
 
Theoremlooinv 83 The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. Using dfor2 227, we can see that this essentially expresses "disjunction commutes." Theorem *2.69 of [WhiteheadRussell] p. 108.
|- (((ph -> ps) -> ps) -> ((ps -> ph) -> ph))
 
Theoremnotnot2 84 Converse of double negation. Theorem *2.14 of [WhiteheadRussell] p. 102. (The proof was shortened by David Harvey, 5-Sep-1999. An even shorter proof found by Josh Purinton, 29-Dec-2000.)
|- (-. -. ph -> ph)
 
Theoremnotnotri 85 Inference from double negation.
|- -. -. ph   =>   |- ph
 
Theoremnotnot1 86 Converse of double negation. Theorem *2.12 of [WhiteheadRussell] p. 101.
|- (ph -> -. -. ph)
 
Theoremnotnoti 87 Infer double negation.
|- ph   =>   |- -. -. ph
 
Theorempm2.01 88 Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. (The proof was shortened by O'Cat, 21-Nov-2008.
|- ((ph -> -. ph) -> -. ph)
 
Theorempm2.01d 89 Deduction based on reductio ad absurdum.
|- (ph -> (ps -> -. ps))   =>   |- (ph -> -. ps)
 
Theoremcon2 90 Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100.
|- ((ph -> -. ps) -> (ps -> -. ph))
 
Theoremcon2d 91 A contraposition deduction.
|- (ph -> (ps -> -. ch))   =>   |- (ph -> (ch -> -. ps))
 
Theoremcon1 92 Contraposition. Theorem *2.15 of [WhiteheadRussell] p. 102.
|- ((-. ph -> ps) -> (-. ps -> ph))
 
Theoremcon1d 93 A contraposition deduction.
|- (ph -> (-. ps -> ch))   =>   |- (ph -> (-. ch -> ps))
 
Theoremcon3 94 Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103.
|- ((ph -> ps) -> (-. ps -> -. ph))
 
Theoremcon3d 95 A contraposition deduction.
|- (ph -> (ps -> ch))   =>   |- (ph -> (-. ch -> -. ps))
 
Theoremcon1i 96 A contraposition inference. (The proof was shortened by O'Cat, 28-Nov-2008.)
|- (-. ph -> ps)   =>   |- (-. ps -> ph)
 
Theoremcon2i 97 A contraposition inference. (The proof was shortened by O'Cat, 28-Nov-2008.)
|- (ph -> -. ps)   =>   |- (ps -> -. ph)
 
Theoremcon3i 98 A contraposition inference.
|- (ph -> ps)   =>   |- (-. ps -> -. ph)
 
Theorempm2.5 99 Theorem *2.5 of [WhiteheadRussell] p. 107.
|- (-. (ph -> ps) -> (-. ph -> ps))
 
Theorempm2.51 100 Theorem *2.51 of [WhiteheadRussell] p. 107.
|- (-. (ph -> ps) -> (ph -> -. ps))

MPE Home   Contents Copyright terms: Public domain < Wrap  Next >