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  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 614
            1.2.6  Logical disjunction   wo 708
            1.2.7  Stable propositions   wstab 830
            1.2.8  Decidable propositions   wdc 834
            ​*1.2.9  Theorems of decidable propositions   const 852
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 916
            1.2.11  Abbreviated conjunction and disjunction of three wff's   w3o 977
            1.2.12  True and false constants   wal 1351
                  ​*1.2.12.1  Universal quantifier for use by df-tru   wal 1351
                  ​*1.2.12.2  Equality predicate for use by df-tru   cv 1352
                  1.2.12.3  Define the true and false constants   wtru 1354
            1.2.13  Logical 'xor'   wxo 1375
            ​*1.2.14  Truth tables: Operations on true and false constants   truantru 1401
            ​*1.2.15  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1423
            1.2.16  Logical implication (continued)   syl6an 1434
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1447
            ​*1.3.2  Equality predicate (continued)   weq 1503
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1526
            1.3.4  Introduce Axiom of Existence   ax-i9 1530
            1.3.5  Additional intuitionistic axioms   ax-ial 1534
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1536
            1.3.7  The existential quantifier   19.8a 1590
            1.3.8  Equality theorems without distinct variables   a9e 1696
            1.3.9  Axioms ax-10 and ax-11   ax10o 1715
            1.3.10  Substitution (without distinct variables)   wsb 1762
            1.3.11  Theorems using axiom ax-11   equs5a 1794
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1811
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1822
            1.4.3  More theorems related to ax-11 and substitution   albidv 1824
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1858
            1.4.5  More substitution theorems   hbs1 1938
            1.4.6  Existential uniqueness   weu 2026
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2124
      ​​*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 2159
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2163
            2.1.3  Class form not-free predicate   wnfc 2306
            2.1.4  Negated equality and membership   wne 2347
                  2.1.4.1  Negated equality   wne 2347
                  2.1.4.2  Negated membership   wnel 2442
            2.1.5  Restricted quantification   wral 2455
            2.1.6  The universal class   cvv 2737
            ​*2.1.7  Conditional equality (experimental)   wcdeq 2945
            2.1.8  Russell's Paradox   ru 2961
            2.1.9  Proper substitution of classes for sets   wsbc 2962
            2.1.10  Proper substitution of classes for sets into classes   csb 3057
            2.1.11  Define basic set operations and relations   cdif 3126
            2.1.12  Subclasses and subsets   df-ss 3142
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3245
                  2.1.13.1  The difference of two classes   dfdif3 3245
                  2.1.13.2  The union of two classes   elun 3276
                  2.1.13.3  The intersection of two classes   elin 3318
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3366
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3401
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3415
            2.1.14  The empty set   c0 3422
            2.1.15  Conditional operator   cif 3534
            2.1.16  Power classes   cpw 3575
            2.1.17  Unordered and ordered pairs   csn 3592
            2.1.18  The union of a class   cuni 3809
            2.1.19  The intersection of a class   cint 3844
            2.1.20  Indexed union and intersection   ciun 3886
            2.1.21  Disjointness   wdisj 3980
            2.1.22  Binary relations   wbr 4003
            2.1.23  Ordered-pair class abstractions (class builders)   copab 4063
            2.1.24  Transitive classes   wtr 4101
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4118
            2.2.2  Introduce the Axiom of Separation   ax-sep 4121
            2.2.3  Derive the Null Set Axiom   zfnuleu 4127
            2.2.4  Theorems requiring subset and intersection existence   nalset 4133
            2.2.5  Theorems requiring empty set existence   class2seteq 4163
            2.2.6  Collection principle   bnd 4172
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4174
            2.3.2  A notation for excluded middle   wem 4194
            2.3.3  Axiom of Pairing   ax-pr 4209
            2.3.4  Ordered pair theorem   opm 4234
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4257
            2.3.6  Power class of union and intersection   pwin 4282
            2.3.7  Epsilon and identity relations   cep 4287
            ​*2.3.8  Partial and total orderings   wpo 4294
            2.3.9  Founded and set-like relations   wfrfor 4327
            2.3.10  Ordinals   word 4362
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4433
            2.4.2  Ordinals (continued)   ordon 4485
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4531
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4536
            2.5.3  Transfinite induction   tfi 4581
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4587
            2.6.2  The natural numbers   com 4589
            2.6.3  Peano's postulates   peano1 4593
            2.6.4  Finite induction (for finite ordinals)   find 4598
            2.6.5  The Natural Numbers (continued)   nn0suc 4603
            2.6.6  Relations   cxp 4624
            2.6.7  Definite description binder (inverted iota)   cio 5176
            2.6.8  Functions   wfun 5210
            2.6.9  Cantor's Theorem   canth 5828
            2.6.10  Restricted iota (description binder)   crio 5829
            2.6.11  Operations   co 5874
            2.6.12  Maps-to notation   elmpocl 6068
            2.6.13  Function operation   cof 6080
            2.6.14  Functions (continued)   resfunexgALT 6108
            2.6.15  First and second members of an ordered pair   c1st 6138
            ​*2.6.16  Special maps-to operations   opeliunxp2f 6238
            2.6.17  Function transposition   ctpos 6244
            2.6.18  Undefined values   pwuninel2 6282
            2.6.19  Functions on ordinals; strictly monotone ordinal functions   iunon 6284
            2.6.20  "Strong" transfinite recursion   crecs 6304
            2.6.21  Recursive definition generator   crdg 6369
            2.6.22  Finite recursion   cfrec 6390
            2.6.23  Ordinal arithmetic   c1o 6409
            2.6.24  Natural number arithmetic   nna0 6474
            2.6.25  Equivalence relations and classes   wer 6531
            2.6.26  The mapping operation   cmap 6647
            2.6.27  Infinite Cartesian products   cixp 6697
            2.6.28  Equinumerosity   cen 6737
            2.6.29  Equinumerosity (cont.)   xpf1o 6843
            2.6.30  Pigeonhole Principle   phplem1 6851
            2.6.31  Finite sets   fict 6867
            2.6.32  Schroeder-Bernstein Theorem   sbthlem1 6955
            2.6.33  Finite intersections   cfi 6966
            2.6.34  Supremum and infimum   csup 6980
            2.6.35  Ordinal isomorphism   ordiso2 7033
            2.6.36  Disjoint union   cdju 7035
                  2.6.36.1  Disjoint union   cdju 7035
                  ​*2.6.36.2  Left and right injections of a disjoint union   cinl 7043
                  2.6.36.3  Universal property of the disjoint union   djuss 7068
                  2.6.36.4  Dominance and equinumerosity properties of disjoint union   djudom 7091
                  2.6.36.5  Older definition temporarily kept for comparison, to be deleted   cdjud 7100
                  2.6.36.6  Countable sets   0ct 7105
            ​*2.6.37  The one-point compactification of the natural numbers   xnninf 7117
            2.6.38  Omniscient sets   comni 7131
            2.6.39  Markov's principle   cmarkov 7148
            2.6.40  Weakly omniscient sets   cwomni 7160
            2.6.41  Cardinal numbers   ccrd 7177
            2.6.42  Axiom of Choice equivalents   wac 7203
            2.6.43  Cardinal number arithmetic   endjudisj 7208
            2.6.44  Ordinal trichotomy   exmidontriimlem1 7219
            2.6.45  Excluded middle and the power set of a singleton   pw1on 7224
            2.6.46  Apartness relations   wap 7245
