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
      3.9  Elementary trigonometry
PART 4  ELEMENTARY NUMBER THEORY
      4.1  Elementary properties of divisibility
      4.2  Elementary prime number theory
      4.3  Cardinality of real and complex number subsets
PART 5  BASIC STRUCTURES
      5.1  Extensible structures
      5.2  The complex numbers as an algebraic extensible structure
PART 6  BASIC TOPOLOGY
      6.1  Topology
      6.2  Metric spaces
PART 7  BASIC REAL AND COMPLEX ANALYSIS
      7.1  Derivatives
PART 8  GUIDES AND MISCELLANEA
      8.1  Guides (conventions, explanations, and examples)
PART 9  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
      ​9.1  Mathboxes for user contributions
      9.2  Mathbox for BJ
      9.3  Mathbox for Jim Kingdon
      9.4  Mathbox for Mykola Mostovenko
      9.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 818
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 882
            1.2.11  Abbreviated conjunction and disjunction of three wff's   w3o 942
            1.2.12  True and false constants   wal 1310
                  ​*1.2.12.1  Universal quantifier for use by df-tru   wal 1310
                  ​*1.2.12.2  Equality predicate for use by df-tru   cv 1311
                  1.2.12.3  Define the true and false constants   wtru 1313
            1.2.13  Logical 'xor'   wxo 1334
            ​*1.2.14  Truth tables: Operations on true and false constants   truantru 1360
            ​*1.2.15  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1382
            1.2.16  Logical implication (continued)   syl6an 1391
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1404
            ​*1.3.2  Equality predicate (continued)   weq 1460
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1487
            1.3.4  Introduce Axiom of Existence   ax-i9 1491
            1.3.5  Additional intuitionistic axioms   ax-ial 1495
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1497
            1.3.7  The existential quantifier   19.8a 1550
            1.3.8  Equality theorems without distinct variables   a9e 1655
            1.3.9  Axioms ax-10 and ax-11   ax10o 1674
            1.3.10  Substitution (without distinct variables)   wsb 1716
            1.3.11  Theorems using axiom ax-11   equs5a 1746
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1763
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1774
            1.4.3  More theorems related to ax-11 and substitution   albidv 1776
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1810
            1.4.5  More substitution theorems   hbs1 1887
            1.4.6  Existential uniqueness   weu 1973
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2071
​​*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 2095
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2099
            2.1.3  Class form not-free predicate   wnfc 2240
            2.1.4  Negated equality and membership   wne 2280
                  2.1.4.1  Negated equality   wne 2280
                  2.1.4.2  Negated membership   wnel 2375
            2.1.5  Restricted quantification   wral 2388
            2.1.6  The universal class   cvv 2655
            ​*2.1.7  Conditional equality (experimental)   wcdeq 2859
            2.1.8  Russell's Paradox   ru 2875
            2.1.9  Proper substitution of classes for sets   wsbc 2876
            2.1.10  Proper substitution of classes for sets into classes   csb 2969
            2.1.11  Define basic set operations and relations   cdif 3032
            2.1.12  Subclasses and subsets   df-ss 3048
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3150
                  2.1.13.1  The difference of two classes   dfdif3 3150
                  2.1.13.2  The union of two classes   elun 3181
                  2.1.13.3  The intersection of two classes   elin 3223
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3271
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3306
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3320
            2.1.14  The empty set   c0 3327
            2.1.15  Conditional operator   cif 3438
            2.1.16  Power classes   cpw 3474
            2.1.17  Unordered and ordered pairs   csn 3491
            2.1.18  The union of a class   cuni 3700
            2.1.19  The intersection of a class   cint 3735
            2.1.20  Indexed union and intersection   ciun 3777
            2.1.21  Disjointness   wdisj 3870
            2.1.22  Binary relations   wbr 3893
            2.1.23  Ordered-pair class abstractions (class builders)   copab 3946
            2.1.24  Transitive classes   wtr 3984
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4001
            2.2.2  Introduce the Axiom of Separation   ax-sep 4004
            2.2.3  Derive the Null Set Axiom   zfnuleu 4010
            2.2.4  Theorems requiring subset and intersection existence   nalset 4016
            2.2.5  Theorems requiring empty set existence   class2seteq 4045
            2.2.6  Collection principle   bnd 4054
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4056
            2.3.2  A notation for excluded middle   wem 4076
            2.3.3  Axiom of Pairing   ax-pr 4089
            2.3.4  Ordered pair theorem   opm 4114
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4137
            2.3.6  Power class of union and intersection   pwin 4162
            2.3.7  Epsilon and identity relations   cep 4167
            2.3.8  Partial and complete ordering   wpo 4174
            2.3.9  Founded and set-like relations   wfrfor 4207
            2.3.10  Ordinals   word 4242
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4313
            2.4.2  Ordinals (continued)   ordon 4360
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4405
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4410
            2.5.3  Transfinite induction   tfi 4454
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4460
            2.6.2  The natural numbers (i.e. finite ordinals)   com 4462
            2.6.3  Peano's postulates   peano1 4466
            2.6.4  Finite induction (for finite ordinals)   find 4471
            2.6.5  The Natural Numbers (continued)   nn0suc 4476
            2.6.6  Relations   cxp 4495
            2.6.7  Definite description binder (inverted iota)   cio 5042
            2.6.8  Functions   wfun 5073
            2.6.9  Restricted iota (description binder)   crio 5681
            2.6.10  Operations   co 5726
            2.6.11  Maps-to notation   elmpocl 5920
            2.6.12  Function operation   cof 5932
            2.6.13  Functions (continued)   resfunexgALT 5959
            2.6.14  First and second members of an ordered pair   c1st 5987
            ​*2.6.15  Special maps-to operations   opeliunxp2f 6086
            2.6.16  Function transposition   ctpos 6092
            2.6.17  Undefined values   pwuninel2 6130
            2.6.18  Functions on ordinals; strictly monotone ordinal functions   iunon 6132
            2.6.19  "Strong" transfinite recursion   crecs 6152
            2.6.20  Recursive definition generator   crdg 6217
            2.6.21  Finite recursion   cfrec 6238
            2.6.22  Ordinal arithmetic   c1o 6257
            2.6.23  Natural number arithmetic   nna0 6321
            2.6.24  Equivalence relations and classes   wer 6377
            2.6.25  The mapping operation   cmap 6493
            2.6.26  Infinite Cartesian products   cixp 6543
            2.6.27  Equinumerosity   cen 6583
            2.6.28  Equinumerosity (cont.)   xpf1o 6688
            2.6.29  Pigeonhole Principle   phplem1 6696
            2.6.30  Finite sets   fict 6712
            2.6.31  Schroeder-Bernstein Theorem   sbthlem1 6794
            2.6.32  Finite intersections   cfi 6805
            2.6.33  Supremum and infimum   csup 6818
            2.6.34  Ordinal isomorphism   ordiso2 6869
            2.6.35  Disjoint union   cdju 6871
                  2.6.35.1  Disjoint union   cdju 6871
                  ​*2.6.35.2  Left and right injections of a disjoint union   cinl 6879
                  2.6.35.3  Universal property of the disjoint union   djuss 6904
                  2.6.35.4  Dominance and equinumerosity properties of disjoint union   djudom 6927
                  2.6.35.5  Older definition temporarily kept for comparison, to be deleted   cdjud 6936
                  2.6.35.6  Countable sets   0ct 6941
            2.6.36  Omniscient sets   comni 6951
            2.6.37  Markov's principle   cmarkov 6972
            2.6.38  Cardinal numbers   ccrd 6981
            2.6.39  Axiom of Choice equivalents   wac 7005
            2.6.40  Cardinal number arithmetic   endjudisj 7010
