TOC of Theorem List - Intuitionistic Logic Explorer

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
      3.4  Integer sets
      3.5  Order sets
      3.6  Elementary integer functions
      3.7  Elementary real and complex functions
      3.8  Elementary limits and convergence
PART 4  ELEMENTARY NUMBER THEORY
      4.1  Elementary properties of divisibility
      4.2  Elementary prime number theory
PART 5  GUIDES AND MISCELLANEA
      5.1  Guides (conventions, explanations, and examples)
PART 6  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
      ​6.1  Mathboxes for user contributions
      6.2  Mathbox for BJ
      6.3  Mathbox for Jim Kingdon
      6.4  Mathbox for Mykola Mostovenko
      6.5  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   a1ii 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 102
            1.2.5  Logical negation (intuitionistic)   ax-in1 576
            1.2.6  Logical disjunction   wo 661
            1.2.7  Stable propositions   wstab 772
            1.2.8  Decidable propositions   wdc 775
            ​*1.2.9  Theorems of decidable propositions   condc 782
            1.2.10  Testable propositions   dftest 855
            1.2.11  Miscellaneous theorems of propositional calculus   pm5.21nd 858
            1.2.12  Abbreviated conjunction and disjunction of three wff's   w3o 918
            1.2.13  True and false constants   wal 1282
                  ​*1.2.13.1  Universal quantifier for use by df-tru   wal 1282
                  ​*1.2.13.2  Equality predicate for use by df-tru   cv 1283
                  1.2.13.3  Define the true and false constants   wtru 1285
            1.2.14  Logical 'xor'   wxo 1306
            ​*1.2.15  Truth tables: Operations on true and false constants   truantru 1332
            ​*1.2.16  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1354
            1.2.17  Logical implication (continued)   syl6an 1363
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1376
            ​*1.3.2  Equality predicate (continued)   weq 1432
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1459
            1.3.4  Introduce Axiom of Existence   ax-i9 1463
            1.3.5  Additional intuitionistic axioms   ax-ial 1467
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1469
            1.3.7  The existential quantifier   19.8a 1522
            1.3.8  Equality theorems without distinct variables   a9e 1626
            1.3.9  Axioms ax-10 and ax-11   ax10o 1643
            1.3.10  Substitution (without distinct variables)   wsb 1685
            1.3.11  Theorems using axiom ax-11   equs5a 1715
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1732
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1743
            1.4.3  More theorems related to ax-11 and substitution   albidv 1745
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1779
            1.4.5  More substitution theorems   hbs1 1855
            1.4.6  Existential uniqueness   weu 1941
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2039
​​*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 2063
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2067
            2.1.3  Class form not-free predicate   wnfc 2206
            2.1.4  Negated equality and membership   wne 2245
                  2.1.4.1  Negated equality   wne 2245
                  2.1.4.2  Negated membership   wnel 2339
            2.1.5  Restricted quantification   wral 2348
            2.1.6  The universal class   cvv 2601
            ​*2.1.7  Conditional equality (experimental)   wcdeq 2798
            2.1.8  Russell's Paradox   ru 2814
            2.1.9  Proper substitution of classes for sets   wsbc 2815
            2.1.10  Proper substitution of classes for sets into classes   csb 2908
            2.1.11  Define basic set operations and relations   cdif 2970
            2.1.12  Subclasses and subsets   df-ss 2986
            2.1.13  The difference, union, and intersection of two classes   difeq1 3083
                  2.1.13.1  The difference of two classes   difeq1 3083
                  2.1.13.2  The union of two classes   elun 3113
                  2.1.13.3  The intersection of two classes   elin 3155
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3196
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3230
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3244
            2.1.14  The empty set   c0 3251
            2.1.15  Conditional operator   cif 3351
            2.1.16  Power classes   cpw 3382
            2.1.17  Unordered and ordered pairs   csn 3398
            2.1.18  The union of a class   cuni 3601
            2.1.19  The intersection of a class   cint 3636
            2.1.20  Indexed union and intersection   ciun 3678
            2.1.21  Disjointness   wdisj 3766
            2.1.22  Binary relations   wbr 3785
            2.1.23  Ordered-pair class abstractions (class builders)   copab 3838
            2.1.24  Transitive classes   wtr 3875
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 3893
            2.2.2  Introduce the Axiom of Separation   ax-sep 3896
            2.2.3  Derive the Null Set Axiom   zfnuleu 3902
            2.2.4  Theorems requiring subset and intersection existence   nalset 3908
            2.2.5  Theorems requiring empty set existence   class2seteq 3937
            2.2.6  Collection principle   bnd 3946
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 3948
            2.3.2  Axiom of Pairing   ax-pr 3964
            2.3.3  Ordered pair theorem   opm 3989
            2.3.4  Ordered-pair class abstractions (cont.)   opabid 4012
            2.3.5  Power class of union and intersection   pwin 4037
            2.3.6  Epsilon and identity relations   cep 4042
            2.3.7  Partial and complete ordering   wpo 4049
            2.3.8  Founded and set-like relations   wfrfor 4082
            2.3.9  Ordinals   word 4117
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4188
            2.4.2  Ordinals (continued)   ordon 4230
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4275
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4280
            2.5.3  Transfinite induction   tfi 4323
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4329
            2.6.2  The natural numbers (i.e. finite ordinals)   com 4331
            2.6.3  Peano's postulates   peano1 4335
            2.6.4  Finite induction (for finite ordinals)   find 4340
            2.6.5  The Natural Numbers (continued)   nn0suc 4345
            2.6.6  Relations   cxp 4361
            2.6.7  Definite description binder (inverted iota)   cio 4885
            2.6.8  Functions   wfun 4916
            2.6.9  Restricted iota (description binder)   crio 5487
            2.6.10  Operations   co 5532
            2.6.11  "Maps to" notation   elmpt2cl 5718
            2.6.12  Function operation   cof 5730
            2.6.13  Functions (continued)   resfunexgALT 5757
            2.6.14  First and second members of an ordered pair   c1st 5785
            ​*2.6.15  Special "Maps to" operations   mpt2xopn0yelv 5877
            2.6.16  Function transposition   ctpos 5882
            2.6.17  Undefined values   pwuninel2 5920
            2.6.18  Functions on ordinals; strictly monotone ordinal functions   iunon 5922
            2.6.19  "Strong" transfinite recursion   crecs 5942
            2.6.20  Recursive definition generator   crdg 5979
            2.6.21  Finite recursion   cfrec 6000
            2.6.22  Ordinal arithmetic   c1o 6017
            2.6.23  Natural number arithmetic   nna0 6076
            2.6.24  Equivalence relations and classes   wer 6126
            2.6.25  Equinumerosity   cen 6242
            2.6.26  Pigeonhole Principle   phplem1 6338
            2.6.27  Finite sets   fidceq 6354
            2.6.28  Supremum and infimum   csup 6395
            2.6.29  Ordinal isomorphism   ordiso2 6446
            2.6.30  Cardinal numbers   ccrd 6448
