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
PART 7  BASIC ALGEBRAIC STRUCTURES
      7.1  Monoids
      7.2  Groups
      7.3  Rings
      7.4  Division rings and fields
      7.5  Left modules
      7.6  Subring algebras and ideals
      7.7  The complex numbers as an algebraic extensible structure
PART 8  BASIC TOPOLOGY
      8.1  Topology
      8.2  Metric spaces
PART 9  BASIC REAL AND COMPLEX ANALYSIS
      9.1  Derivatives
PART 10  BASIC REAL AND COMPLEX FUNCTIONS
      10.1  Basic trigonometry
      10.2  Basic number theory
PART 11  GUIDES AND MISCELLANEA
      11.1  Guides (conventions, explanations, and examples)
PART 12  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​12.1  Mathboxes for user contributions
      12.2  Mathbox for BJ
      12.3  Mathbox for Jim Kingdon
      12.4  Mathbox for Mykola Mostovenko
      12.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 104
            1.2.5  Logical negation (intuitionistic)   ax-in1 615
            1.2.6  Logical disjunction   wo 709
            1.2.7  Stable propositions   wstab 831
            1.2.8  Decidable propositions   wdc 835
            ​*1.2.9  Theorems of decidable propositions   const 853
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 917
            1.2.11  Abbreviated conjunction and disjunction of three wff's   w3o 979
            1.2.12  True and false constants   wal 1362
                  ​*1.2.12.1  Universal quantifier for use by df-tru   wal 1362
                  ​*1.2.12.2  Equality predicate for use by df-tru   cv 1363
                  1.2.12.3  Define the true and false constants   wtru 1365
            1.2.13  Logical 'xor'   wxo 1386
            ​*1.2.14  Truth tables: Operations on true and false constants   truantru 1412
            ​*1.2.15  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1434
            1.2.16  Logical implication (continued)   syl6an 1445
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1458
            ​*1.3.2  Equality predicate (continued)   weq 1514
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1537
            1.3.4  Introduce Axiom of Existence   ax-i9 1541
            1.3.5  Additional intuitionistic axioms   ax-ial 1545
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1547
            1.3.7  The existential quantifier   19.8a 1601
            1.3.8  Equality theorems without distinct variables   a9e 1707
            1.3.9  Axioms ax-10 and ax-11   ax10o 1726
            1.3.10  Substitution (without distinct variables)   wsb 1773
            1.3.11  Theorems using axiom ax-11   equs5a 1805
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1822
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1833
            1.4.3  More theorems related to ax-11 and substitution   albidv 1835
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1869
            1.4.5  More substitution theorems   hbs1 1950
            1.4.6  Existential uniqueness   weu 2038
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2136
      ​​*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 2171
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2175
                  2.1.2.1  Elementary properties of class abstractions   eqabdv 2318
            2.1.3  Class form not-free predicate   wnfc 2319
            2.1.4  Negated equality and membership   wne 2360
                  2.1.4.1  Negated equality   wne 2360
                  2.1.4.2  Negated membership   wnel 2455
            2.1.5  Restricted quantification   wral 2468
            2.1.6  The universal class   cvv 2752
            ​*2.1.7  Conditional equality (experimental)   wcdeq 2960
            2.1.8  Russell's Paradox   ru 2976
            2.1.9  Proper substitution of classes for sets   wsbc 2977
            2.1.10  Proper substitution of classes for sets into classes   csb 3072
            2.1.11  Define basic set operations and relations   cdif 3141
            2.1.12  Subclasses and subsets   df-ss 3157
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3260
                  2.1.13.1  The difference of two classes   dfdif3 3260
                  2.1.13.2  The union of two classes   elun 3291
                  2.1.13.3  The intersection of two classes   elin 3333
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3381
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3416
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3430
            2.1.14  The empty set   c0 3437
            2.1.15  Conditional operator   cif 3549
            2.1.16  Power classes   cpw 3590
            2.1.17  Unordered and ordered pairs   csn 3607
            2.1.18  The union of a class   cuni 3824
            2.1.19  The intersection of a class   cint 3859
            2.1.20  Indexed union and intersection   ciun 3901
            2.1.21  Disjointness   wdisj 3995
            2.1.22  Binary relations   wbr 4018
            2.1.23  Ordered-pair class abstractions (class builders)   copab 4078
            2.1.24  Transitive classes   wtr 4116
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4133
            2.2.2  Introduce the Axiom of Separation   ax-sep 4136
            2.2.3  Derive the Null Set Axiom   zfnuleu 4142
            2.2.4  Theorems requiring subset and intersection existence   nalset 4148
            2.2.5  Theorems requiring empty set existence   class2seteq 4178
            2.2.6  Collection principle   bnd 4187
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4189
            2.3.2  A notation for excluded middle   wem 4209
            2.3.3  Axiom of Pairing   ax-pr 4224
            2.3.4  Ordered pair theorem   opm 4249
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4272
            2.3.6  Power class of union and intersection   pwin 4297
            2.3.7  Epsilon and identity relations   cep 4302
            ​*2.3.8  Partial and total orderings   wpo 4309
            2.3.9  Founded and set-like relations   wfrfor 4342
            2.3.10  Ordinals   word 4377
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4448
            2.4.2  Ordinals (continued)   ordon 4500
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4546
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4551
            2.5.3  Transfinite induction   tfi 4596
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4602
            2.6.2  The natural numbers   com 4604
            2.6.3  Peano's postulates   peano1 4608
            2.6.4  Finite induction (for finite ordinals)   find 4613
            2.6.5  The Natural Numbers (continued)   nn0suc 4618
            2.6.6  Relations   cxp 4639
            2.6.7  Definite description binder (inverted iota)   cio 5191
            2.6.8  Functions   wfun 5226
            2.6.9  Cantor's Theorem   canth 5846
            2.6.10  Restricted iota (description binder)   crio 5847
            2.6.11  Operations   co 5892
            2.6.12  Maps-to notation   elmpocl 6087
            2.6.13  Function operation   cof 6100
            2.6.14  Functions (continued)   resfunexgALT 6128
            2.6.15  First and second members of an ordered pair   c1st 6158
            ​*2.6.16  Special maps-to operations   opeliunxp2f 6258
            2.6.17  Function transposition   ctpos 6264
            2.6.18  Undefined values   pwuninel2 6302
            2.6.19  Functions on ordinals; strictly monotone ordinal functions   iunon 6304
            2.6.20  "Strong" transfinite recursion   crecs 6324
            2.6.21  Recursive definition generator   crdg 6389
            2.6.22  Finite recursion   cfrec 6410
            2.6.23  Ordinal arithmetic   c1o 6429
            2.6.24  Natural number arithmetic   nna0 6494
            2.6.25  Equivalence relations and classes   wer 6551
            2.6.26  The mapping operation   cmap 6667
            2.6.27  Infinite Cartesian products   cixp 6717
            2.6.28  Equinumerosity   cen 6757
            2.6.29  Equinumerosity (cont.)   xpf1o 6863
            2.6.30  Pigeonhole Principle   phplem1 6871
            2.6.31  Finite sets   fict 6887
            2.6.32  Schroeder-Bernstein Theorem   sbthlem1 6976
            2.6.33  Finite intersections   cfi 6987
            2.6.34  Supremum and infimum   csup 7001
            2.6.35  Ordinal isomorphism   ordiso2 7054
            2.6.36  Disjoint union   cdju 7056
                  2.6.36.1  Disjoint union   cdju 7056
                  ​*2.6.36.2  Left and right injections of a disjoint union   cinl 7064
                  2.6.36.3  Universal property of the disjoint union   djuss 7089
                  2.6.36.4  Dominance and equinumerosity properties of disjoint union   djudom 7112
                  2.6.36.5  Older definition temporarily kept for comparison, to be deleted   cdjud 7121
                  2.6.36.6  Countable sets   0ct 7126
            ​*2.6.37  The one-point compactification of the natural numbers   xnninf 7138
            2.6.38  Omniscient sets   comni 7152
            2.6.39  Markov's principle   cmarkov 7169
            2.6.40  Weakly omniscient sets   cwomni 7181
            2.6.41  Cardinal numbers   ccrd 7198
            2.6.42  Axiom of Choice equivalents   wac 7224
            2.6.43  Cardinal number arithmetic   endjudisj 7229
            2.6.44  Ordinal trichotomy   exmidontriimlem1 7240
            2.6.45  Excluded middle and the power set of a singleton   pw1on 7245
            2.6.46  Apartness relations   wap 7266
