HomeHome New Foundations Explorer
Theorem List (Table of Contents)
< Wrap  Next >
Bad symbols? Use Firefox
(or GIF version for IE).

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 with equality: Tarski's system S2 (1 rule, 6 schemes)
      1.5  Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)
      1.6  Predicate calculus with equality: Older axiomatization (1 rule, 14 schemes)
      1.7  Existential uniqueness
      1.8  Other axiomatizations related to classical predicate calculus
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

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 97
            1.2.5  Logical equivalence   wb 176
            1.2.6  Logical disjunction and conjunction   wo 357
            1.2.7  Miscellaneous theorems of propositional calculus   pm5.21nd 868
            1.2.8  Abbreviated conjunction and disjunction of three wff's   w3o 933
            1.2.9  Logical 'nand' (Sheffer stroke)   wnan 1287
            1.2.10  Logical 'xor'   wxo 1304
            1.2.11  True and false constants   wtru 1316
            1.2.12  Truth tables   truantru 1336
            1.2.13  Auxiliary theorems for Alan Sare's virtual deduction tool, part 1   ee22 1362
            1.2.14  Half-adders and full adders in propositional calculus   whad 1378
      1.3  Other axiomatizations of classical propositional calculus
            1.3.1  Derive the Lukasiewicz axioms from Meredith's sole axiom   meredith 1404
            1.3.2  Derive the standard axioms from the Lukasiewicz axioms   luklem1 1423
            1.3.3  Derive Nicod's axiom from the standard axioms   nic-dfim 1434
            1.3.4  Derive the Lukasiewicz axioms from Nicod's axiom   nic-imp 1440
            1.3.5  Derive Nicod's Axiom from Lukasiewicz's First Sheffer Stroke Axiom   lukshef-ax1 1459
            1.3.6  Derive the Lukasiewicz Axioms from the Tarski-Bernays-Wajsberg Axioms   tbw-bijust 1463
            1.3.7  Derive the Tarski-Bernays-Wajsberg axioms from Meredith's First CO Axiom   merco1 1478
            1.3.8  Derive the Tarski-Bernays-Wajsberg axioms from Meredith's Second CO Axiom   merco2 1501
            1.3.9  Derive the Lukasiewicz axioms from the The Russell-Bernays Axioms   rb-bijust 1514
            1.3.10  Stoic logic indemonstrables (Chrysippus of Soli)   mpto1 1533
      1.4  Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
            1.4.1  Universal quantifier; define "exists" and "not free"   wal 1540
            1.4.2  Rule scheme ax-gen (Generalization)   ax-gen 1546
            1.4.3  Axiom scheme ax-5 (Quantified Implication)   ax-5 1557
            1.4.4  Axiom scheme ax-17 (Distinctness) - first use of $d   ax-17 1616
            1.4.5  Equality predicate; define substitution   cv 1641
            1.4.6  Axiom scheme ax-9 (Existence)   ax-9 1654
            1.4.7  Axiom scheme ax-8 (Equality)   ax-8 1675
            1.4.8  Membership predicate   wcel 1710
            1.4.9  Axiom schemes ax-13 (Left Equality for Binary Predicate)   ax-13 1712
            1.4.10  Axiom schemes ax-14 (Right Equality for Binary Predicate)   ax-14 1714
            1.4.11  Logical redundancy of ax-6 , ax-7 , ax-11 , ax-12   ax9dgen 1716
      1.5  Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)
            1.5.1  Axiom scheme ax-6 (Quantified Negation)   ax-6 1729
            1.5.2  Axiom scheme ax-7 (Quantifier Commutation)   ax-7 1734
            1.5.3  Axiom scheme ax-11 (Substitution)   ax-11 1746
            1.5.4  Axiom scheme ax-12 (Quantified Equality)   ax-12 1925
      1.6  Predicate calculus with equality: Older axiomatization (1 rule, 14 schemes)
            1.6.1  Obsolete schemes ax-5o ax-4 ax-6o ax-9o ax-10o ax-10 ax-11o ax-12o ax-15 ax-16   ax-4 2135
            1.6.2  Rederive new axioms from old: ax5 , ax6 , ax9from9o , ax11 , ax12from12o   ax4 2145
            1.6.3  Legacy theorems using obsolete axioms   ax17o 2157
      1.7  Existential uniqueness
      1.8  Other axiomatizations related to classical predicate calculus
            1.8.1  Predicate calculus with all distinct variables   ax-7d 2295
            1.8.2  Aristotelian logic: Assertic syllogisms   barbara 2301
            1.8.3  Intuitionistic logic   axi4 2325
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 2334
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2339
            2.1.3  Class form not-free predicate   wnfc 2476
            2.1.4  Negated equality and membership   wne 2516
            2.1.5  Restricted quantification   wral 2614
            2.1.6  The universal class   cvv 2859
            2.1.7  Russell's Paradox   ru 3045
            2.1.8  Proper substitution of classes for sets   wsbc 3046
            2.1.9  Proper substitution of classes for sets into classes   csb 3136
            2.1.10  Define boolean set operations   cnin 3204
            2.1.11  Subclasses and subsets   wss 3257
            2.1.12  The difference, union, and intersection of two classes   difeq12 3380
            2.1.13  The empty set   c0 3550
            2.1.14  "Weak deduction theorem" for set theory   cif 3662
            2.1.15  Power classes   cpw 3722
            2.1.16  Unordered and ordered pairs   csn 3737
            2.1.17  The union of a class   cuni 3891
            2.1.18  The intersection of a class   cint 3926
            2.1.19  Indexed union and intersection   ciun 3969
            2.1.20  The Kuratowski ordered pair   copk 4057
            2.1.21  More Boolean set operations   compldif 4069
      2.2  NF Set Theory - add the Set Construction Axioms
            2.2.1  Introduce the set construction axioms   ax-nin 4078
            2.2.2  Primitive forms for some axioms   axprimlem1 4088
            2.2.3  Initial existence theorems   ninexg 4097
            2.2.4  Singletons and pairs (continued)   snprss1 4120
            2.2.5  Kuratowski ordered pairs (continued)   elopk 4129
            2.2.6  Cardinal one, unit unions, and unit power classes   cuni1 4133
            2.2.7  Kuratowski relationships   cxpk 4174
            2.2.8  Kuratowski existence theorems   xpkvexg 4285
            2.2.9  Definite description binder (inverted iota)   cio 4337
            2.2.10  Finite cardinals   cnnc 4373
            2.2.11  Deriving infinity   clefin 4431
      2.3  Ordered Pairs, Relationships, and Functions
            2.3.1  Ordered Pairs   cop 4561
            2.3.2  Ordered-pair class abstractions (class builders)   copab 4614
            2.3.3  Binary relations   wbr 4631
            2.3.4  Ordered-pair class abstractions (cont.)   opabid 4687
            2.3.5  Set construction functions   c1st 4709
            2.3.6  Epsilon and identity relations   cep 4754
            2.3.7  Functions and relations   cxp 4762
            2.3.8  Operations   co 5564
            2.3.9  "Maps to" notation   cmpt 5691
            2.3.10  Set construction lemmas   ctxp 5771
            2.3.11  Closure operation   cclos1 5894
      2.4  Orderings
            2.4.1  Basic ordering relationships   ctrans 5908
            2.4.2  Equivalence relations and classes   cec 5965
            2.4.3  The mapping operation   cmap 6019
            2.4.4  Equinumerosity   cen 6048
            2.4.5  Cardinal numbers   cncs 6108
            2.4.6  Specker's disproof of the axiom of choice   cspac 6273

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