​​*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 6462
            3.1.2  Final derivation of real and complex number postulates   axcnex 7027
            3.1.3  Real and complex number postulates restated as axioms   ax-cnex 7067
      ​3.2  Derive the basic properties from the field axioms
            3.2.1  Some deductions from the field axioms for complex numbers   cnex 7097
            3.2.2  Infinity and the extended real number system   cpnf 7150
            3.2.3  Restate the ordering postulates with extended real "less than"   axltirr 7179
            3.2.4  Ordering on reals   lttr 7185
            3.2.5  Initial properties of the complex numbers   mul12 7237
      ​3.3  Real and complex numbers - basic operations
            3.3.1  Addition   add12 7266
            3.3.2  Subtraction   cmin 7279
            3.3.3  Multiplication   kcnktkm1cn 7487
            3.3.4  Ordering on reals (cont.)   ltadd2 7523
            3.3.5  Real Apartness   creap 7674
            3.3.6  Complex Apartness   cap 7681
            3.3.7  Reciprocals   recextlem1 7741
            3.3.8  Division   cdiv 7760
            3.3.9  Ordering on reals (cont.)   ltp1 7922
            3.3.10  Suprema   lbreu 8023
            3.3.11  Imaginary and complex number properties   crap0 8035
      ​3.4  Integer sets
            3.4.1  Positive integers (as a subset of complex numbers)   cn 8039
            3.4.2  Principle of mathematical induction   nnind 8055
            ​*3.4.3  Decimal representation of numbers   c2 8089
            ​*3.4.4  Some properties of specific numbers   neg1cn 8144
            3.4.5  Simple number properties   halfcl 8257
            3.4.6  The Archimedean property   arch 8285
            3.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 8288
            3.4.8  Integers (as a subset of complex numbers)   cz 8351
            3.4.9  Decimal arithmetic   cdc 8477
            3.4.10  Upper sets of integers   cuz 8619
            3.4.11  Rational numbers (as a subset of complex numbers)   cq 8704
            3.4.12  Complex numbers as pairs of reals   cnref1o 8733
      ​3.5  Order sets
            3.5.1  Positive reals (as a subset of complex numbers)   crp 8734
            3.5.2  Infinity and the extended real number system (cont.)   cxne 8840
            3.5.3  Real number intervals   cioo 8911
            3.5.4  Finite intervals of integers   cfz 9029
            ​*3.5.5  Finite intervals of nonnegative integers   elfz2nn0 9128
            3.5.6  Half-open integer ranges   cfzo 9152
            3.5.7  Rational numbers (cont.)   qtri3or 9252
      ​3.6  Elementary integer functions
            3.6.1  The floor and ceiling functions   cfl 9272
            3.6.2  The modulo (remainder) operation   cmo 9324
            3.6.3  Miscellaneous theorems about integers   frec2uz0d 9401
            3.6.4  Strong induction over upper sets of integers   uzsinds 9428
            3.6.5  The infinite sequence builder "seq"   cseq 9431
            3.6.6  Integer powers   cexp 9475
            3.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 9646
            3.6.8  Factorial function   cfa 9652
            3.6.9  The binomial coefficient operation   cbc 9674
      ​3.7  Elementary real and complex functions
            3.7.1  The "shift" operation   cshi 9702
            3.7.2  Real and imaginary parts; conjugate   ccj 9726
            3.7.3  Sequence convergence   caucvgrelemrec 9865
            3.7.4  Square root; absolute value   csqrt 9882
            3.7.5  The maximum of two real numbers   maxcom 10089
            3.7.6  The minimum of two real numbers   mincom 10111
      ​3.8  Elementary limits and convergence
            3.8.1  Limits   cli 10117
            3.8.2  Finite and infinite sums   csu 10190