​​*PART 3  CHOICE PRINCIPLES
      ​3.1  Countable Choice and Dependent Choice
            3.1.1  Introduce Countable Choice   wacc 7281
​​*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 7291
            4.1.2  Final derivation of real and complex number postulates   axcnex 7878
            4.1.3  Real and complex number postulates restated as axioms   ax-cnex 7922
      ​4.2  Derive the basic properties from the field axioms
            4.2.1  Some deductions from the field axioms for complex numbers   cnex 7955
            4.2.2  Infinity and the extended real number system   cpnf 8009
            4.2.3  Restate the ordering postulates with extended real "less than"   axltirr 8044
            4.2.4  Ordering on reals   lttr 8051
            4.2.5  Initial properties of the complex numbers   mul12 8106
      ​4.3  Real and complex numbers - basic operations
            4.3.1  Addition   add12 8135
            4.3.2  Subtraction   cmin 8148
            4.3.3  Multiplication   kcnktkm1cn 8360
            4.3.4  Ordering on reals (cont.)   ltadd2 8396
            4.3.5  Real Apartness   creap 8551
            4.3.6  Complex Apartness   cap 8558
            4.3.7  Reciprocals   recextlem1 8628
            4.3.8  Division   cdiv 8649
            4.3.9  Ordering on reals (cont.)   ltp1 8821
            4.3.10  Suprema   lbreu 8922
            4.3.11  Imaginary and complex number properties   crap0 8935
      ​4.4  Integer sets
            4.4.1  Positive integers (as a subset of complex numbers)   cn 8939
            4.4.2  Principle of mathematical induction   nnind 8955
            ​*4.4.3  Decimal representation of numbers   c2 8990
            ​*4.4.4  Some properties of specific numbers   neg1cn 9044
            4.4.5  Simple number properties   halfcl 9165
            4.4.6  The Archimedean property   arch 9193
            4.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 9196
            ​*4.4.8  Extended nonnegative integers   cxnn0 9259
            4.4.9  Integers (as a subset of complex numbers)   cz 9273
            4.4.10  Decimal arithmetic   cdc 9404
            4.4.11  Upper sets of integers   cuz 9548
            4.4.12  Rational numbers (as a subset of complex numbers)   cq 9639
            4.4.13  Complex numbers as pairs of reals   cnref1o 9670
      ​4.5  Order sets
            4.5.1  Positive reals (as a subset of complex numbers)   crp 9673
            4.5.2  Infinity and the extended real number system (cont.)   cxne 9789
            4.5.3  Real number intervals   cioo 9908
            4.5.4  Finite intervals of integers   cfz 10028
            ​*4.5.5  Finite intervals of nonnegative integers   elfz2nn0 10132
            4.5.6  Half-open integer ranges   cfzo 10162
            4.5.7  Rational numbers (cont.)   qtri3or 10263
      ​4.6  Elementary integer functions
            4.6.1  The floor and ceiling functions   cfl 10288
            4.6.2  The modulo (remainder) operation   cmo 10342
            4.6.3  Miscellaneous theorems about integers   frec2uz0d 10419
            4.6.4  Strong induction over upper sets of integers   uzsinds 10462
            4.6.5  The infinite sequence builder "seq"   cseq 10465
            4.6.6  Integer powers   cexp 10539
            4.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 10719
            4.6.8  Factorial function   cfa 10725
            4.6.9  The binomial coefficient operation   cbc 10747
            4.6.10  The ` # ` (set size) function   chash 10775
      ​4.7  Elementary real and complex functions
            4.7.1  The "shift" operation   cshi 10843
            4.7.2  Real and imaginary parts; conjugate   ccj 10868
            4.7.3  Sequence convergence   caucvgrelemrec 11008
            4.7.4  Square root; absolute value   csqrt 11025
            4.7.5  The maximum of two real numbers   maxcom 11232
            4.7.6  The minimum of two real numbers   mincom 11257
            4.7.7  The maximum of two extended reals   xrmaxleim 11272
            4.7.8  The minimum of two extended reals   xrnegiso 11290
      ​4.8  Elementary limits and convergence
            4.8.1  Limits   cli 11306
            4.8.2  Finite and infinite sums   csu 11381
            4.8.3  The binomial theorem   binomlem 11511
            4.8.4  Infinite sums (cont.)   isumshft 11518
            4.8.5  Miscellaneous converging and diverging sequences   divcnv 11525
            4.8.6  Arithmetic series   arisum 11526
            4.8.7  Geometric series   expcnvap0 11530
            4.8.8  Ratio test for infinite series convergence   cvgratnnlembern 11551
            4.8.9  Mertens' theorem   mertenslemub 11562
            4.8.10  Finite and infinite products   prodf 11566
                  4.8.10.1  Product sequences   prodf 11566
                  4.8.10.2  Non-trivial convergence   ntrivcvgap 11576
                  4.8.10.3  Complex products   cprod 11578
                  4.8.10.4  Finite products   fprodseq 11611
      ​4.9  Elementary trigonometry
            4.9.1  The exponential, sine, and cosine functions   ce 11670
                  4.9.1.1  The circle constant (tau = 2 pi)   ctau 11802
            4.9.2  _e is irrational   eirraplem 11804
