HomeHome Intuitionistic Logic Explorer
Theorem List (Table of Contents)
< Wrap  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page:  Detailed Table of Contents  Page List

Table of Contents Summary
PART 1  FIRST ORDER LOGIC WITH EQUALITY
      1.1  Pre-logic
      1.2  Propositional calculus
      1.3  Predicate calculus mostly without distinct variables
      1.4  Predicate calculus with distinct variables
PART 2  SET THEORY
      2.1  IZF Set Theory - start with the Axiom of Extensionality
      2.2  IZF Set Theory - add the Axioms of Collection and Separation
      2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
      2.4  IZF Set Theory - add the Axiom of Union
      2.5  IZF Set Theory - add the Axiom of Set Induction
      2.6  IZF Set Theory - add the Axiom of Infinity
PART 3  REAL AND COMPLEX NUMBERS
      3.1  Construction and axiomatization of real and complex numbers
      3.2  Derive the basic properties from the field axioms
      3.3  Real and complex numbers - basic operations
PART 4  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
      4.1  Mathboxes for user contributions
      4.2  Mathbox for Mykola Mostovenko
      4.3  Mathbox for BJ
      4.4  Mathbox for David A. Wheeler

Detailed Table of Contents
(* means the section header has a description)
PART 1  FIRST ORDER LOGIC WITH EQUALITY
      1.1  Pre-logic
            1.1.1  Inferences for assisting proof development   dummylink 1
      1.2  Propositional calculus
            1.2.1  Recursively define primitive wffs for propositional calculus   wn 3
            1.2.2  Propositional logic axioms for implication   ax-1 5
            *1.2.3  Logical implication   mp2b 8
            1.2.4  Logical conjunction and logical equivalence   wa 97
            1.2.5  Logical negation (intuitionistic)   ax-in1 532
            1.2.6  Logical disjunction   wo 616
            1.2.7  Stable propositions   wstab 727
            1.2.8  Decidable propositions   wdc 730
            *1.2.9  Theorems of decidable propositions   condc 737
            1.2.10  Testable propositions   dftest 810
            1.2.11  Miscellaneous theorems of propositional calculus   pm5.21nd 813
            1.2.12  Abbreviated conjunction and disjunction of three wff's   w3o 870
            1.2.13  True and false constants   wal 1224
                  *1.2.13.1  Universal quantifier for use by df-tru   wal 1224
                  *1.2.13.2  Equality predicate for use by df-tru   cv 1225
                  1.2.13.3  Define the true and false constants   wtru 1227
            1.2.14  Logical 'xor'   wxo 1249
            *1.2.15  Truth tables: Operations on true and false constants   truantru 1273
            *1.2.16  Stoic logic indemonstrables (Chrysippus of Soli)   mpto1 1295
            1.2.17  Logical implication (continued)   syl6an 1299
      1.3  Predicate calculus mostly without distinct variables
            *1.3.1  Universal quantifier (continued)   ax-5 1312
            *1.3.2  Equality predicate (continued)   weq 1369
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1396
            1.3.4  Introduce Axiom of Existence   ax-i9 1400
            1.3.5  Additional intuitionistic axioms   ax-ial 1405
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1407
            1.3.7  The existential quantifier   19.8a 1460
            1.3.8  Equality theorems without distinct variables   a9e 1564
            1.3.9  Axioms ax-10 and ax-11   ax10o 1581
            1.3.10  Substitution (without distinct variables)   wsb 1623
            1.3.11  Theorems using axiom ax-11   equs5a 1653
      1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1670
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1681
            1.4.3  More theorems related to ax-11 and substitution   albidv 1683
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1716
            1.4.5  More substitution theorems   hbs1 1792
            1.4.6  Existential uniqueness   weu 1878
            *1.4.7  Aristotelian logic: Assertic syllogisms   barbara 1976
