TOC of Theorem List - Intuitionistic Logic Explorer

Table of Contents Summary

PART 1  INTUITIONISTIC 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  BASIC REAL AND COMPLEX FUNCTIONS
      9.1  Basic trigonometry
PART 10  GUIDES AND MISCELLANEA
      10.1  Guides (conventions, explanations, and examples)
PART 11  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​11.1  Mathboxes for user contributions
      11.2  Mathbox for BJ
      11.3  Mathbox for Jim Kingdon
      11.4  Mathbox for Mykola Mostovenko
      11.5  Mathbox for David A. Wheeler

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

​​*PART 1  INTUITIONISTIC 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-mp 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 603
            1.2.6  Logical disjunction   wo 697
            1.2.7  Stable propositions   wstab 815
            1.2.8  Decidable propositions   wdc 819
            ​*1.2.9  Theorems of decidable propositions   const 837
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 901
            1.2.11  Abbreviated conjunction and disjunction of three wff's   w3o 961
            1.2.12  True and false constants   wal 1329
                  ​*1.2.12.1  Universal quantifier for use by df-tru   wal 1329
                  ​*1.2.12.2  Equality predicate for use by df-tru   cv 1330
                  1.2.12.3  Define the true and false constants   wtru 1332
            1.2.13  Logical 'xor'   wxo 1353
            ​*1.2.14  Truth tables: Operations on true and false constants   truantru 1379
            ​*1.2.15  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1401
            1.2.16  Logical implication (continued)   syl6an 1410
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1423
            ​*1.3.2  Equality predicate (continued)   weq 1479
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1506
            1.3.4  Introduce Axiom of Existence   ax-i9 1510
            1.3.5  Additional intuitionistic axioms   ax-ial 1514
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1516
            1.3.7  The existential quantifier   19.8a 1569
            1.3.8  Equality theorems without distinct variables   a9e 1674
            1.3.9  Axioms ax-10 and ax-11   ax10o 1693
            1.3.10  Substitution (without distinct variables)   wsb 1735
            1.3.11  Theorems using axiom ax-11   equs5a 1766
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1783
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1794
            1.4.3  More theorems related to ax-11 and substitution   albidv 1796
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1830
            1.4.5  More substitution theorems   hbs1 1911
            1.4.6  Existential uniqueness   weu 1999
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2097
​​*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 2121
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2125
            2.1.3  Class form not-free predicate   wnfc 2268
            2.1.4  Negated equality and membership   wne 2308
                  2.1.4.1  Negated equality   wne 2308
                  2.1.4.2  Negated membership   wnel 2403
            2.1.5  Restricted quantification   wral 2416
            2.1.6  The universal class   cvv 2686
            ​*2.1.7  Conditional equality (experimental)   wcdeq 2892
            2.1.8  Russell's Paradox   ru 2908
            2.1.9  Proper substitution of classes for sets   wsbc 2909
            2.1.10  Proper substitution of classes for sets into classes   csb 3003
            2.1.11  Define basic set operations and relations   cdif 3068
            2.1.12  Subclasses and subsets   df-ss 3084
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3186
                  2.1.13.1  The difference of two classes   dfdif3 3186
                  2.1.13.2  The union of two classes   elun 3217
                  2.1.13.3  The intersection of two classes   elin 3259
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3307
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3342
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3356
            2.1.14  The empty set   c0 3363
            2.1.15  Conditional operator   cif 3474
            2.1.16  Power classes   cpw 3510
            2.1.17  Unordered and ordered pairs   csn 3527
            2.1.18  The union of a class   cuni 3736
            2.1.19  The intersection of a class   cint 3771
            2.1.20  Indexed union and intersection   ciun 3813
            2.1.21  Disjointness   wdisj 3906
            2.1.22  Binary relations   wbr 3929
            2.1.23  Ordered-pair class abstractions (class builders)   copab 3988
            2.1.24  Transitive classes   wtr 4026
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4043
            2.2.2  Introduce the Axiom of Separation   ax-sep 4046
            2.2.3  Derive the Null Set Axiom   zfnuleu 4052
            2.2.4  Theorems requiring subset and intersection existence   nalset 4058
            2.2.5  Theorems requiring empty set existence   class2seteq 4087
            2.2.6  Collection principle   bnd 4096
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4098
            2.3.2  A notation for excluded middle   wem 4118
            2.3.3  Axiom of Pairing   ax-pr 4131
            2.3.4  Ordered pair theorem   opm 4156
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4179
            2.3.6  Power class of union and intersection   pwin 4204
            2.3.7  Epsilon and identity relations   cep 4209
            2.3.8  Partial and complete ordering   wpo 4216
            2.3.9  Founded and set-like relations   wfrfor 4249
            2.3.10  Ordinals   word 4284
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4355
            2.4.2  Ordinals (continued)   ordon 4402
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4447
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4452
            2.5.3  Transfinite induction   tfi 4496
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4502
            2.6.2  The natural numbers (i.e. finite ordinals)   com 4504
            2.6.3  Peano's postulates   peano1 4508
            2.6.4  Finite induction (for finite ordinals)   find 4513
            2.6.5  The Natural Numbers (continued)   nn0suc 4518
            2.6.6  Relations   cxp 4537
            2.6.7  Definite description binder (inverted iota)   cio 5086
            2.6.8  Functions   wfun 5117
            2.6.9  Restricted iota (description binder)   crio 5729
            2.6.10  Operations   co 5774
            2.6.11  Maps-to notation   elmpocl 5968
            2.6.12  Function operation   cof 5980
            2.6.13  Functions (continued)   resfunexgALT 6008
            2.6.14  First and second members of an ordered pair   c1st 6036
            ​*2.6.15  Special maps-to operations   opeliunxp2f 6135
            2.6.16  Function transposition   ctpos 6141
            2.6.17  Undefined values   pwuninel2 6179
            2.6.18  Functions on ordinals; strictly monotone ordinal functions   iunon 6181
            2.6.19  "Strong" transfinite recursion   crecs 6201
            2.6.20  Recursive definition generator   crdg 6266
            2.6.21  Finite recursion   cfrec 6287
            2.6.22  Ordinal arithmetic   c1o 6306
            2.6.23  Natural number arithmetic   nna0 6370
            2.6.24  Equivalence relations and classes   wer 6426
            2.6.25  The mapping operation   cmap 6542
            2.6.26  Infinite Cartesian products   cixp 6592
            2.6.27  Equinumerosity   cen 6632
            2.6.28  Equinumerosity (cont.)   xpf1o 6738
            2.6.29  Pigeonhole Principle   phplem1 6746
            2.6.30  Finite sets   fict 6762
            2.6.31  Schroeder-Bernstein Theorem   sbthlem1 6845
            2.6.32  Finite intersections   cfi 6856
            2.6.33  Supremum and infimum   csup 6869
            2.6.34  Ordinal isomorphism   ordiso2 6920
            2.6.35  Disjoint union   cdju 6922
                  2.6.35.1  Disjoint union   cdju 6922
                  ​*2.6.35.2  Left and right injections of a disjoint union   cinl 6930
                  2.6.35.3  Universal property of the disjoint union   djuss 6955
                  2.6.35.4  Dominance and equinumerosity properties of disjoint union   djudom 6978
                  2.6.35.5  Older definition temporarily kept for comparison, to be deleted   cdjud 6987
                  2.6.35.6  Countable sets   0ct 6992
            2.6.36  Omniscient sets   comni 7004
            2.6.37  Markov's principle   cmarkov 7025
            2.6.38  Cardinal numbers   ccrd 7035
            2.6.39  Axiom of Choice equivalents   wac 7061
            2.6.40  Cardinal number arithmetic   endjudisj 7066