​​*PART 3  CHOICE PRINCIPLES
      ​3.1  Countable Choice and Dependent Choice
            3.1.1  Introduce Countable Choice   wacc 7260
​​*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 7270
            4.1.2  Final derivation of real and complex number postulates   axcnex 7857
            4.1.3  Real and complex number postulates restated as axioms   ax-cnex 7901
      ​4.2  Derive the basic properties from the field axioms
            4.2.1  Some deductions from the field axioms for complex numbers   cnex 7934
            4.2.2  Infinity and the extended real number system   cpnf 7988
            4.2.3  Restate the ordering postulates with extended real "less than"   axltirr 8023
            4.2.4  Ordering on reals   lttr 8030
            4.2.5  Initial properties of the complex numbers   mul12 8085
      ​4.3  Real and complex numbers - basic operations
            4.3.1  Addition   add12 8114
            4.3.2  Subtraction   cmin 8127
            4.3.3  Multiplication   kcnktkm1cn 8339
            4.3.4  Ordering on reals (cont.)   ltadd2 8375
            4.3.5  Real Apartness   creap 8530
            4.3.6  Complex Apartness   cap 8537
            4.3.7  Reciprocals   recextlem1 8607
            4.3.8  Division   cdiv 8628
            4.3.9  Ordering on reals (cont.)   ltp1 8800
            4.3.10  Suprema   lbreu 8901
            4.3.11  Imaginary and complex number properties   crap0 8914
      ​4.4  Integer sets
            4.4.1  Positive integers (as a subset of complex numbers)   cn 8918
            4.4.2  Principle of mathematical induction   nnind 8934
            ​*4.4.3  Decimal representation of numbers   c2 8969
            ​*4.4.4  Some properties of specific numbers   neg1cn 9023
            4.4.5  Simple number properties   halfcl 9144
            4.4.6  The Archimedean property   arch 9172
            4.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 9175
            ​*4.4.8  Extended nonnegative integers   cxnn0 9238
            4.4.9  Integers (as a subset of complex numbers)   cz 9252
            4.4.10  Decimal arithmetic   cdc 9383
            4.4.11  Upper sets of integers   cuz 9527
            4.4.12  Rational numbers (as a subset of complex numbers)   cq 9618
            4.4.13  Complex numbers as pairs of reals   cnref1o 9649
      ​4.5  Order sets
            4.5.1  Positive reals (as a subset of complex numbers)   crp 9652
            4.5.2  Infinity and the extended real number system (cont.)   cxne 9768
            4.5.3  Real number intervals   cioo 9887
            4.5.4  Finite intervals of integers   cfz 10007
            ​*4.5.5  Finite intervals of nonnegative integers   elfz2nn0 10111
            4.5.6  Half-open integer ranges   cfzo 10141
            4.5.7  Rational numbers (cont.)   qtri3or 10242
      ​4.6  Elementary integer functions
            4.6.1  The floor and ceiling functions   cfl 10267
            4.6.2  The modulo (remainder) operation   cmo 10321
            4.6.3  Miscellaneous theorems about integers   frec2uz0d 10398
            4.6.4  Strong induction over upper sets of integers   uzsinds 10441
            4.6.5  The infinite sequence builder "seq"   cseq 10444
            4.6.6  Integer powers   cexp 10518
            4.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 10698
            4.6.8  Factorial function   cfa 10704
            4.6.9  The binomial coefficient operation   cbc 10726
            4.6.10  The ` # ` (set size) function   chash 10754
      ​4.7  Elementary real and complex functions
            4.7.1  The "shift" operation   cshi 10822
            4.7.2  Real and imaginary parts; conjugate   ccj 10847
            4.7.3  Sequence convergence   caucvgrelemrec 10987
            4.7.4  Square root; absolute value   csqrt 11004
            4.7.5  The maximum of two real numbers   maxcom 11211
            4.7.6  The minimum of two real numbers   mincom 11236
            4.7.7  The maximum of two extended reals   xrmaxleim 11251
            4.7.8  The minimum of two extended reals   xrnegiso 11269
      ​4.8  Elementary limits and convergence
            4.8.1  Limits   cli 11285
            4.8.2  Finite and infinite sums   csu 11360
            4.8.3  The binomial theorem   binomlem 11490
            4.8.4  Infinite sums (cont.)   isumshft 11497
            4.8.5  Miscellaneous converging and diverging sequences   divcnv 11504
            4.8.6  Arithmetic series   arisum 11505
            4.8.7  Geometric series   expcnvap0 11509
            4.8.8  Ratio test for infinite series convergence   cvgratnnlembern 11530
            4.8.9  Mertens' theorem   mertenslemub 11541
            4.8.10  Finite and infinite products   prodf 11545
                  4.8.10.1  Product sequences   prodf 11545
                  4.8.10.2  Non-trivial convergence   ntrivcvgap 11555
                  4.8.10.3  Complex products   cprod 11557
                  4.8.10.4  Finite products   fprodseq 11590
      ​4.9  Elementary trigonometry
            4.9.1  The exponential, sine, and cosine functions   ce 11649
                  4.9.1.1  The circle constant (tau = 2 pi)   ctau 11781
            4.9.2  _e is irrational   eirraplem 11783
