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
      1.5  First-order logic with one non-logical binary predicate
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 604
            1.2.6  Logical disjunction   wo 698
            1.2.7  Stable propositions   wstab 816
            1.2.8  Decidable propositions   wdc 820
            ​*1.2.9  Theorems of decidable propositions   const 838
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 902
            1.2.11  Abbreviated conjunction and disjunction of three wff's   w3o 962
            1.2.12  True and false constants   wal 1333
                  ​*1.2.12.1  Universal quantifier for use by df-tru   wal 1333
                  ​*1.2.12.2  Equality predicate for use by df-tru   cv 1334
                  1.2.12.3  Define the true and false constants   wtru 1336
            1.2.13  Logical 'xor'   wxo 1357
            ​*1.2.14  Truth tables: Operations on true and false constants   truantru 1383
            ​*1.2.15  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1405
            1.2.16  Logical implication (continued)   syl6an 1414
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1427
            ​*1.3.2  Equality predicate (continued)   weq 1483
            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 1570
            1.3.8  Equality theorems without distinct variables   a9e 1676
            1.3.9  Axioms ax-10 and ax-11   ax10o 1695
            1.3.10  Substitution (without distinct variables)   wsb 1742
            1.3.11  Theorems using axiom ax-11   equs5a 1774
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1791
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1802
            1.4.3  More theorems related to ax-11 and substitution   albidv 1804
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1838
            1.4.5  More substitution theorems   hbs1 1918
            1.4.6  Existential uniqueness   weu 2006
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2104
      ​​*1.5  First-order logic with one non-logical binary predicate