​​*PART 3  CHOICE PRINCIPLES
      ​3.1  Countable Choice and Dependent Choice
            3.1.1  Introduce Countable Choice   wacc 7077
​​*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 7080
            4.1.2  Final derivation of real and complex number postulates   axcnex 7667
            4.1.3  Real and complex number postulates restated as axioms   ax-cnex 7711
      ​4.2  Derive the basic properties from the field axioms
            4.2.1  Some deductions from the field axioms for complex numbers   cnex 7744
            4.2.2  Infinity and the extended real number system   cpnf 7797
            4.2.3  Restate the ordering postulates with extended real "less than"   axltirr 7831
            4.2.4  Ordering on reals   lttr 7838
            4.2.5  Initial properties of the complex numbers   mul12 7891
      ​4.3  Real and complex numbers - basic operations
            4.3.1  Addition   add12 7920
            4.3.2  Subtraction   cmin 7933
            4.3.3  Multiplication   kcnktkm1cn 8145
            4.3.4  Ordering on reals (cont.)   ltadd2 8181
            4.3.5  Real Apartness   creap 8336
            4.3.6  Complex Apartness   cap 8343
            4.3.7  Reciprocals   recextlem1 8412
            4.3.8  Division   cdiv 8432
            4.3.9  Ordering on reals (cont.)   ltp1 8602
            4.3.10  Suprema   lbreu 8703
            4.3.11  Imaginary and complex number properties   crap0 8716
      ​4.4  Integer sets
            4.4.1  Positive integers (as a subset of complex numbers)   cn 8720
            4.4.2  Principle of mathematical induction   nnind 8736
            ​*4.4.3  Decimal representation of numbers   c2 8771
            ​*4.4.4  Some properties of specific numbers   neg1cn 8825
            4.4.5  Simple number properties   halfcl 8946
            4.4.6  The Archimedean property   arch 8974
            4.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 8977
            ​*4.4.8  Extended nonnegative integers   cxnn0 9040
            4.4.9  Integers (as a subset of complex numbers)   cz 9054
            4.4.10  Decimal arithmetic   cdc 9182
            4.4.11  Upper sets of integers   cuz 9326
            4.4.12  Rational numbers (as a subset of complex numbers)   cq 9411
            4.4.13  Complex numbers as pairs of reals   cnref1o 9440
      ​4.5  Order sets
            4.5.1  Positive reals (as a subset of complex numbers)   crp 9441
            4.5.2  Infinity and the extended real number system (cont.)   cxne 9556
            4.5.3  Real number intervals   cioo 9671
            4.5.4  Finite intervals of integers   cfz 9790
            ​*4.5.5  Finite intervals of nonnegative integers   elfz2nn0 9892
            4.5.6  Half-open integer ranges   cfzo 9919
            4.5.7  Rational numbers (cont.)   qtri3or 10020
      ​4.6  Elementary integer functions
            4.6.1  The floor and ceiling functions   cfl 10041
            4.6.2  The modulo (remainder) operation   cmo 10095
            4.6.3  Miscellaneous theorems about integers   frec2uz0d 10172
            4.6.4  Strong induction over upper sets of integers   uzsinds 10215
            4.6.5  The infinite sequence builder "seq"   cseq 10218
            4.6.6  Integer powers   cexp 10292
            4.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 10465
            4.6.8  Factorial function   cfa 10471
            4.6.9  The binomial coefficient operation   cbc 10493
            4.6.10  The ` # ` (set size) function   chash 10521
      ​4.7  Elementary real and complex functions
            4.7.1  The "shift" operation   cshi 10586
            4.7.2  Real and imaginary parts; conjugate   ccj 10611
            4.7.3  Sequence convergence   caucvgrelemrec 10751
            4.7.4  Square root; absolute value   csqrt 10768
            4.7.5  The maximum of two real numbers   maxcom 10975
            4.7.6  The minimum of two real numbers   mincom 11000
            4.7.7  The maximum of two extended reals   xrmaxleim 11013
            4.7.8  The minimum of two extended reals   xrnegiso 11031
      ​4.8  Elementary limits and convergence
            4.8.1  Limits   cli 11047
            4.8.2  Finite and infinite sums   csu 11122
            4.8.3  The binomial theorem   binomlem 11252
            4.8.4  Infinite sums (cont.)   isumshft 11259
            4.8.5  Miscellaneous converging and diverging sequences   divcnv 11266
            4.8.6  Arithmetic series   arisum 11267
            4.8.7  Geometric series   expcnvap0 11271
            4.8.8  Ratio test for infinite series convergence   cvgratnnlembern 11292
            4.8.9  Mertens' theorem   mertenslemub 11303
            4.8.10  Finite and infinite products   prodf 11307
                  4.8.10.1  Product sequences   prodf 11307
                  4.8.10.2  Non-trivial convergence   ntrivcvgap 11317
                  4.8.10.3  Complex products   cprod 11319
      ​4.9  Elementary trigonometry
            4.9.1  The exponential, sine, and cosine functions   ce 11348
                  4.9.1.1  The circle constant (tau = 2 pi)   ctau 11481
            4.9.2  _e is irrational   eirraplem 11483