​​*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 7021
            3.1.2  Final derivation of real and complex number postulates   axcnex 7587
            3.1.3  Real and complex number postulates restated as axioms   ax-cnex 7629
      ​3.2  Derive the basic properties from the field axioms
            3.2.1  Some deductions from the field axioms for complex numbers   cnex 7661
            3.2.2  Infinity and the extended real number system   cpnf 7714
            3.2.3  Restate the ordering postulates with extended real "less than"   axltirr 7748
            3.2.4  Ordering on reals   lttr 7754
            3.2.5  Initial properties of the complex numbers   mul12 7807
      ​3.3  Real and complex numbers - basic operations
            3.3.1  Addition   add12 7836
            3.3.2  Subtraction   cmin 7849
            3.3.3  Multiplication   kcnktkm1cn 8057
            3.3.4  Ordering on reals (cont.)   ltadd2 8093
            3.3.5  Real Apartness   creap 8247
            3.3.6  Complex Apartness   cap 8254
            3.3.7  Reciprocals   recextlem1 8318
            3.3.8  Division   cdiv 8338
            3.3.9  Ordering on reals (cont.)   ltp1 8505
            3.3.10  Suprema   lbreu 8606
            3.3.11  Imaginary and complex number properties   crap0 8619
      ​3.4  Integer sets
            3.4.1  Positive integers (as a subset of complex numbers)   cn 8623
            3.4.2  Principle of mathematical induction   nnind 8639
            ​*3.4.3  Decimal representation of numbers   c2 8674
            ​*3.4.4  Some properties of specific numbers   neg1cn 8728
            3.4.5  Simple number properties   halfcl 8843
            3.4.6  The Archimedean property   arch 8871
            3.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 8874
            ​*3.4.8  Extended nonnegative integers   cxnn0 8937
            3.4.9  Integers (as a subset of complex numbers)   cz 8951
            3.4.10  Decimal arithmetic   cdc 9079
            3.4.11  Upper sets of integers   cuz 9221
            3.4.12  Rational numbers (as a subset of complex numbers)   cq 9306
            3.4.13  Complex numbers as pairs of reals   cnref1o 9335
      ​3.5  Order sets
            3.5.1  Positive reals (as a subset of complex numbers)   crp 9336
            3.5.2  Infinity and the extended real number system (cont.)   cxne 9442
            3.5.3  Real number intervals   cioo 9557
            3.5.4  Finite intervals of integers   cfz 9676
            ​*3.5.5  Finite intervals of nonnegative integers   elfz2nn0 9778
            3.5.6  Half-open integer ranges   cfzo 9805
            3.5.7  Rational numbers (cont.)   qtri3or 9906
      ​3.6  Elementary integer functions
            3.6.1  The floor and ceiling functions   cfl 9927
            3.6.2  The modulo (remainder) operation   cmo 9981
            3.6.3  Miscellaneous theorems about integers   frec2uz0d 10058
            3.6.4  Strong induction over upper sets of integers   uzsinds 10101
            3.6.5  The infinite sequence builder "seq"   cseq 10104
            3.6.6  Integer powers   cexp 10178
            3.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 10351
            3.6.8  Factorial function   cfa 10357
            3.6.9  The binomial coefficient operation   cbc 10379
            3.6.10  The ` # ` (set size) function   chash 10407
      ​3.7  Elementary real and complex functions
            3.7.1  The "shift" operation   cshi 10472
            3.7.2  Real and imaginary parts; conjugate   ccj 10497
            3.7.3  Sequence convergence   caucvgrelemrec 10636
            3.7.4  Square root; absolute value   csqrt 10653
            3.7.5  The maximum of two real numbers   maxcom 10860
            3.7.6  The minimum of two real numbers   mincom 10885
            3.7.7  The maximum of two extended reals   xrmaxleim 10898
            3.7.8  The minimum of two extended reals   xrnegiso 10916
      ​3.8  Elementary limits and convergence
            3.8.1  Limits   cli 10932
            3.8.2  Finite and infinite sums   csu 11007
            3.8.3  The binomial theorem   binomlem 11137
            3.8.4  Infinite sums (cont.)   isumshft 11144
            3.8.5  Miscellaneous converging and diverging sequences   divcnv 11151
            3.8.6  Arithmetic series   arisum 11152
            3.8.7  Geometric series   expcnvap0 11156
            3.8.8  Ratio test for infinite series convergence   cvgratnnlembern 11177
            3.8.9  Mertens' theorem   mertenslemub 11188
      ​3.9  Elementary trigonometry
            3.9.1  The exponential, sine, and cosine functions   ce 11192
            3.9.2  _e is irrational   eirraplem 11324