​​*PART 5  ELEMENTARY NUMBER THEORY
      ​5.1  Elementary properties of divisibility
            5.1.1  The divides relation   cdvds 11793
            ​*5.1.2  Even and odd numbers   evenelz 11871
            5.1.3  The division algorithm   divalglemnn 11922
            5.1.4  The greatest common divisor operator   cgcd 11942
            5.1.5  Bézout's identity   bezoutlemnewy 11996
            5.1.6  Decidable sets of integers   nnmindc 12034
            5.1.7  Algorithms   nn0seqcvgd 12040
            5.1.8  Euclid's Algorithm   eucalgval2 12052
            ​*5.1.9  The least common multiple   clcm 12059
            ​*5.1.10  Coprimality and Euclid's lemma   coprmgcdb 12087
            5.1.11  Cancellability of congruences   congr 12099
      ​5.2  Elementary prime number theory
            ​*5.2.1  Elementary properties   cprime 12106
            ​*5.2.2  Coprimality and Euclid's lemma (cont.)   coprm 12143
            5.2.3  Non-rationality of square root of 2   sqrt2irrlem 12160
            5.2.4  Properties of the canonical representation of a rational   cnumer 12180
            5.2.5  Euler's theorem   codz 12207
            5.2.6  Arithmetic modulo a prime number   modprm1div 12246
            5.2.7  Pythagorean Triples   coprimeprodsq 12256
            5.2.8  The prime count function   cpc 12283
            5.2.9  Pocklington's theorem   prmpwdvds 12352
            5.2.10  Infinite primes theorem   infpnlem1 12356
            5.2.11  Fundamental theorem of arithmetic   1arithlem1 12360
            5.2.12  Lagrange's four-square theorem   cgz 12366
      ​5.3  Cardinality of real and complex number subsets
            5.3.1  Countability of integers and rationals   oddennn 12392