​​*PART 5  ELEMENTARY NUMBER THEORY
      ​5.1  Elementary properties of divisibility
            5.1.1  The divides relation   cdvds 11493
            ​*5.1.2  Even and odd numbers   evenelz 11564
            5.1.3  The division algorithm   divalglemnn 11615
            5.1.4  The greatest common divisor operator   cgcd 11635
            5.1.5  Bézout's identity   bezoutlemnewy 11684
            5.1.6  Algorithms   nn0seqcvgd 11722
            5.1.7  Euclid's Algorithm   eucalgval2 11734
            ​*5.1.8  The least common multiple   clcm 11741
            ​*5.1.9  Coprimality and Euclid's lemma   coprmgcdb 11769
            5.1.10  Cancellability of congruences   congr 11781
      ​5.2  Elementary prime number theory
            ​*5.2.1  Elementary properties   cprime 11788
            ​*5.2.2  Coprimality and Euclid's lemma (cont.)   coprm 11822
            5.2.3  Non-rationality of square root of 2   sqrt2irrlem 11839
            5.2.4  Properties of the canonical representation of a rational   cnumer 11859
            5.2.5  Euler's theorem   cphi 11886
      ​5.3  Cardinality of real and complex number subsets
            5.3.1  Countability of integers and rationals   oddennn 11905