​​*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 2139
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2143
            2.1.3  Class form not-free predicate   wnfc 2286
            2.1.4  Negated equality and membership   wne 2327
                  2.1.4.1  Negated equality   wne 2327
                  2.1.4.2  Negated membership   wnel 2422
            2.1.5  Restricted quantification   wral 2435
            2.1.6  The universal class   cvv 2712
            ​*2.1.7  Conditional equality (experimental)   wcdeq 2920
            2.1.8  Russell's Paradox   ru 2936
            2.1.9  Proper substitution of classes for sets   wsbc 2937
            2.1.10  Proper substitution of classes for sets into classes   csb 3031
            2.1.11  Define basic set operations and relations   cdif 3099
            2.1.12  Subclasses and subsets   df-ss 3115
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3217
                  2.1.13.1  The difference of two classes   dfdif3 3217
                  2.1.13.2  The union of two classes   elun 3248
                  2.1.13.3  The intersection of two classes   elin 3290
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3338
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3373
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3387
            2.1.14  The empty set   c0 3394
            2.1.15  Conditional operator   cif 3505
            2.1.16  Power classes   cpw 3543
            2.1.17  Unordered and ordered pairs   csn 3560
            2.1.18  The union of a class   cuni 3772
            2.1.19  The intersection of a class   cint 3807
            2.1.20  Indexed union and intersection   ciun 3849
            2.1.21  Disjointness   wdisj 3942
            2.1.22  Binary relations   wbr 3965
            2.1.23  Ordered-pair class abstractions (class builders)   copab 4024
            2.1.24  Transitive classes   wtr 4062
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4079
            2.2.2  Introduce the Axiom of Separation   ax-sep 4082
            2.2.3  Derive the Null Set Axiom   zfnuleu 4088
            2.2.4  Theorems requiring subset and intersection existence   nalset 4094
            2.2.5  Theorems requiring empty set existence   class2seteq 4124
            2.2.6  Collection principle   bnd 4133
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4135
            2.3.2  A notation for excluded middle   wem 4155
            2.3.3  Axiom of Pairing   ax-pr 4169
            2.3.4  Ordered pair theorem   opm 4194
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4217
            2.3.6  Power class of union and intersection   pwin 4242
            2.3.7  Epsilon and identity relations   cep 4247
            ​*2.3.8  Partial and total orderings   wpo 4254
            2.3.9  Founded and set-like relations   wfrfor 4287
            2.3.10  Ordinals   word 4322
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4393
            2.4.2  Ordinals (continued)   ordon 4444
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4490
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4495
            2.5.3  Transfinite induction   tfi 4540
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4546
            2.6.2  The natural numbers   com 4548
            2.6.3  Peano's postulates   peano1 4552
            2.6.4  Finite induction (for finite ordinals)   find 4557
            2.6.5  The Natural Numbers (continued)   nn0suc 4562
            2.6.6  Relations   cxp 4583
            2.6.7  Definite description binder (inverted iota)   cio 5132
            2.6.8  Functions   wfun 5163
            2.6.9  Cantor's Theorem   canth 5775
            2.6.10  Restricted iota (description binder)   crio 5776
            2.6.11  Operations   co 5821
            2.6.12  Maps-to notation   elmpocl 6015
            2.6.13  Function operation   cof 6027
            2.6.14  Functions (continued)   resfunexgALT 6055
            2.6.15  First and second members of an ordered pair   c1st 6083
            ​*2.6.16  Special maps-to operations   opeliunxp2f 6182
            2.6.17  Function transposition   ctpos 6188
            2.6.18  Undefined values   pwuninel2 6226
            2.6.19  Functions on ordinals; strictly monotone ordinal functions   iunon 6228
            2.6.20  "Strong" transfinite recursion   crecs 6248
            2.6.21  Recursive definition generator   crdg 6313
            2.6.22  Finite recursion   cfrec 6334
            2.6.23  Ordinal arithmetic   c1o 6353
            2.6.24  Natural number arithmetic   nna0 6418
            2.6.25  Equivalence relations and classes   wer 6474
            2.6.26  The mapping operation   cmap 6590
            2.6.27  Infinite Cartesian products   cixp 6640
            2.6.28  Equinumerosity   cen 6680
            2.6.29  Equinumerosity (cont.)   xpf1o 6786
            2.6.30  Pigeonhole Principle   phplem1 6794
            2.6.31  Finite sets   fict 6810
            2.6.32  Schroeder-Bernstein Theorem   sbthlem1 6898
            2.6.33  Finite intersections   cfi 6909
            2.6.34  Supremum and infimum   csup 6922
            2.6.35  Ordinal isomorphism   ordiso2 6973
            2.6.36  Disjoint union   cdju 6975
                  2.6.36.1  Disjoint union   cdju 6975
                  ​*2.6.36.2  Left and right injections of a disjoint union   cinl 6983
                  2.6.36.3  Universal property of the disjoint union   djuss 7008
                  2.6.36.4  Dominance and equinumerosity properties of disjoint union   djudom 7031
                  2.6.36.5  Older definition temporarily kept for comparison, to be deleted   cdjud 7040
                  2.6.36.6  Countable sets   0ct 7045
            ​*2.6.37  The one-point compactification of the natural numbers   xnninf 7057
            2.6.38  Omniscient sets   comni 7071
            2.6.39  Markov's principle   cmarkov 7088
            2.6.40  Weakly omniscient sets   cwomni 7100
            2.6.41  Cardinal numbers   ccrd 7108
            2.6.42  Axiom of Choice equivalents   wac 7134
            2.6.43  Cardinal number arithmetic   endjudisj 7139
            2.6.44  Ordinal trichotomy   exmidontriimlem1 7150
            2.6.45  Excluded middle and the power set of a singleton   pw1on 7155
​​*PART 3  CHOICE PRINCIPLES
      ​3.1  Countable Choice and Dependent Choice
            3.1.1  Introduce Countable Choice   wacc 7176
