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  CHOICE PRINCIPLES
      3.1  Countable Choice and Dependent Choice
PART 4  REAL AND COMPLEX NUMBERS
      4.1  Construction and axiomatization of real and complex numbers
      4.2  Derive the basic properties from the field axioms
      4.3  Real and complex numbers - basic operations
      4.4  Integer sets
      4.5  Order sets
      4.6  Elementary integer functions
      4.7  Elementary real and complex functions
      4.8  Elementary limits and convergence
      4.9  Elementary trigonometry
PART 5  ELEMENTARY NUMBER THEORY
      5.1  Elementary properties of divisibility
      5.2  Elementary prime number theory
      5.3  Cardinality of real and complex number subsets
PART 6  BASIC STRUCTURES
      6.1  Extensible structures
      6.2  The complex numbers as an algebraic extensible structure
PART 7  BASIC TOPOLOGY
      7.1  Topology
      7.2  Metric spaces
PART 8  BASIC REAL AND COMPLEX ANALYSIS
      8.1  Derivatives
PART 9  GUIDES AND MISCELLANEA
      9.1  Guides (conventions, explanations, and examples)
PART 10  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​10.1  Mathboxes for user contributions
      10.2  Mathbox for BJ
      10.3  Mathbox for Jim Kingdon
      10.4  Mathbox for Mykola Mostovenko
      10.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   idi 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 103
            1.2.5  Logical negation (intuitionistic)   ax-in1 586
            1.2.6  Logical disjunction   wo 680
            1.2.7  Stable propositions   wstab 798
            1.2.8  Decidable propositions   wdc 802
            ​*1.2.9  Theorems of decidable propositions   const 820
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 884
            1.2.11  Abbreviated conjunction and disjunction of three wff's   w3o 944
            1.2.12  True and false constants   wal 1312
                  ​*1.2.12.1  Universal quantifier for use by df-tru   wal 1312
                  ​*1.2.12.2  Equality predicate for use by df-tru   cv 1313
                  1.2.12.3  Define the true and false constants   wtru 1315
            1.2.13  Logical 'xor'   wxo 1336
            ​*1.2.14  Truth tables: Operations on true and false constants   truantru 1362
            ​*1.2.15  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1384
            1.2.16  Logical implication (continued)   syl6an 1393
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1406
            ​*1.3.2  Equality predicate (continued)   weq 1462
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1489
            1.3.4  Introduce Axiom of Existence   ax-i9 1493
            1.3.5  Additional intuitionistic axioms   ax-ial 1497
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1499
            1.3.7  The existential quantifier   19.8a 1552
            1.3.8  Equality theorems without distinct variables   a9e 1657
            1.3.9  Axioms ax-10 and ax-11   ax10o 1676
            1.3.10  Substitution (without distinct variables)   wsb 1718
            1.3.11  Theorems using axiom ax-11   equs5a 1748
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1765
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1776
            1.4.3  More theorems related to ax-11 and substitution   albidv 1778
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1812
            1.4.5  More substitution theorems   hbs1 1889
            1.4.6  Existential uniqueness   weu 1975
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2073
​​*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 2097
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2101
            2.1.3  Class form not-free predicate   wnfc 2242
            2.1.4  Negated equality and membership   wne 2282
                  2.1.4.1  Negated equality   wne 2282
                  2.1.4.2  Negated membership   wnel 2377
            2.1.5  Restricted quantification   wral 2390
            2.1.6  The universal class   cvv 2657
            ​*2.1.7  Conditional equality (experimental)   wcdeq 2861
            2.1.8  Russell's Paradox   ru 2877
            2.1.9  Proper substitution of classes for sets   wsbc 2878
            2.1.10  Proper substitution of classes for sets into classes   csb 2971
            2.1.11  Define basic set operations and relations   cdif 3034
            2.1.12  Subclasses and subsets   df-ss 3050
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3152
                  2.1.13.1  The difference of two classes   dfdif3 3152
                  2.1.13.2  The union of two classes   elun 3183
                  2.1.13.3  The intersection of two classes   elin 3225
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3273
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3308
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3322
            2.1.14  The empty set   c0 3329
            2.1.15  Conditional operator   cif 3440
            2.1.16  Power classes   cpw 3476
            2.1.17  Unordered and ordered pairs   csn 3493
            2.1.18  The union of a class   cuni 3702
            2.1.19  The intersection of a class   cint 3737
            2.1.20  Indexed union and intersection   ciun 3779
            2.1.21  Disjointness   wdisj 3872
            2.1.22  Binary relations   wbr 3895
            2.1.23  Ordered-pair class abstractions (class builders)   copab 3948
            2.1.24  Transitive classes   wtr 3986
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4003
            2.2.2  Introduce the Axiom of Separation   ax-sep 4006
            2.2.3  Derive the Null Set Axiom   zfnuleu 4012
            2.2.4  Theorems requiring subset and intersection existence   nalset 4018
            2.2.5  Theorems requiring empty set existence   class2seteq 4047
            2.2.6  Collection principle   bnd 4056
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4058
            2.3.2  A notation for excluded middle   wem 4078
            2.3.3  Axiom of Pairing   ax-pr 4091
            2.3.4  Ordered pair theorem   opm 4116
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4139
            2.3.6  Power class of union and intersection   pwin 4164
            2.3.7  Epsilon and identity relations   cep 4169
            2.3.8  Partial and complete ordering   wpo 4176
            2.3.9  Founded and set-like relations   wfrfor 4209
            2.3.10  Ordinals   word 4244
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4315
            2.4.2  Ordinals (continued)   ordon 4362
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4407
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4412
            2.5.3  Transfinite induction   tfi 4456
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4462
            2.6.2  The natural numbers (i.e. finite ordinals)   com 4464
            2.6.3  Peano's postulates   peano1 4468
            2.6.4  Finite induction (for finite ordinals)   find 4473
            2.6.5  The Natural Numbers (continued)   nn0suc 4478
            2.6.6  Relations   cxp 4497
            2.6.7  Definite description binder (inverted iota)   cio 5044
            2.6.8  Functions   wfun 5075
            2.6.9  Restricted iota (description binder)   crio 5683
            2.6.10  Operations   co 5728
            2.6.11  Maps-to notation   elmpocl 5922
            2.6.12  Function operation   cof 5934
            2.6.13  Functions (continued)   resfunexgALT 5962
            2.6.14  First and second members of an ordered pair   c1st 5990
            ​*2.6.15  Special maps-to operations   opeliunxp2f 6089
            2.6.16  Function transposition   ctpos 6095
            2.6.17  Undefined values   pwuninel2 6133
            2.6.18  Functions on ordinals; strictly monotone ordinal functions   iunon 6135
            2.6.19  "Strong" transfinite recursion   crecs 6155
            2.6.20  Recursive definition generator   crdg 6220
            2.6.21  Finite recursion   cfrec 6241
            2.6.22  Ordinal arithmetic   c1o 6260
            2.6.23  Natural number arithmetic   nna0 6324
            2.6.24  Equivalence relations and classes   wer 6380
            2.6.25  The mapping operation   cmap 6496
            2.6.26  Infinite Cartesian products   cixp 6546
            2.6.27  Equinumerosity   cen 6586
            2.6.28  Equinumerosity (cont.)   xpf1o 6691
            2.6.29  Pigeonhole Principle   phplem1 6699
            2.6.30  Finite sets   fict 6715
            2.6.31  Schroeder-Bernstein Theorem   sbthlem1 6797
            2.6.32  Finite intersections   cfi 6808
            2.6.33  Supremum and infimum   csup 6821
            2.6.34  Ordinal isomorphism   ordiso2 6872
            2.6.35  Disjoint union   cdju 6874
                  2.6.35.1  Disjoint union   cdju 6874
                  ​*2.6.35.2  Left and right injections of a disjoint union   cinl 6882
                  2.6.35.3  Universal property of the disjoint union   djuss 6907
                  2.6.35.4  Dominance and equinumerosity properties of disjoint union   djudom 6930
                  2.6.35.5  Older definition temporarily kept for comparison, to be deleted   cdjud 6939
                  2.6.35.6  Countable sets   0ct 6944
            2.6.36  Omniscient sets   comni 6954
            2.6.37  Markov's principle   cmarkov 6975
            2.6.38  Cardinal numbers   ccrd 6985
            2.6.39  Axiom of Choice equivalents   wac 7009
            2.6.40  Cardinal number arithmetic   endjudisj 7014