​​*PART 5  ELEMENTARY NUMBER THEORY
      ​5.1  Elementary properties of divisibility
            5.1.1  The divides relation   cdvds 11814
            ​*5.1.2  Even and odd numbers   evenelz 11892
            5.1.3  The division algorithm   divalglemnn 11943
            5.1.4  The greatest common divisor operator   cgcd 11963
            5.1.5  Bézout's identity   bezoutlemnewy 12017
            5.1.6  Decidable sets of integers   nnmindc 12055
            5.1.7  Algorithms   nn0seqcvgd 12061
            5.1.8  Euclid's Algorithm   eucalgval2 12073
            ​*5.1.9  The least common multiple   clcm 12080
            ​*5.1.10  Coprimality and Euclid's lemma   coprmgcdb 12108
            5.1.11  Cancellability of congruences   congr 12120
      ​5.2  Elementary prime number theory
            ​*5.2.1  Elementary properties   cprime 12127
            ​*5.2.2  Coprimality and Euclid's lemma (cont.)   coprm 12164
            5.2.3  Non-rationality of square root of 2   sqrt2irrlem 12181
            5.2.4  Properties of the canonical representation of a rational   cnumer 12201
            5.2.5  Euler's theorem   codz 12228
            5.2.6  Arithmetic modulo a prime number   modprm1div 12267
            5.2.7  Pythagorean Triples   coprimeprodsq 12277
            5.2.8  The prime count function   cpc 12304
            5.2.9  Pocklington's theorem   prmpwdvds 12373
            5.2.10  Infinite primes theorem   infpnlem1 12377
            5.2.11  Fundamental theorem of arithmetic   1arithlem1 12381
            5.2.12  Lagrange's four-square theorem   cgz 12387
      ​5.3  Cardinality of real and complex number subsets
            5.3.1  Countability of integers and rationals   oddennn 12418