​​*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 7186
            4.1.2  Final derivation of real and complex number postulates   axcnex 7773
            4.1.3  Real and complex number postulates restated as axioms   ax-cnex 7817
      ​4.2  Derive the basic properties from the field axioms
            4.2.1  Some deductions from the field axioms for complex numbers   cnex 7850
            4.2.2  Infinity and the extended real number system   cpnf 7903
            4.2.3  Restate the ordering postulates with extended real "less than"   axltirr 7938
            4.2.4  Ordering on reals   lttr 7945
            4.2.5  Initial properties of the complex numbers   mul12 7998
      ​4.3  Real and complex numbers - basic operations
            4.3.1  Addition   add12 8027
            4.3.2  Subtraction   cmin 8040
            4.3.3  Multiplication   kcnktkm1cn 8252
            4.3.4  Ordering on reals (cont.)   ltadd2 8288
            4.3.5  Real Apartness   creap 8443
            4.3.6  Complex Apartness   cap 8450
            4.3.7  Reciprocals   recextlem1 8519
            4.3.8  Division   cdiv 8539
            4.3.9  Ordering on reals (cont.)   ltp1 8709
            4.3.10  Suprema   lbreu 8810
            4.3.11  Imaginary and complex number properties   crap0 8823
      ​4.4  Integer sets
            4.4.1  Positive integers (as a subset of complex numbers)   cn 8827
            4.4.2  Principle of mathematical induction   nnind 8843
            ​*4.4.3  Decimal representation of numbers   c2 8878
            ​*4.4.4  Some properties of specific numbers   neg1cn 8932
            4.4.5  Simple number properties   halfcl 9053
            4.4.6  The Archimedean property   arch 9081
            4.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 9084
            ​*4.4.8  Extended nonnegative integers   cxnn0 9147
            4.4.9  Integers (as a subset of complex numbers)   cz 9161
            4.4.10  Decimal arithmetic   cdc 9289
            4.4.11  Upper sets of integers   cuz 9433
            4.4.12  Rational numbers (as a subset of complex numbers)   cq 9521
            4.4.13  Complex numbers as pairs of reals   cnref1o 9552
      ​4.5  Order sets
            4.5.1  Positive reals (as a subset of complex numbers)   crp 9553
            4.5.2  Infinity and the extended real number system (cont.)   cxne 9669
            4.5.3  Real number intervals   cioo 9785
            4.5.4  Finite intervals of integers   cfz 9905
            ​*4.5.5  Finite intervals of nonnegative integers   elfz2nn0 10007
            4.5.6  Half-open integer ranges   cfzo 10034
            4.5.7  Rational numbers (cont.)   qtri3or 10135
      ​4.6  Elementary integer functions
            4.6.1  The floor and ceiling functions   cfl 10160
            4.6.2  The modulo (remainder) operation   cmo 10214
            4.6.3  Miscellaneous theorems about integers   frec2uz0d 10291
            4.6.4  Strong induction over upper sets of integers   uzsinds 10334
            4.6.5  The infinite sequence builder "seq"   cseq 10337
            4.6.6  Integer powers   cexp 10411
            4.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 10586
            4.6.8  Factorial function   cfa 10592
            4.6.9  The binomial coefficient operation   cbc 10614
            4.6.10  The ` # ` (set size) function   chash 10642
      ​4.7  Elementary real and complex functions
            4.7.1  The "shift" operation   cshi 10707
            4.7.2  Real and imaginary parts; conjugate   ccj 10732
            4.7.3  Sequence convergence   caucvgrelemrec 10872
            4.7.4  Square root; absolute value   csqrt 10889
            4.7.5  The maximum of two real numbers   maxcom 11096
            4.7.6  The minimum of two real numbers   mincom 11121
            4.7.7  The maximum of two extended reals   xrmaxleim 11134
            4.7.8  The minimum of two extended reals   xrnegiso 11152
      ​4.8  Elementary limits and convergence
            4.8.1  Limits   cli 11168
            4.8.2  Finite and infinite sums   csu 11243
            4.8.3  The binomial theorem   binomlem 11373
            4.8.4  Infinite sums (cont.)   isumshft 11380
            4.8.5  Miscellaneous converging and diverging sequences   divcnv 11387
            4.8.6  Arithmetic series   arisum 11388
            4.8.7  Geometric series   expcnvap0 11392
            4.8.8  Ratio test for infinite series convergence   cvgratnnlembern 11413
            4.8.9  Mertens' theorem   mertenslemub 11424
            4.8.10  Finite and infinite products   prodf 11428
                  4.8.10.1  Product sequences   prodf 11428
                  4.8.10.2  Non-trivial convergence   ntrivcvgap 11438
                  4.8.10.3  Complex products   cprod 11440
                  4.8.10.4  Finite products   fprodseq 11473
      ​4.9  Elementary trigonometry
            4.9.1  The exponential, sine, and cosine functions   ce 11532
                  4.9.1.1  The circle constant (tau = 2 pi)   ctau 11664
            4.9.2  _e is irrational   eirraplem 11666