​​*PART 3  CHOICE PRINCIPLES
      ​3.1  Countable Choice and Dependent Choice
            3.1.1  Introduce Countable Choice   wacc 7025
​​*PART 4  REAL AND COMPLEX NUMBERS
      ​4.1  Construction and axiomatization of real and complex numbers
            4.1.1  Dedekind-cut construction of real and complex numbers   cnpi 7028
            4.1.2  Final derivation of real and complex number postulates   axcnex 7594
            4.1.3  Real and complex number postulates restated as axioms   ax-cnex 7636
      ​4.2  Derive the basic properties from the field axioms
            4.2.1  Some deductions from the field axioms for complex numbers   cnex 7668
            4.2.2  Infinity and the extended real number system   cpnf 7721
            4.2.3  Restate the ordering postulates with extended real "less than"   axltirr 7755
            4.2.4  Ordering on reals   lttr 7761
            4.2.5  Initial properties of the complex numbers   mul12 7814
      ​4.3  Real and complex numbers - basic operations
            4.3.1  Addition   add12 7843
            4.3.2  Subtraction   cmin 7856
            4.3.3  Multiplication   kcnktkm1cn 8064
            4.3.4  Ordering on reals (cont.)   ltadd2 8100
            4.3.5  Real Apartness   creap 8254
            4.3.6  Complex Apartness   cap 8261
            4.3.7  Reciprocals   recextlem1 8325
            4.3.8  Division   cdiv 8345
            4.3.9  Ordering on reals (cont.)   ltp1 8512
            4.3.10  Suprema   lbreu 8613
            4.3.11  Imaginary and complex number properties   crap0 8626
      ​4.4  Integer sets
            4.4.1  Positive integers (as a subset of complex numbers)   cn 8630
            4.4.2  Principle of mathematical induction   nnind 8646
            ​*4.4.3  Decimal representation of numbers   c2 8681
            ​*4.4.4  Some properties of specific numbers   neg1cn 8735
            4.4.5  Simple number properties   halfcl 8850
            4.4.6  The Archimedean property   arch 8878
            4.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 8881
            ​*4.4.8  Extended nonnegative integers   cxnn0 8944
            4.4.9  Integers (as a subset of complex numbers)   cz 8958
            4.4.10  Decimal arithmetic   cdc 9086
            4.4.11  Upper sets of integers   cuz 9228
            4.4.12  Rational numbers (as a subset of complex numbers)   cq 9313
            4.4.13  Complex numbers as pairs of reals   cnref1o 9342
      ​4.5  Order sets
            4.5.1  Positive reals (as a subset of complex numbers)   crp 9343
            4.5.2  Infinity and the extended real number system (cont.)   cxne 9449
            4.5.3  Real number intervals   cioo 9564
            4.5.4  Finite intervals of integers   cfz 9683
            ​*4.5.5  Finite intervals of nonnegative integers   elfz2nn0 9785
            4.5.6  Half-open integer ranges   cfzo 9812
            4.5.7  Rational numbers (cont.)   qtri3or 9913
      ​4.6  Elementary integer functions
            4.6.1  The floor and ceiling functions   cfl 9934
            4.6.2  The modulo (remainder) operation   cmo 9988
            4.6.3  Miscellaneous theorems about integers   frec2uz0d 10065
            4.6.4  Strong induction over upper sets of integers   uzsinds 10108
            4.6.5  The infinite sequence builder "seq"   cseq 10111
            4.6.6  Integer powers   cexp 10185
            4.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 10358
            4.6.8  Factorial function   cfa 10364
            4.6.9  The binomial coefficient operation   cbc 10386
            4.6.10  The ` # ` (set size) function   chash 10414
      ​4.7  Elementary real and complex functions
            4.7.1  The "shift" operation   cshi 10479
            4.7.2  Real and imaginary parts; conjugate   ccj 10504
            4.7.3  Sequence convergence   caucvgrelemrec 10643
            4.7.4  Square root; absolute value   csqrt 10660
            4.7.5  The maximum of two real numbers   maxcom 10867
            4.7.6  The minimum of two real numbers   mincom 10892
            4.7.7  The maximum of two extended reals   xrmaxleim 10905
            4.7.8  The minimum of two extended reals   xrnegiso 10923
      ​4.8  Elementary limits and convergence
            4.8.1  Limits   cli 10939
            4.8.2  Finite and infinite sums   csu 11014
            4.8.3  The binomial theorem   binomlem 11144
            4.8.4  Infinite sums (cont.)   isumshft 11151
            4.8.5  Miscellaneous converging and diverging sequences   divcnv 11158
            4.8.6  Arithmetic series   arisum 11159
            4.8.7  Geometric series   expcnvap0 11163
            4.8.8  Ratio test for infinite series convergence   cvgratnnlembern 11184
            4.8.9  Mertens' theorem   mertenslemub 11195
      ​4.9  Elementary trigonometry
            4.9.1  The exponential, sine, and cosine functions   ce 11199
            4.9.2  _e is irrational   eirraplem 11331