​PART 6  BASIC STRUCTURES
      ​6.1  Extensible structures
            ​*6.1.1  Basic definitions   cstr 12457
            6.1.2  Slot definitions   cplusg 12535
            6.1.3  Definition of the structure product   crest 12687
            6.1.4  Definition of the structure quotient   cimas 12719
​PART 7  BASIC ALGEBRAIC STRUCTURES
      ​7.1  Monoids
            ​*7.1.1  Magmas   cplusf 12771
            ​*7.1.2  Identity elements   mgmidmo 12790
            ​*7.1.3  Semigroups   csgrp 12806
            ​*7.1.4  Definition and basic properties of monoids   cmnd 12816
            7.1.5  Monoid homomorphisms and submonoids   cmhm 12848
      ​7.2  Groups
            7.2.1  Definition and basic properties   cgrp 12876
            ​*7.2.2  Group multiple operation   cmg 12982
            7.2.3  Subgroups and Quotient groups   csubg 13025
            7.2.4  Abelian groups   ccmn 13086
                  7.2.4.1  Definition and basic properties   ccmn 13086
      ​7.3  Rings
            7.3.1  Multiplicative Group   cmgp 13128
            ​*7.3.2  Ring unity (multiplicative identity)   cur 13140
            7.3.3  Semirings   csrg 13144
            7.3.4  Definition and basic properties of unital rings   crg 13177
            7.3.5  Opposite ring   coppr 13237
            7.3.6  Divisibility   cdsr 13253
            7.3.7  Ring homomorphisms   crh 13317
            7.3.8  Nonzero rings and zero rings   cnzr 13321
            7.3.9  Local rings   clring 13329
            7.3.10  Subrings of a ring   csubrg 13336
      ​7.4  Division rings and fields
            7.4.1  Ring apartness   capr 13368
      ​7.5  The complex numbers as an algebraic extensible structure
            7.5.1  Definition and basic properties   cpsmet 13375
            ​*7.5.2  Ring of integers   czring 13416
​PART 8  BASIC TOPOLOGY
      ​8.1  Topology
            ​*8.1.1  Topological spaces   ctop 13433
                  8.1.1.1  Topologies   ctop 13433
                  8.1.1.2  Topologies on sets   ctopon 13446
                  8.1.1.3  Topological spaces   ctps 13466
            8.1.2  Topological bases   ctb 13478
            8.1.3  Examples of topologies   distop 13521
            8.1.4  Closure and interior   ccld 13528
            8.1.5  Neighborhoods   cnei 13574
            8.1.6  Subspace topologies   restrcl 13603
            8.1.7  Limits and continuity in topological spaces   ccn 13621
            8.1.8  Product topologies   ctx 13688
            8.1.9  Continuous function-builders   cnmptid 13717
            8.1.10  Homeomorphisms   chmeo 13736
      ​8.2  Metric spaces
            8.2.1  Pseudometric spaces   psmetrel 13758
            8.2.2  Basic metric space properties   cxms 13772
            8.2.3  Metric space balls   blfvalps 13821
            8.2.4  Open sets of a metric space   mopnrel 13877
            8.2.5  Continuity in metric spaces   metcnp3 13947
            8.2.6  Topology on the reals   qtopbasss 13957
            8.2.7  Topological definitions using the reals   ccncf 13993