​​*PART 4  ELEMENTARY NUMBER THEORY
      ​4.1  Elementary properties of divisibility
            4.1.1  The divides relation   cdvds 10195
            ​*4.1.2  Even and odd numbers   evenelz 10266
            4.1.3  The division algorithm   divalglemnn 10318
            4.1.4  The greatest common divisor operator   cgcd 10338
            4.1.5  Bézout's identity   bezoutlemnewy 10385
            4.1.6  Algorithms   nn0seqcvgd 10423
            4.1.7  Euclid's Algorithm   eucalgval2 10435
            ​*4.1.8  The least common multiple   clcm 10442
            ​*4.1.9  Coprimality and Euclid's lemma   coprmgcdb 10470
            4.1.10  Cancellability of congruences   congr 10482
      ​4.2  Elementary prime number theory
            ​*4.2.1  Elementary properties   cprime 10489
            ​*4.2.2  Coprimality and Euclid's lemma (cont.)   coprm 10523
            4.2.3  Non-rationality of square root of 2   sqrt2irrlem 10540
​PART 5  GUIDES AND MISCELLANEA
      ​5.1  Guides (conventions, explanations, and examples)
            ​*5.1.1  Conventions   conventions 10559
            5.1.2  Definitional examples   ex-or 10560
​PART 6  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
      ​6.1  Mathboxes for user contributions
            6.1.1  Mathbox guidelines   mathbox 10569
      ​6.2  Mathbox for BJ
            6.2.1  Propositional calculus   nnexmid 10570
            6.2.2  Predicate calculus   bj-ex 10573
            ​*6.2.3  Extensionality   bj-vtoclgft 10585
            ​*6.2.4  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 10603
                  *6.2.4.1  Bounded formulas   wbd 10603
                  ​*6.2.4.2  Bounded classes   wbdc 10631
            ​*6.2.5  CZF: Bounded separation   ax-bdsep 10675
                  6.2.5.1  Delta_0-classical logic   ax-bj-d0cl 10715
                  6.2.5.2  Inductive classes and the class of natural numbers (finite ordinals)   wind 10721
                  ​*6.2.5.3  The first three Peano postulates   bj-peano2 10734
            ​*6.2.6  CZF: Infinity   ax-infvn 10736
                  *6.2.6.1  The set of natural numbers (finite ordinals)   ax-infvn 10736
                  ​*6.2.6.2  Peano's fifth postulate   bdpeano5 10738
                  ​*6.2.6.3  Bounded induction and Peano's fourth postulate   findset 10740
            ​*6.2.7  CZF: Set induction   setindft 10760
                  *6.2.7.1  Set induction   setindft 10760
                  ​*6.2.7.2  Full induction   bj-findis 10774
            ​*6.2.8  CZF: Strong collection   ax-strcoll 10777
            ​*6.2.9  CZF: Subset collection   ax-sscoll 10782
            6.2.10  Real numbers   ax-ddkcomp 10784
      ​6.3  Mathbox for Jim Kingdon
      ​6.4  Mathbox for Mykola Mostovenko
      ​6.5  Mathbox for David A. Wheeler
            ​*6.5.1  Allsome quantifier   walsi 10787