​PART 6  BASIC STRUCTURES
      ​6.1  Extensible structures
            ​*6.1.1  Basic definitions   cstr 12483
            6.1.2  Slot definitions   cplusg 12562
            6.1.3  Definition of the structure product   crest 12717
            6.1.4  Definition of the structure quotient   cimas 12749
​PART 7  BASIC ALGEBRAIC STRUCTURES
      ​7.1  Monoids
            ​*7.1.1  Magmas   cplusf 12802
            ​*7.1.2  Identity elements   mgmidmo 12821
            ​*7.1.3  Semigroups   csgrp 12837
            ​*7.1.4  Definition and basic properties of monoids   cmnd 12850
            7.1.5  Monoid homomorphisms and submonoids   cmhm 12882
      ​7.2  Groups
            7.2.1  Definition and basic properties   cgrp 12918
            ​*7.2.2  Group multiple operation   cmg 13034
            7.2.3  Subgroups and Quotient groups   csubg 13079
            7.2.4  Elementary theory of group homomorphisms   cghm 13147
            7.2.5  Abelian groups   ccmn 13191
                  7.2.5.1  Definition and basic properties   ccmn 13191
      ​7.3  Rings
            7.3.1  Multiplicative Group   cmgp 13242
            ​*7.3.2  Non-unital rings ("rngs")   crng 13254
            ​*7.3.3  Ring unity (multiplicative identity)   cur 13281
            7.3.4  Semirings   csrg 13285
            7.3.5  Definition and basic properties of unital rings   crg 13318
            7.3.6  Opposite ring   coppr 13385
            7.3.7  Divisibility   cdsr 13404
            7.3.8  Ring homomorphisms   crh 13468
            7.3.9  Nonzero rings and zero rings   cnzr 13497
            7.3.10  Local rings   clring 13505
            7.3.11  Subrings   csubrng 13512
                  7.3.11.1  Subrings of non-unital rings   csubrng 13512
                  7.3.11.2  Subrings of unital rings   csubrg 13532
      ​7.4  Division rings and fields
            7.4.1  Ring apartness   capr 13564
      ​7.5  Left modules
            7.5.1  Definition and basic properties   clmod 13571
            7.5.2  Subspaces and spans in a left module   clss 13636
      ​7.6  Subring algebras and ideals
            7.6.1  Subring algebras   csra 13717
            7.6.2  Ideals and spans   clidl 13751
            7.6.3  Two-sided ideals and quotient rings   c2idl 13783
      ​7.7  The complex numbers as an algebraic extensible structure
            7.7.1  Definition and basic properties   cpsmet 13816
            ​*7.7.2  Ring of integers   czring 13857
            7.7.3  Algebraic constructions based on the complex numbers   czrh 13877
