HomeHome New Foundations Explorer
Theorem List (Table of Contents)
< Wrap  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page:  Detailed Table of Contents  Page List

Table of Contents Summary
PART 1  CLASSICAL FIRST ORDER LOGIC WITH EQUALITY
      1.1  Pre-logic
      1.2  Propositional calculus
      1.3  Other axiomatizations of classical propositional calculus
      1.4  Predicate calculus mostly without distinct variables
      1.5  Predicate calculus with distinct variables
PART 2  NEW FOUNDATIONS (NF) SET THEORY
      2.1  NF Set Theory - start with the Axiom of Extensionality
      2.2  NF Set Theory - add the Set Construction Axioms
      2.3  Ordered Pairs, Relationships, and Functions
      2.4  Orderings
      2.5  Appendix: Typesetting definitions for the tokens in this file

Detailed Table of Contents
PART 1  CLASSICAL 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  The axioms of propositional calculus   ax-1 5
            1.2.3  Logical implication   mp2b 9
            1.2.4  Logical negation   con4d 96
            1.2.5  Logical equivalence   wb 173
            1.2.6  Logical disjunction and conjunction   wo 354
            1.2.7  Miscellaneous theorems of propositional calculus   pm5.21nd 822
            1.2.8  Abbreviated conjunction and disjunction of three wff's   w3o 883
      1.3  Other axiomatizations of classical propositional calculus
            1.3.1  Derive the Lukasiewicz axioms from Meredith's sole axiom   meredith 1229
            1.3.2  Derive the standard axioms from the Lukasiewicz axioms   luklem1 1247
            1.3.3  Logical 'nand' (Sheffer stroke)   wnand 1258
            1.3.4  Derive Nicod's axiom from the standard axioms   nic-justlem 1269
            1.3.5  Derive the Lukasiewicz axioms from Nicod's axiom   nic-imp 1279
            1.3.6  True and false constants   wtru 1298
            1.3.7  Auxiliary theorems for Alan Sare's virtual deduction tool, part 1   ee22 1306
      1.4  Predicate calculus mostly without distinct variables
            1.4.1  "Pure" (equality-free) predicate calculus axioms ax-5, ax-6, ax-7, ax-gen   wal 1322
            1.4.2  Introduce equality axioms ax-8 through ax-14 except ax-9   cv 1397
            1.4.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1413
            1.4.4  Derive ax-9 from a weaker version   a9wa9lem1 1415
            1.4.5  Introduce Axiom of Existence ax-9   ax-9 1424
            1.4.6  Derive ax-4, ax-5o, and ax-6o   ax4 1428
            1.4.7  "Pure" predicate calculus including ax-4, without distinct variables   a4i 1436
            1.4.8  Equality theorems without distinct variables   ax9o 1518
            1.4.9  Axioms ax-10 and ax-11   ax10o 1537
            1.4.10  Substitution (without distinct variables)   wsbc 1566
            1.4.11  Theorems using axiom ax-11   equs5a 1593
      1.5  Predicate calculus with distinct variables
            1.5.1  Derive the axiom of distinct variables ax-16   a4imv 1603
            1.5.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1615
            1.5.3  Theorems without distinct variables that use axiom ax-11o   ax11b 1618
            1.5.4  Predicate calculus with distinct variables (cont.)   ax11v 1665
            1.5.5  More substitution theorems   equsb3lem 1733
            1.5.6  Existential uniqueness   weu 1791
PART 2  NEW FOUNDATIONS (NF) SET THEORY
      2.1  NF Set Theory - start with the Axiom of Extensionality
            2.1.1  Introduce the Axiom of Extensionality   ax-ext 1877
            2.1.2  Class abstractions (a.k.a. class builders)   cab 1882
            2.1.3  Negated equality and membership   wne 2012
            2.1.4  Restricted quantification   wral 2103
            2.1.5  The universal class   cvv 2300
            2.1.6  Russell's Paradox   ru 2468
            2.1.7  Proper substitution of classes for sets   df-sbc 2469
            2.1.8  Proper substitution of classes for sets into classes   csb 2550
            2.1.9  Boolean set operators   cnin 2606
            2.1.10  The empty set   c0 2726
            2.1.11  Singleton class and unordered pair   csn 2803
            2.1.12  The Kuratowski ordered pair   copk 2862
            2.1.13  Subset   wss 2874
            2.1.14  The union of a class   cuni 3037
            2.1.15  The intersection of a class   cint 3071
            2.1.16  "Weak deduction theorem" for set theory   cif 3108
            2.1.17  Power classes   cpw 3165
      2.2  NF Set Theory - add the Set Construction Axioms
            2.2.1  Introduce the set construction axioms   ax-nin 3180
            2.2.2  Primitive forms for some axioms   axprimlem1 3190
            2.2.3  Initial existence theorems   ninexg 3199
            2.2.4  Singletons and pairs (continued)   snprss1 3222
            2.2.5  Kuratowski ordered pairs (continued)   elopk 3233
            2.2.6  Cardinal one, unit unions, and unit power classes   cuni1 3237
            2.2.7  Kuratowski relationships   cxpk 3278
            2.2.8  Kuratowski existence theorems   xpkvexg 3389
            2.2.9  Definite description binder (inverted iota)   cio 3448
            2.2.10  Finite cardinals   cnnc 3481
            2.2.11  Deriving infinity   clefin 3539
      2.3  Ordered Pairs, Relationships, and Functions
            2.3.1  Ordered Pairs   cop 3669
            2.3.2  Ordered-pair class abstractions (class builders)   copab 3722
            2.3.3  Binary relations   wbr 3736
            2.3.4  Ordered-pair class abstractions (cont.)   opabid 3790
            2.3.5  Set construction functions   c1st 3815
            2.3.6  Indexed union and intersection   ciun 3860
            2.3.7  Epsilon and identity relations   cep 3934
            2.3.8  Functions and relations   cxp 3942
            2.3.9  Operations   co 4766
            2.3.10  "Maps to" notation   cmpt 4893
            2.3.11  Set construction lemmas   ctxp 4962
            2.3.12  Closure operation   cclos1 5085
      2.4  Orderings
            2.4.1  Basic ordering relationships   ctrans 5099
            2.4.2  Equivalence relations and classes   cec 5156
            2.4.3  The mapping operation   cmap 5211
            2.4.4  Equinumerosity   cen 5240
            2.4.5  Cardinal numbers   cncs 5300
            2.4.6  Specker's disproof of the axiom of choice   cspac 5465
      2.5  Appendix: Typesetting definitions for the tokens in this file

    < 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-5506
  Copyright terms: Public domain < Wrap  Next >