​​*PART 5  ELEMENTARY NUMBER THEORY
      ​5.1  Elementary properties of divisibility
            5.1.1  The divides relation   cdvds 11676
            ​*5.1.2  Even and odd numbers   evenelz 11750
            5.1.3  The division algorithm   divalglemnn 11801
            5.1.4  The greatest common divisor operator   cgcd 11821
            5.1.5  Bézout's identity   bezoutlemnewy 11871
            5.1.6  Algorithms   nn0seqcvgd 11909
            5.1.7  Euclid's Algorithm   eucalgval2 11921
            ​*5.1.8  The least common multiple   clcm 11928
            ​*5.1.9  Coprimality and Euclid's lemma   coprmgcdb 11956
            5.1.10  Cancellability of congruences   congr 11968
      ​5.2  Elementary prime number theory
            ​*5.2.1  Elementary properties   cprime 11975
            ​*5.2.2  Coprimality and Euclid's lemma (cont.)   coprm 12009
            5.2.3  Non-rationality of square root of 2   sqrt2irrlem 12026
            5.2.4  Properties of the canonical representation of a rational   cnumer 12046
            5.2.5  Euler's theorem   cphi 12073
      ​5.3  Cardinality of real and complex number subsets
            5.3.1  Countability of integers and rationals   oddennn 12104
​PART 6  BASIC STRUCTURES
      ​6.1  Extensible structures
            ​*6.1.1  Basic definitions   cstr 12157
            6.1.2  Slot definitions   cplusg 12223
            6.1.3  Definition of the structure product   crest 12322
      ​6.2  The complex numbers as an algebraic extensible structure
            6.2.1  Definition and basic properties   cpsmet 12350
​PART 7  BASIC TOPOLOGY
      ​7.1  Topology
            ​*7.1.1  Topological spaces   ctop 12366
                  7.1.1.1  Topologies   ctop 12366
                  7.1.1.2  Topologies on sets   ctopon 12379
                  7.1.1.3  Topological spaces   ctps 12399
            7.1.2  Topological bases   ctb 12411
            7.1.3  Examples of topologies   distop 12456
            7.1.4  Closure and interior   ccld 12463
            7.1.5  Neighborhoods   cnei 12509
            7.1.6  Subspace topologies   restrcl 12538
            7.1.7  Limits and continuity in topological spaces   ccn 12556
            7.1.8  Product topologies   ctx 12623
            7.1.9  Continuous function-builders   cnmptid 12652
            7.1.10  Homeomorphisms   chmeo 12671
      ​7.2  Metric spaces
            7.2.1  Pseudometric spaces   psmetrel 12693
            7.2.2  Basic metric space properties   cxms 12707
            7.2.3  Metric space balls   blfvalps 12756
            7.2.4  Open sets of a metric space   mopnrel 12812
            7.2.5  Continuity in metric spaces   metcnp3 12882
            7.2.6  Topology on the reals   qtopbasss 12892
            7.2.7  Topological definitions using the reals   ccncf 12928