​PART 6  BASIC STRUCTURES
      ​6.1  Extensible structures
            ​*6.1.1  Basic definitions   cstr 11955
            6.1.2  Slot definitions   cplusg 12021
            6.1.3  Definition of the structure product   crest 12120
      ​6.2  The complex numbers as an algebraic extensible structure
            6.2.1  Definition and basic properties   cpsmet 12148
​PART 7  BASIC TOPOLOGY
      ​7.1  Topology
            ​*7.1.1  Topological spaces   ctop 12164
                  7.1.1.1  Topologies   ctop 12164
                  7.1.1.2  Topologies on sets   ctopon 12177
                  7.1.1.3  Topological spaces   ctps 12197
            7.1.2  Topological bases   ctb 12209
            7.1.3  Examples of topologies   distop 12254
            7.1.4  Closure and interior   ccld 12261
            7.1.5  Neighborhoods   cnei 12307
            7.1.6  Subspace topologies   restrcl 12336
            7.1.7  Limits and continuity in topological spaces   ccn 12354
            7.1.8  Product topologies   ctx 12421
            7.1.9  Continuous function-builders   cnmptid 12450
            7.1.10  Homeomorphisms   chmeo 12469
      ​7.2  Metric spaces
            7.2.1  Pseudometric spaces   psmetrel 12491
            7.2.2  Basic metric space properties   cxms 12505
            7.2.3  Metric space balls   blfvalps 12554
            7.2.4  Open sets of a metric space   mopnrel 12610
            7.2.5  Continuity in metric spaces   metcnp3 12680
            7.2.6  Topology on the reals   qtopbasss 12690
            7.2.7  Topological definitions using the reals   ccncf 12726