​PART 9  BASIC REAL AND COMPLEX ANALYSIS
            9.0.1  Dedekind cuts   dedekindeulemuub 14031
            9.0.2  Intermediate value theorem   ivthinclemlm 14048
      ​9.1  Derivatives
            9.1.1  Real and complex differentiation   climc 14059
                  9.1.1.1  Derivatives of functions of one complex or real variable   climc 14059
​PART 10  BASIC REAL AND COMPLEX FUNCTIONS
      ​10.1  Basic trigonometry
            10.1.1  The exponential, sine, and cosine functions (cont.)   efcn 14125
            10.1.2  Properties of pi = 3.14159...   pilem1 14136
            10.1.3  The natural logarithm on complex numbers   clog 14213
            ​*10.1.4  Logarithms to an arbitrary base   clogb 14297
            10.1.5  Quartic binomial expansion   binom4 14333
      ​10.2  Basic number theory
            ​*10.2.1  Quadratic residues and the Legendre symbol   clgs 14334
            10.2.2  Quadratic reciprocity   lgseisenlem1 14386
            10.2.3  All primes 4n+1 are the sum of two squares   2sqlem1 14397
​PART 11  GUIDES AND MISCELLANEA
      ​11.1  Guides (conventions, explanations, and examples)
            ​*11.1.1  Conventions   conventions 14409
            11.1.2  Definitional examples   ex-or 14410
​PART 12  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​12.1  Mathboxes for user contributions
            12.1.1  Mathbox guidelines   mathbox 14420
      ​12.2  Mathbox for BJ
            12.2.1  Propositional calculus   bj-nnsn 14421
                  ​*12.2.1.1  Stable formulas   bj-trst 14427
                  12.2.1.2  Decidable formulas   bj-trdc 14440
            12.2.2  Predicate calculus   bj-ex 14450
            12.2.3  Set theorey miscellaneous   bj-el2oss1o 14462
            ​*12.2.4  Extensionality   bj-vtoclgft 14463
            ​*12.2.5  Decidability of classes   wdcin 14481
            12.2.6  Disjoint union   djucllem 14488
            12.2.7  Miscellaneous   funmptd 14491
            ​*12.2.8  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 14500
                  *12.2.8.1  Bounded formulas   wbd 14500
                  ​*12.2.8.2  Bounded classes   wbdc 14528
            ​*12.2.9  CZF: Bounded separation   ax-bdsep 14572
                  12.2.9.1  Delta_0-classical logic   ax-bj-d0cl 14612
                  12.2.9.2  Inductive classes and the class of natural number ordinals   wind 14614
                  ​*12.2.9.3  The first three Peano postulates   bj-peano2 14627
            ​*12.2.10  CZF: Infinity   ax-infvn 14629
                  *12.2.10.1  The set of natural number ordinals   ax-infvn 14629
                  ​*12.2.10.2  Peano's fifth postulate   bdpeano5 14631
                  ​*12.2.10.3  Bounded induction and Peano's fourth postulate   findset 14633
            ​*12.2.11  CZF: Set induction   setindft 14653
                  *12.2.11.1  Set induction   setindft 14653
                  ​*12.2.11.2  Full induction   bj-findis 14667
            ​*12.2.12  CZF: Strong collection   ax-strcoll 14670
            ​*12.2.13  CZF: Subset collection   ax-sscoll 14675
            12.2.14  Real numbers   ax-ddkcomp 14677
      ​12.3  Mathbox for Jim Kingdon
            12.3.1  Propositional and predicate logic   nnnotnotr 14678
            12.3.2  Natural numbers   ss1oel2o 14679
            12.3.3  The power set of a singleton   pwtrufal 14683
            12.3.4  Omniscience of NN+oo   0nninf 14689
            12.3.5  Schroeder-Bernstein Theorem   exmidsbthrlem 14706
            12.3.6  Real and complex numbers   qdencn 14711
            ​*12.3.7  Analytic omniscience principles   trilpolemclim 14720
            12.3.8  Supremum and infimum   supfz 14754
            12.3.9  Circle constant   taupi 14756
      ​12.4  Mathbox for Mykola Mostovenko
      ​12.5  Mathbox for David A. Wheeler
            12.5.1  Testable propositions   dftest 14758
            ​*12.5.2  Allsome quantifier   walsi 14759