​​*PART 4  ELEMENTARY NUMBER THEORY
      ​4.1  Elementary properties of divisibility
            4.1.1  The divides relation   cdvds 11334
            ​*4.1.2  Even and odd numbers   evenelz 11405
            4.1.3  The division algorithm   divalglemnn 11456
            4.1.4  The greatest common divisor operator   cgcd 11476
            4.1.5  Bézout's identity   bezoutlemnewy 11523
            4.1.6  Algorithms   nn0seqcvgd 11561
            4.1.7  Euclid's Algorithm   eucalgval2 11573
            ​*4.1.8  The least common multiple   clcm 11580
            ​*4.1.9  Coprimality and Euclid's lemma   coprmgcdb 11608
            4.1.10  Cancellability of congruences   congr 11620
      ​4.2  Elementary prime number theory
            ​*4.2.1  Elementary properties   cprime 11627
            ​*4.2.2  Coprimality and Euclid's lemma (cont.)   coprm 11661
            4.2.3  Non-rationality of square root of 2   sqrt2irrlem 11678
            4.2.4  Properties of the canonical representation of a rational   cnumer 11697
            4.2.5  Euler's theorem   cphi 11724
      ​4.3  Cardinality of real and complex number subsets
            4.3.1  Countability of integers and rationals   oddennn 11743
