TOC of Theorem List - New Foundations Explorer

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
      2.5  Cantorian and Strongly Cantorian Sets
PART 3  GUIDES AND MISCELLANEA
      3.1  Guides (conventions, explanations, and examples)

Detailed Table of Contents
(* means the section header has a description)

​​*PART 1  CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
      ​*1.1  Pre-logic
            *1.1.1  Inferences for assisting proof development   idi 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-mp 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 2477
            2.1.4  Negated equality and membership   wne 2517
            2.1.5  Restricted quantification   wral 2615
            2.1.6  The universal class   cvv 2860
            2.1.7  Russell's Paradox   ru 3046
            2.1.8  Proper substitution of classes for sets   wsbc 3047
            2.1.9  Proper substitution of classes for sets into classes   csb 3137
            2.1.10  Define boolean set operations   cnin 3205
            2.1.11  Subclasses and subsets   wss 3258
            2.1.12  The difference, union, and intersection of two classes   difeq12 3381
            2.1.13  The empty set   c0 3551
            ​*2.1.14  "Weak deduction theorem" for set theory   cif 3663
            2.1.15  Power classes   cpw 3723
            2.1.16  Unordered and ordered pairs   csn 3738
            2.1.17  The union of a class   cuni 3892
            2.1.18  The intersection of a class   cint 3927
            2.1.19  Indexed union and intersection   ciun 3970
            2.1.20  The Kuratowski ordered pair   copk 4058
            2.1.21  More Boolean set operations   compldif 4070
      ​2.2  NF Set Theory - add the Set Construction Axioms
            2.2.1  Introduce the set construction axioms   ax-nin 4079
            2.2.2  Primitive forms for some axioms   axprimlem1 4089
            2.2.3  Initial existence theorems   ninexg 4098
            2.2.4  Singletons and pairs (continued)   snprss1 4121
            2.2.5  Kuratowski ordered pairs (continued)   elopk 4130
            2.2.6  Cardinal one, unit unions, and unit power classes   cuni1 4134
            2.2.7  Kuratowski relationships   cxpk 4175
            2.2.8  Kuratowski existence theorems   xpkvexg 4286
            2.2.9  Definite description binder (inverted iota)   cio 4338
            2.2.10  Finite cardinals   cnnc 4374
            2.2.11  Deriving infinity   clefin 4433
      ​2.3  Ordered Pairs, Relationships, and Functions
            2.3.1  Ordered Pairs   cop 4562
            2.3.2  Ordered-pair class abstractions (class builders)   copab 4623
            2.3.3  Binary relations   wbr 4640
            2.3.4  Ordered-pair class abstractions (cont.)   opabid 4696
            2.3.5  Set construction functions   c1st 4718
            2.3.6  Epsilon and identity relations   cep 4763
            2.3.7  Functions and relations   cxp 4771
            2.3.8  Operations   co 5526
            2.3.9  "Maps to" notation   cmpt 5652
            2.3.10  Set construction lemmas   ctxp 5736
            2.3.11  Closure operation   cclos1 5873
      ​2.4  Orderings
            2.4.1  Basic ordering relationships   ctrans 5889
            2.4.2  Equivalence relations and classes   cec 5946
            2.4.3  The mapping operation   cmap 6000
            2.4.4  Equinumerosity   cen 6029
            2.4.5  Cardinal numbers   cncs 6089
            2.4.6  Specker's disproof of the axiom of choice   cspac 6274
            2.4.7  Finite recursion   cfrec 6310
      ​2.5  Cantorian and Strongly Cantorian Sets
​PART 3  GUIDES AND MISCELLANEA
      ​3.1  Guides (conventions, explanations, and examples)
            ​*3.1.1  Conventions   conventions 6339