​PART 8  BASIC REAL AND COMPLEX ANALYSIS
            8.0.1  Dedekind cuts   dedekindeulemuub 12966
            8.0.2  Intermediate value theorem   ivthinclemlm 12983
      ​8.1  Derivatives
            8.1.1  Real and complex differentiation   climc 12994
                  8.1.1.1  Derivatives of functions of one complex or real variable   climc 12994
​PART 9  BASIC REAL AND COMPLEX FUNCTIONS
      ​9.1  Basic trigonometry
            9.1.1  The exponential, sine, and cosine functions (cont.)   efcn 13060
            9.1.2  Properties of pi = 3.14159...   pilem1 13071
            9.1.3  The natural logarithm on complex numbers   clog 13148
            ​*9.1.4  Logarithms to an arbitrary base   clogb 13231
            9.1.5  Quartic binomial expansion   binom4 13267
​PART 10  GUIDES AND MISCELLANEA
      ​10.1  Guides (conventions, explanations, and examples)
            ​*10.1.1  Conventions   conventions 13268
            10.1.2  Definitional examples   ex-or 13269
​PART 11  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​11.1  Mathboxes for user contributions
            11.1.1  Mathbox guidelines   mathbox 13279
      ​11.2  Mathbox for BJ
            11.2.1  Propositional calculus   bj-nnsn 13280
                  ​*11.2.1.1  Stable formulas   bj-trst 13285
                  11.2.1.2  Decidable formulas   bj-trdc 13295
            11.2.2  Predicate calculus   bj-ex 13307
            11.2.3  Set theorey miscellaneous   bj-el2oss1o 13319
            ​*11.2.4  Extensionality   bj-vtoclgft 13320
            ​*11.2.5  Decidability of classes   wdcin 13338
            11.2.6  Disjoint union   djucllem 13345
            11.2.7  Miscellaneous   2ssom 13348
            ​*11.2.8  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 13358
                  *11.2.8.1  Bounded formulas   wbd 13358
                  ​*11.2.8.2  Bounded classes   wbdc 13386
            ​*11.2.9  CZF: Bounded separation   ax-bdsep 13430
                  11.2.9.1  Delta_0-classical logic   ax-bj-d0cl 13470
                  11.2.9.2  Inductive classes and the class of natural number ordinals   wind 13472
                  ​*11.2.9.3  The first three Peano postulates   bj-peano2 13485
            ​*11.2.10  CZF: Infinity   ax-infvn 13487
                  *11.2.10.1  The set of natural number ordinals   ax-infvn 13487
                  ​*11.2.10.2  Peano's fifth postulate   bdpeano5 13489
                  ​*11.2.10.3  Bounded induction and Peano's fourth postulate   findset 13491
            ​*11.2.11  CZF: Set induction   setindft 13511
                  *11.2.11.1  Set induction   setindft 13511
                  ​*11.2.11.2  Full induction   bj-findis 13525
            ​*11.2.12  CZF: Strong collection   ax-strcoll 13528
            ​*11.2.13  CZF: Subset collection   ax-sscoll 13533
            11.2.14  Real numbers   ax-ddkcomp 13535
      ​11.3  Mathbox for Jim Kingdon
            11.3.1  Natural numbers   ss1oel2o 13536
            11.3.2  The power set of a singleton   pwtrufal 13540
            11.3.3  Omniscience of NN+oo   0nninf 13547
            11.3.4  Schroeder-Bernstein Theorem   exmidsbthrlem 13564
            11.3.5  Real and complex numbers   qdencn 13569
            ​*11.3.6  Analytic omniscience principles   trilpolemclim 13578
            11.3.7  Supremum and infimum   supfz 13610
            11.3.8  Circle constant   taupi 13612
      ​11.4  Mathbox for Mykola Mostovenko
      ​11.5  Mathbox for David A. Wheeler
            11.5.1  Testable propositions   dftest 13614
            ​*11.5.2  Allsome quantifier   walsi 13615