*PART 2  SET THEORY
      2.1  IZF Set Theory - start with the Axiom of Extensionality
            2.1.1  Introduce the Axiom of Extensionality   ax-ext 2000
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2004
            2.1.3  Class form not-free predicate   wnfc 2143
            2.1.4  Negated equality and membership   wne 2182
                  2.1.4.1  Negated equality   neii 2186
                  2.1.4.2  Negated membership   neli 2273
            2.1.5  Restricted quantification   wral 2280
            2.1.6  The universal class   cvv 2531
            *2.1.7  Conditional equality (experimental)   wcdeq 2720
            2.1.8  Russell's Paradox   ru 2736
            2.1.9  Proper substitution of classes for sets   wsbc 2737
            2.1.10  Proper substitution of classes for sets into classes   csb 2825
            2.1.11  Define basic set operations and relations   cdif 2887
            2.1.12  Subclasses and subsets   df-ss 2904
            2.1.13  The difference, union, and intersection of two classes   difeq1 3028
                  2.1.13.1  The difference of two classes   difeq1 3028
                  2.1.13.2  The union of two classes   elun 3057
                  2.1.13.3  The intersection of two classes   elin 3099
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3140
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3176
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3190
            2.1.14  The empty set   c0 3197
            2.1.15  Conditional operator   cif 3306
            2.1.16  Power classes   cpw 3330
            2.1.17  Unordered and ordered pairs   csn 3346
            2.1.18  The union of a class   cuni 3550
            2.1.19  The intersection of a class   cint 3585
            2.1.20  Indexed union and intersection   ciun 3627
            2.1.21  Disjointness   wdisj 3715
            2.1.22  Binary relations   wbr 3734
            2.1.23  Ordered-pair class abstractions (class builders)   copab 3787
            2.1.24  Transitive classes   wtr 3824
      2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 3842
            2.2.2  Introduce the Axiom of Separation   ax-sep 3845
            2.2.3  Derive the Null Set Axiom   zfnuleu 3851
            2.2.4  Theorems requiring subset and intersection existence   nalset 3857
            2.2.5  Theorems requiring empty set existence   class2seteq 3886
            2.2.6  Collection principle   bnd 3895
      2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 3897
            2.3.2  Axiom of Pairing   ax-pr 3914
            2.3.3  Ordered pair theorem   opm 3941
            2.3.4  Ordered-pair class abstractions (cont.)   opabid 3964
            2.3.5  Power class of union and intersection   pwin 3989
            2.3.6  Epsilon and identity relations   cep 3994
            2.3.7  Partial and complete ordering   wpo 4001
            2.3.8  Set-like relations   wse 4034
            2.3.9  Ordinals   word 4044
      2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4116
            2.4.2  Ordinals (continued)   ordon 4158
      2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4197
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4200
            2.5.3  Transfinite induction   tfi 4228
      2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4234
            2.6.2  The natural numbers (i.e. finite ordinals)   com 4236
            2.6.3  Peano's postulates   peano1 4240
            2.6.4  Finite induction (for finite ordinals)   find 4245
            2.6.5  The Natural Numbers (continued)   nn0suc 4250
            2.6.6  Relations   cxp 4266
            2.6.7  Definite description binder (inverted iota)   cio 4788
            2.6.8  Functions   wfun 4819
            2.6.9  Restricted iota (description binder)   crio 5388
            2.6.10  Operations   co 5432
            2.6.11  "Maps to" notation   elmpt2cl 5617
            2.6.12  Function operation   cof 5629
            2.6.13  Functions (continued)   resfunexgALT 5656
            2.6.14  First and second members of an ordered pair   c1st 5684
            *2.6.15  Special "Maps to" operations   mpt2xopn0yelv 5772
            2.6.16  Function transposition   ctpos 5777
            2.6.17  Undefined values   pwuninel2 5815
            2.6.18  Functions on ordinals; strictly monotone ordinal functions   iunon 5817
            2.6.19  "Strong" transfinite recursion   crecs 5837
            2.6.20  Recursive definition generator   crdg 5873
            2.6.21  Finite recursion   cfrec 5893
            2.6.22  Ordinal arithmetic   c1o 5905
            2.6.23  Natural number arithmetic   nna0 5964
            2.6.24  Equivalence relations and classes   wer 6010
*PART 3  REAL AND COMPLEX NUMBERS
      3.1  Construction and axiomatization of real and complex numbers
            3.1.1  Dedekind-cut construction of real and complex numbers   cnpi 6126
            3.1.2  Final derivation of real and complex number postulates   axcnex 6558
            3.1.3  Real and complex number postulates restated as axioms   ax-cnex 6586
      3.2  Derive the basic properties from the field axioms
            3.2.1  Some deductions from the field axioms for complex numbers   cnex 6614
            3.2.2  Infinity and the extended real number system   cpnf 6665
            3.2.3  Restate the ordering postulates with extended real "less than"   axltirr 6694
            3.2.4  Ordering on reals   lttr 6700
            3.2.5  Initial properties of the complex numbers   mul12 6750
      3.3  Real and complex numbers - basic operations
            3.3.1  Addition   add12 6777
            3.3.2  Subtraction   cmin 6790
            3.3.3  Multiplication   kcnktkm1cn 6987
            3.3.4  Ordering on reals (cont.)   ltadd2 7023
            3.3.5  Real Apartness   creap 7169
            3.3.6  Complex Apartness   cap 7176
            3.3.7  Reciprocals   recextlem1 7211
PART 4  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
      4.1  Mathboxes for user contributions
            4.1.1  Mathbox guidelines   mathbox 7223
      4.2  Mathbox for Mykola Mostovenko
      4.3  Mathbox for BJ
            4.3.1  Propositional calculus   nnexmid 7225
            4.3.2  Predicate calculus   bj-ex 7228
            *4.3.3  Extensionality   bj-vtoclgft 7240
            *4.3.4  Bounded formulas   wbd 7258
            *4.3.5  Bounded classes   wbdc 7286
            *4.3.6  Bounded separation   ax-bdsep 7330
                  4.3.6.1  Delta_0-classical logic   ax-bj-d0cl 7366
                  4.3.6.2  Inductive classes and the class of natural numbers (finite ordinals)   wind 7372
                  *4.3.6.3  The first three Peano postulates   bj-peano2 7384
            *4.3.7  Axiom of infinity   ax-infvn 7386
                  *4.3.7.1  The set of natural numbers (finite ordinals)   ax-infvn 7386
                  *4.3.7.2  The remaining two Peano postulates   bdpeano5 7388
                  *4.3.7.3  Bounded induction   findset 7390
            *4.3.8  Set induction   setindft 7406
                  *4.3.8.1  Set induction   setindft 7406
                  *4.3.8.2  Full induction   bj-findis 7420
            *4.3.9  Strong collection   ax-strcoll 7423
            *4.3.10  Subset collection   ax-sscoll 7428
      4.4  Mathbox for David A. Wheeler
            *4.4.1  Allsome quantifier   walsi 7430

    < Wrap  Next >

Page List
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-7438
  Copyright terms: Public domain < Wrap  Next >