​​*PART 5  ELEMENTARY NUMBER THEORY
      ​5.1  Elementary properties of divisibility
            5.1.1  The divides relation   cdvds 11341
            ​*5.1.2  Even and odd numbers   evenelz 11412
            5.1.3  The division algorithm   divalglemnn 11463
            5.1.4  The greatest common divisor operator   cgcd 11483
            5.1.5  Bézout's identity   bezoutlemnewy 11530
            5.1.6  Algorithms   nn0seqcvgd 11568
            5.1.7  Euclid's Algorithm   eucalgval2 11580
            ​*5.1.8  The least common multiple   clcm 11587
            ​*5.1.9  Coprimality and Euclid's lemma   coprmgcdb 11615
            5.1.10  Cancellability of congruences   congr 11627
      ​5.2  Elementary prime number theory
            ​*5.2.1  Elementary properties   cprime 11634
            ​*5.2.2  Coprimality and Euclid's lemma (cont.)   coprm 11668
            5.2.3  Non-rationality of square root of 2   sqrt2irrlem 11685
            5.2.4  Properties of the canonical representation of a rational   cnumer 11704
            5.2.5  Euler's theorem   cphi 11731
      ​5.3  Cardinality of real and complex number subsets
            5.3.1  Countability of integers and rationals   oddennn 11750