​PART 8  BASIC REAL AND COMPLEX ANALYSIS
            8.0.1  Dedekind cuts   dedekindeulemuub 12764
            8.0.2  Intermediate value theorem   ivthinclemlm 12781
      ​8.1  Derivatives
            8.1.1  Real and complex differentiation   climc 12792
                  8.1.1.1  Derivatives of functions of one complex or real variable   climc 12792
​PART 9  BASIC REAL AND COMPLEX FUNCTIONS
      ​9.1  Basic trigonometry
            9.1.1  The exponential, sine, and cosine functions (cont.)   efcn 12857
            9.1.2  Properties of pi = 3.14159...   pilem1 12860
​PART 10  GUIDES AND MISCELLANEA
      ​10.1  Guides (conventions, explanations, and examples)
            ​*10.1.1  Conventions   conventions 12933
            10.1.2  Definitional examples   ex-or 12934
​PART 11  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​11.1  Mathboxes for user contributions
            11.1.1  Mathbox guidelines   mathbox 12944
      ​11.2  Mathbox for BJ
            11.2.1  Propositional calculus   bj-nnsn 12945
                  11.2.1.1  Stable formulas   bj-trst 12951
                  11.2.1.2  Decidable formulas   bj-trdc 12959
            11.2.2  Predicate calculus   bj-ex 12969
            11.2.3  Set theorey miscellaneous   bj-el2oss1o 12981
            ​*11.2.4  Extensionality   bj-vtoclgft 12982
            ​*11.2.5  Decidability of classes   wdcin 13000
            11.2.6  Disjoint union   djucllem 13007
            ​*11.2.7  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 13010
                  *11.2.7.1  Bounded formulas   wbd 13010
                  ​*11.2.7.2  Bounded classes   wbdc 13038
            ​*11.2.8  CZF: Bounded separation   ax-bdsep 13082
                  11.2.8.1  Delta_0-classical logic   ax-bj-d0cl 13122
                  11.2.8.2  Inductive classes and the class of natural numbers (finite ordinals)   wind 13124
                  ​*11.2.8.3  The first three Peano postulates   bj-peano2 13137
            ​*11.2.9  CZF: Infinity   ax-infvn 13139
                  *11.2.9.1  The set of natural numbers (finite ordinals)   ax-infvn 13139
                  ​*11.2.9.2  Peano's fifth postulate   bdpeano5 13141
                  ​*11.2.9.3  Bounded induction and Peano's fourth postulate   findset 13143
            ​*11.2.10  CZF: Set induction   setindft 13163
                  *11.2.10.1  Set induction   setindft 13163
                  ​*11.2.10.2  Full induction   bj-findis 13177
            ​*11.2.11  CZF: Strong collection   ax-strcoll 13180
            ​*11.2.12  CZF: Subset collection   ax-sscoll 13185
            11.2.13  Real numbers   ax-ddkcomp 13187
      ​11.3  Mathbox for Jim Kingdon
            11.3.1  Natural numbers   el2oss1o 13188
            11.3.2  The power set of a singleton   pwtrufal 13192
            11.3.3  Omniscience of NN+oo   0nninf 13197
            11.3.4  Schroeder-Bernstein Theorem   exmidsbthrlem 13217
            11.3.5  Real and complex numbers   qdencn 13222
            11.3.6  Supremum and infimum   supfz 13237
                  11.3.6.1  Circle constant   taupi 13239
      ​11.4  Mathbox for Mykola Mostovenko
      ​11.5  Mathbox for David A. Wheeler
            11.5.1  Testable propositions   dftest 13241
            ​*11.5.2  Allsome quantifier   walsi 13242