​PART 8  BASIC TOPOLOGY
      ​8.1  Topology
            ​*8.1.1  Topological spaces   ctop 13901
                  8.1.1.1  Topologies   ctop 13901
                  8.1.1.2  Topologies on sets   ctopon 13914
                  8.1.1.3  Topological spaces   ctps 13934
            8.1.2  Topological bases   ctb 13946
            8.1.3  Examples of topologies   distop 13989
            8.1.4  Closure and interior   ccld 13996
            8.1.5  Neighborhoods   cnei 14042
            8.1.6  Subspace topologies   restrcl 14071
            8.1.7  Limits and continuity in topological spaces   ccn 14089
            8.1.8  Product topologies   ctx 14156
            8.1.9  Continuous function-builders   cnmptid 14185
            8.1.10  Homeomorphisms   chmeo 14204
      ​8.2  Metric spaces
            8.2.1  Pseudometric spaces   psmetrel 14226
            8.2.2  Basic metric space properties   cxms 14240
            8.2.3  Metric space balls   blfvalps 14289
            8.2.4  Open sets of a metric space   mopnrel 14345
            8.2.5  Continuity in metric spaces   metcnp3 14415
            8.2.6  Topology on the reals   qtopbasss 14425
            8.2.7  Topological definitions using the reals   ccncf 14461
​PART 9  BASIC REAL AND COMPLEX ANALYSIS
            9.0.1  Dedekind cuts   dedekindeulemuub 14499
            9.0.2  Intermediate value theorem   ivthinclemlm 14516
      ​9.1  Derivatives
            9.1.1  Real and complex differentiation   climc 14527
                  9.1.1.1  Derivatives of functions of one complex or real variable   climc 14527