​PART 5  BASIC STRUCTURES
      ​5.1  Extensible structures
            ​*5.1.1  Basic definitions   cstr 11791
            5.1.2  Slot definitions   cplusg 11857
            5.1.3  Definition of the structure product   crest 11956
      ​5.2  The complex numbers as an algebraic extensible structure
            5.2.1  Definition and basic properties   cpsmet 11984
​PART 6  BASIC TOPOLOGY
      ​6.1  Topology
            ​*6.1.1  Topological spaces   ctop 12000
                  6.1.1.1  Topologies   ctop 12000
                  6.1.1.2  Topologies on sets   ctopon 12013
                  6.1.1.3  Topological spaces   ctps 12033
            6.1.2  Topological bases   ctb 12045
            6.1.3  Examples of topologies   distop 12090
            6.1.4  Closure and interior   ccld 12097
            6.1.5  Neighborhoods   cnei 12143
            6.1.6  Subspace topologies   restrcl 12172
            6.1.7  Limits and continuity in topological spaces   ccn 12190
            6.1.8  Product topologies   ctx 12256
            6.1.9  Continuous function-builders   cnmptid 12285
      ​6.2  Metric spaces
            6.2.1  Pseudometric spaces   psmetrel 12304
            6.2.2  Basic metric space properties   cxms 12318
            6.2.3  Metric space balls   blfvalps 12367
            6.2.4  Open sets of a metric space   mopnrel 12423
            6.2.5  Continuity in metric spaces   metcnp3 12493
            6.2.6  Topology on the reals   qtopbasss 12503
            6.2.7  Topological definitions using the reals   ccncf 12536
​PART 7  BASIC REAL AND COMPLEX ANALYSIS
      ​7.1  Derivatives
            7.1.1  Real and complex differentiation   climc 12572
                  7.1.1.1  Derivatives of functions of one complex or real variable   climc 12572
​PART 8  GUIDES AND MISCELLANEA
      ​8.1  Guides (conventions, explanations, and examples)
            ​*8.1.1  Conventions   conventions 12613
            8.1.2  Definitional examples   ex-or 12614
​PART 9  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
      ​9.1  Mathboxes for user contributions
            9.1.1  Mathbox guidelines   mathbox 12624
      ​9.2  Mathbox for BJ
            9.2.1  Propositional calculus   bj-nnsn 12625
                  9.2.1.1  Stable formulas   bj-trst 12630
                  9.2.1.2  Decidable formulas   bj-trdc 12637
            9.2.2  Predicate calculus   bj-ex 12649
            ​*9.2.3  Extensionality   bj-vtoclgft 12661
            ​*9.2.4  Decidability of classes   wdcin 12679
            9.2.5  Disjoint union   djucllem 12686
            ​*9.2.6  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 12689
                  *9.2.6.1  Bounded formulas   wbd 12689
                  ​*9.2.6.2  Bounded classes   wbdc 12717
            ​*9.2.7  CZF: Bounded separation   ax-bdsep 12761
                  9.2.7.1  Delta_0-classical logic   ax-bj-d0cl 12801
                  9.2.7.2  Inductive classes and the class of natural numbers (finite ordinals)   wind 12803
                  ​*9.2.7.3  The first three Peano postulates   bj-peano2 12816
            ​*9.2.8  CZF: Infinity   ax-infvn 12818
                  *9.2.8.1  The set of natural numbers (finite ordinals)   ax-infvn 12818
                  ​*9.2.8.2  Peano's fifth postulate   bdpeano5 12820
                  ​*9.2.8.3  Bounded induction and Peano's fourth postulate   findset 12822
            ​*9.2.9  CZF: Set induction   setindft 12842
                  *9.2.9.1  Set induction   setindft 12842
                  ​*9.2.9.2  Full induction   bj-findis 12856
            ​*9.2.10  CZF: Strong collection   ax-strcoll 12859
            ​*9.2.11  CZF: Subset collection   ax-sscoll 12864
            9.2.12  Real numbers   ax-ddkcomp 12866
      ​9.3  Mathbox for Jim Kingdon
            9.3.1  Natural numbers   el2oss1o 12867
            9.3.2  The power set of a singleton   pwtrufal 12871
            9.3.3  Omniscience of NN+oo   0nninf 12874
            9.3.4  Schroeder-Bernstein Theorem   exmidsbthrlem 12894
            9.3.5  Real and complex numbers   qdencn 12899
            9.3.6  Supremum and infimum   supfz 12914
      ​9.4  Mathbox for Mykola Mostovenko
      ​9.5  Mathbox for David A. Wheeler
            9.5.1  Testable propositions   dftest 12917
            ​*9.5.2  Allsome quantifier   walsi 12918