​PART 6  BASIC STRUCTURES
      ​6.1  Extensible structures
            ​*6.1.1  Basic definitions   cstr 11798
            6.1.2  Slot definitions   cplusg 11864
            6.1.3  Definition of the structure product   crest 11963
      ​6.2  The complex numbers as an algebraic extensible structure
            6.2.1  Definition and basic properties   cpsmet 11991
​PART 7  BASIC TOPOLOGY
      ​7.1  Topology
            ​*7.1.1  Topological spaces   ctop 12007
                  7.1.1.1  Topologies   ctop 12007
                  7.1.1.2  Topologies on sets   ctopon 12020
                  7.1.1.3  Topological spaces   ctps 12040
            7.1.2  Topological bases   ctb 12052
            7.1.3  Examples of topologies   distop 12097
            7.1.4  Closure and interior   ccld 12104
            7.1.5  Neighborhoods   cnei 12150
            7.1.6  Subspace topologies   restrcl 12179
            7.1.7  Limits and continuity in topological spaces   ccn 12197
            7.1.8  Product topologies   ctx 12263
            7.1.9  Continuous function-builders   cnmptid 12292
      ​7.2  Metric spaces
            7.2.1  Pseudometric spaces   psmetrel 12311
            7.2.2  Basic metric space properties   cxms 12325
            7.2.3  Metric space balls   blfvalps 12374
            7.2.4  Open sets of a metric space   mopnrel 12430
            7.2.5  Continuity in metric spaces   metcnp3 12500
            7.2.6  Topology on the reals   qtopbasss 12510
            7.2.7  Topological definitions using the reals   ccncf 12543