​PART 10  BASIC REAL AND COMPLEX FUNCTIONS
      ​10.1  Basic trigonometry
            10.1.1  The exponential, sine, and cosine functions (cont.)   efcn 14593
            10.1.2  Properties of pi = 3.14159...   pilem1 14604
            10.1.3  The natural logarithm on complex numbers   clog 14681
            ​*10.1.4  Logarithms to an arbitrary base   clogb 14765
            10.1.5  Quartic binomial expansion   binom4 14801
      ​10.2  Basic number theory
            ​*10.2.1  Quadratic residues and the Legendre symbol   clgs 14802
            10.2.2  Quadratic reciprocity   lgseisenlem1 14854
            10.2.3  All primes 4n+1 are the sum of two squares   2sqlem1 14865
​PART 11  GUIDES AND MISCELLANEA
      ​11.1  Guides (conventions, explanations, and examples)
            ​*11.1.1  Conventions   conventions 14877
            11.1.2  Definitional examples   ex-or 14878
​PART 12  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​12.1  Mathboxes for user contributions
            12.1.1  Mathbox guidelines   mathbox 14888
      ​12.2  Mathbox for BJ
            12.2.1  Propositional calculus   bj-nnsn 14889
                  ​*12.2.1.1  Stable formulas   bj-trst 14895
                  12.2.1.2  Decidable formulas   bj-trdc 14908
            12.2.2  Predicate calculus   bj-ex 14918
            12.2.3  Set theorey miscellaneous   bj-el2oss1o 14930
            ​*12.2.4  Extensionality   bj-vtoclgft 14931
            ​*12.2.5  Decidability of classes   wdcin 14949
            12.2.6  Disjoint union   djucllem 14956
            12.2.7  Miscellaneous   funmptd 14959
            ​*12.2.8  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 14968
                  *12.2.8.1  Bounded formulas   wbd 14968
                  ​*12.2.8.2  Bounded classes   wbdc 14996
            ​*12.2.9  CZF: Bounded separation   ax-bdsep 15040
                  12.2.9.1  Delta_0-classical logic   ax-bj-d0cl 15080
                  12.2.9.2  Inductive classes and the class of natural number ordinals   wind 15082
                  ​*12.2.9.3  The first three Peano postulates   bj-peano2 15095
            ​*12.2.10  CZF: Infinity   ax-infvn 15097
                  *12.2.10.1  The set of natural number ordinals   ax-infvn 15097
                  ​*12.2.10.2  Peano's fifth postulate   bdpeano5 15099
                  ​*12.2.10.3  Bounded induction and Peano's fourth postulate   findset 15101
            ​*12.2.11  CZF: Set induction   setindft 15121
                  *12.2.11.1  Set induction   setindft 15121
                  ​*12.2.11.2  Full induction   bj-findis 15135
            ​*12.2.12  CZF: Strong collection   ax-strcoll 15138
            ​*12.2.13  CZF: Subset collection   ax-sscoll 15143
            12.2.14  Real numbers   ax-ddkcomp 15145
      ​12.3  Mathbox for Jim Kingdon
            12.3.1  Propositional and predicate logic   nnnotnotr 15146
            12.3.2  Natural numbers   1dom1el 15147
            12.3.3  The power set of a singleton   pwtrufal 15152
            12.3.4  Omniscience of NN+oo   0nninf 15158
            12.3.5  Schroeder-Bernstein Theorem   exmidsbthrlem 15175
            12.3.6  Real and complex numbers   qdencn 15180
            ​*12.3.7  Analytic omniscience principles   trilpolemclim 15189
            12.3.8  Supremum and infimum   supfz 15224
            12.3.9  Circle constant   taupi 15226
      ​12.4  Mathbox for Mykola Mostovenko
      ​12.5  Mathbox for David A. Wheeler
            12.5.1  Testable propositions   dftest 15228
            ​*12.5.2  Allsome quantifier   walsi 15229