​PART 8  BASIC REAL AND COMPLEX ANALYSIS
      ​8.1  Derivatives
            8.1.1  Real and complex differentiation   climc 12579
                  8.1.1.1  Derivatives of functions of one complex or real variable   climc 12579
​PART 9  GUIDES AND MISCELLANEA
      ​9.1  Guides (conventions, explanations, and examples)
            ​*9.1.1  Conventions   conventions 12626
            9.1.2  Definitional examples   ex-or 12627
​PART 10  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​10.1  Mathboxes for user contributions
            10.1.1  Mathbox guidelines   mathbox 12637
      ​10.2  Mathbox for BJ
            10.2.1  Propositional calculus   bj-nnsn 12638
                  10.2.1.1  Stable formulas   bj-trst 12643
                  10.2.1.2  Decidable formulas   bj-trdc 12650
            10.2.2  Predicate calculus   bj-ex 12660
            ​*10.2.3  Extensionality   bj-vtoclgft 12672
            ​*10.2.4  Decidability of classes   wdcin 12690
            10.2.5  Disjoint union   djucllem 12697
            ​*10.2.6  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 12700
                  *10.2.6.1  Bounded formulas   wbd 12700
                  ​*10.2.6.2  Bounded classes   wbdc 12728
            ​*10.2.7  CZF: Bounded separation   ax-bdsep 12772
                  10.2.7.1  Delta_0-classical logic   ax-bj-d0cl 12812
                  10.2.7.2  Inductive classes and the class of natural numbers (finite ordinals)   wind 12814
                  ​*10.2.7.3  The first three Peano postulates   bj-peano2 12827
            ​*10.2.8  CZF: Infinity   ax-infvn 12829
                  *10.2.8.1  The set of natural numbers (finite ordinals)   ax-infvn 12829
                  ​*10.2.8.2  Peano's fifth postulate   bdpeano5 12831
                  ​*10.2.8.3  Bounded induction and Peano's fourth postulate   findset 12833
            ​*10.2.9  CZF: Set induction   setindft 12853
                  *10.2.9.1  Set induction   setindft 12853
                  ​*10.2.9.2  Full induction   bj-findis 12867
            ​*10.2.10  CZF: Strong collection   ax-strcoll 12870
            ​*10.2.11  CZF: Subset collection   ax-sscoll 12875
            10.2.12  Real numbers   ax-ddkcomp 12877
      ​10.3  Mathbox for Jim Kingdon
            10.3.1  Natural numbers   el2oss1o 12878
            10.3.2  The power set of a singleton   pwtrufal 12882
            10.3.3  Omniscience of NN+oo   0nninf 12887
            10.3.4  Schroeder-Bernstein Theorem   exmidsbthrlem 12907
            10.3.5  Real and complex numbers   qdencn 12912
            10.3.6  Supremum and infimum   supfz 12927
      ​10.4  Mathbox for Mykola Mostovenko
      ​10.5  Mathbox for David A. Wheeler
            10.5.1  Testable propositions   dftest 12930
            ​*10.5.2  Allsome quantifier   walsi 12931