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  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 103
            1.2.5  Logical negation (intuitionistic)   ax-in1 609
            1.2.6  Logical disjunction   wo 703
            1.2.7  Stable propositions   wstab 825
            1.2.8  Decidable propositions   wdc 829
            ​*1.2.9  Theorems of decidable propositions   const 847
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 911
            1.2.11  Abbreviated conjunction and disjunction of three wff's   w3o 972
            1.2.12  True and false constants   wal 1346
                  ​*1.2.12.1  Universal quantifier for use by df-tru   wal 1346
                  ​*1.2.12.2  Equality predicate for use by df-tru   cv 1347
                  1.2.12.3  Define the true and false constants   wtru 1349
            1.2.13  Logical 'xor'   wxo 1370
            ​*1.2.14  Truth tables: Operations on true and false constants   truantru 1396
            ​*1.2.15  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1418
            1.2.16  Logical implication (continued)   syl6an 1427
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1440
            ​*1.3.2  Equality predicate (continued)   weq 1496
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1519
            1.3.4  Introduce Axiom of Existence   ax-i9 1523
            1.3.5  Additional intuitionistic axioms   ax-ial 1527
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1529
            1.3.7  The existential quantifier   19.8a 1583
            1.3.8  Equality theorems without distinct variables   a9e 1689
            1.3.9  Axioms ax-10 and ax-11   ax10o 1708
            1.3.10  Substitution (without distinct variables)   wsb 1755
            1.3.11  Theorems using axiom ax-11   equs5a 1787
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1804
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1815
            1.4.3  More theorems related to ax-11 and substitution   albidv 1817
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1851
            1.4.5  More substitution theorems   hbs1 1931
            1.4.6  Existential uniqueness   weu 2019
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2117
      ​​*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 2152
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2156
            2.1.3  Class form not-free predicate   wnfc 2299
            2.1.4  Negated equality and membership   wne 2340
                  2.1.4.1  Negated equality   wne 2340
                  2.1.4.2  Negated membership   wnel 2435
            2.1.5  Restricted quantification   wral 2448
            2.1.6  The universal class   cvv 2730
            ​*2.1.7  Conditional equality (experimental)   wcdeq 2938
            2.1.8  Russell's Paradox   ru 2954
            2.1.9  Proper substitution of classes for sets   wsbc 2955
            2.1.10  Proper substitution of classes for sets into classes   csb 3049
            2.1.11  Define basic set operations and relations   cdif 3118
            2.1.12  Subclasses and subsets   df-ss 3134
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3237
                  2.1.13.1  The difference of two classes   dfdif3 3237
                  2.1.13.2  The union of two classes   elun 3268
                  2.1.13.3  The intersection of two classes   elin 3310
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3358
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3393
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3407
            2.1.14  The empty set   c0 3414
            2.1.15  Conditional operator   cif 3526
            2.1.16  Power classes   cpw 3566
            2.1.17  Unordered and ordered pairs   csn 3583
            2.1.18  The union of a class   cuni 3796
            2.1.19  The intersection of a class   cint 3831
            2.1.20  Indexed union and intersection   ciun 3873
            2.1.21  Disjointness   wdisj 3966
            2.1.22  Binary relations   wbr 3989
            2.1.23  Ordered-pair class abstractions (class builders)   copab 4049
            2.1.24  Transitive classes   wtr 4087
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4104
            2.2.2  Introduce the Axiom of Separation   ax-sep 4107
            2.2.3  Derive the Null Set Axiom   zfnuleu 4113
            2.2.4  Theorems requiring subset and intersection existence   nalset 4119
            2.2.5  Theorems requiring empty set existence   class2seteq 4149
            2.2.6  Collection principle   bnd 4158
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4160
            2.3.2  A notation for excluded middle   wem 4180
            2.3.3  Axiom of Pairing   ax-pr 4194
            2.3.4  Ordered pair theorem   opm 4219
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4242
            2.3.6  Power class of union and intersection   pwin 4267
            2.3.7  Epsilon and identity relations   cep 4272
            ​*2.3.8  Partial and total orderings   wpo 4279
            2.3.9  Founded and set-like relations   wfrfor 4312
            2.3.10  Ordinals   word 4347
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4418
            2.4.2  Ordinals (continued)   ordon 4470
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4516
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4521
            2.5.3  Transfinite induction   tfi 4566
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4572
            2.6.2  The natural numbers   com 4574
            2.6.3  Peano's postulates   peano1 4578
            2.6.4  Finite induction (for finite ordinals)   find 4583
            2.6.5  The Natural Numbers (continued)   nn0suc 4588
            2.6.6  Relations   cxp 4609
            2.6.7  Definite description binder (inverted iota)   cio 5158
            2.6.8  Functions   wfun 5192
            2.6.9  Cantor's Theorem   canth 5807
            2.6.10  Restricted iota (description binder)   crio 5808
            2.6.11  Operations   co 5853
            2.6.12  Maps-to notation   elmpocl 6047
            2.6.13  Function operation   cof 6059
            2.6.14  Functions (continued)   resfunexgALT 6087
            2.6.15  First and second members of an ordered pair   c1st 6117
            ​*2.6.16  Special maps-to operations   opeliunxp2f 6217
            2.6.17  Function transposition   ctpos 6223
            2.6.18  Undefined values   pwuninel2 6261
            2.6.19  Functions on ordinals; strictly monotone ordinal functions   iunon 6263
            2.6.20  "Strong" transfinite recursion   crecs 6283
            2.6.21  Recursive definition generator   crdg 6348
            2.6.22  Finite recursion   cfrec 6369
            2.6.23  Ordinal arithmetic   c1o 6388
            2.6.24  Natural number arithmetic   nna0 6453
            2.6.25  Equivalence relations and classes   wer 6510
            2.6.26  The mapping operation   cmap 6626
            2.6.27  Infinite Cartesian products   cixp 6676
            2.6.28  Equinumerosity   cen 6716
            2.6.29  Equinumerosity (cont.)   xpf1o 6822
            2.6.30  Pigeonhole Principle   phplem1 6830
            2.6.31  Finite sets   fict 6846
            2.6.32  Schroeder-Bernstein Theorem   sbthlem1 6934
            2.6.33  Finite intersections   cfi 6945
            2.6.34  Supremum and infimum   csup 6959
            2.6.35  Ordinal isomorphism   ordiso2 7012
            2.6.36  Disjoint union   cdju 7014
                  2.6.36.1  Disjoint union   cdju 7014
                  ​*2.6.36.2  Left and right injections of a disjoint union   cinl 7022
                  2.6.36.3  Universal property of the disjoint union   djuss 7047
                  2.6.36.4  Dominance and equinumerosity properties of disjoint union   djudom 7070
                  2.6.36.5  Older definition temporarily kept for comparison, to be deleted   cdjud 7079
                  2.6.36.6  Countable sets   0ct 7084
            ​*2.6.37  The one-point compactification of the natural numbers   xnninf 7096
            2.6.38  Omniscient sets   comni 7110
            2.6.39  Markov's principle   cmarkov 7127
            2.6.40  Weakly omniscient sets   cwomni 7139
            2.6.41  Cardinal numbers   ccrd 7156
            2.6.42  Axiom of Choice equivalents   wac 7182
            2.6.43  Cardinal number arithmetic   endjudisj 7187
            2.6.44  Ordinal trichotomy   exmidontriimlem1 7198
            2.6.45  Excluded middle and the power set of a singleton   pw1on 7203
​​*PART 3  CHOICE PRINCIPLES
      ​3.1  Countable Choice and Dependent Choice
            3.1.1  Introduce Countable Choice   wacc 7224
​​*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 7234
            4.1.2  Final derivation of real and complex number postulates   axcnex 7821
            4.1.3  Real and complex number postulates restated as axioms   ax-cnex 7865
      ​4.2  Derive the basic properties from the field axioms
            4.2.1  Some deductions from the field axioms for complex numbers   cnex 7898
            4.2.2  Infinity and the extended real number system   cpnf 7951
            4.2.3  Restate the ordering postulates with extended real "less than"   axltirr 7986
            4.2.4  Ordering on reals   lttr 7993
            4.2.5  Initial properties of the complex numbers   mul12 8048
      ​4.3  Real and complex numbers - basic operations
            4.3.1  Addition   add12 8077
            4.3.2  Subtraction   cmin 8090
            4.3.3  Multiplication   kcnktkm1cn 8302
            4.3.4  Ordering on reals (cont.)   ltadd2 8338
            4.3.5  Real Apartness   creap 8493
            4.3.6  Complex Apartness   cap 8500
            4.3.7  Reciprocals   recextlem1 8569
            4.3.8  Division   cdiv 8589
            4.3.9  Ordering on reals (cont.)   ltp1 8760
            4.3.10  Suprema   lbreu 8861
            4.3.11  Imaginary and complex number properties   crap0 8874
      ​4.4  Integer sets
            4.4.1  Positive integers (as a subset of complex numbers)   cn 8878
            4.4.2  Principle of mathematical induction   nnind 8894
            ​*4.4.3  Decimal representation of numbers   c2 8929
            ​*4.4.4  Some properties of specific numbers   neg1cn 8983
            4.4.5  Simple number properties   halfcl 9104
            4.4.6  The Archimedean property   arch 9132
            4.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 9135
            ​*4.4.8  Extended nonnegative integers   cxnn0 9198
            4.4.9  Integers (as a subset of complex numbers)   cz 9212
            4.4.10  Decimal arithmetic   cdc 9343
            4.4.11  Upper sets of integers   cuz 9487
            4.4.12  Rational numbers (as a subset of complex numbers)   cq 9578
            4.4.13  Complex numbers as pairs of reals   cnref1o 9609
      ​4.5  Order sets
            4.5.1  Positive reals (as a subset of complex numbers)   crp 9610
            4.5.2  Infinity and the extended real number system (cont.)   cxne 9726
            4.5.3  Real number intervals   cioo 9845
            4.5.4  Finite intervals of integers   cfz 9965
            ​*4.5.5  Finite intervals of nonnegative integers   elfz2nn0 10068
            4.5.6  Half-open integer ranges   cfzo 10098
            4.5.7  Rational numbers (cont.)   qtri3or 10199
      ​4.6  Elementary integer functions
            4.6.1  The floor and ceiling functions   cfl 10224
            4.6.2  The modulo (remainder) operation   cmo 10278
            4.6.3  Miscellaneous theorems about integers   frec2uz0d 10355
            4.6.4  Strong induction over upper sets of integers   uzsinds 10398
            4.6.5  The infinite sequence builder "seq"   cseq 10401
            4.6.6  Integer powers   cexp 10475
            4.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 10653
            4.6.8  Factorial function   cfa 10659
            4.6.9  The binomial coefficient operation   cbc 10681
            4.6.10  The ` # ` (set size) function   chash 10709
      ​4.7  Elementary real and complex functions
            4.7.1  The "shift" operation   cshi 10778
            4.7.2  Real and imaginary parts; conjugate   ccj 10803
            4.7.3  Sequence convergence   caucvgrelemrec 10943
            4.7.4  Square root; absolute value   csqrt 10960
            4.7.5  The maximum of two real numbers   maxcom 11167
            4.7.6  The minimum of two real numbers   mincom 11192
            4.7.7  The maximum of two extended reals   xrmaxleim 11207
            4.7.8  The minimum of two extended reals   xrnegiso 11225
      ​4.8  Elementary limits and convergence
            4.8.1  Limits   cli 11241
            4.8.2  Finite and infinite sums   csu 11316
            4.8.3  The binomial theorem   binomlem 11446
            4.8.4  Infinite sums (cont.)   isumshft 11453
            4.8.5  Miscellaneous converging and diverging sequences   divcnv 11460
            4.8.6  Arithmetic series   arisum 11461
            4.8.7  Geometric series   expcnvap0 11465
            4.8.8  Ratio test for infinite series convergence   cvgratnnlembern 11486
            4.8.9  Mertens' theorem   mertenslemub 11497
            4.8.10  Finite and infinite products   prodf 11501
                  4.8.10.1  Product sequences   prodf 11501
                  4.8.10.2  Non-trivial convergence   ntrivcvgap 11511
                  4.8.10.3  Complex products   cprod 11513
                  4.8.10.4  Finite products   fprodseq 11546
      ​4.9  Elementary trigonometry
            4.9.1  The exponential, sine, and cosine functions   ce 11605
                  4.9.1.1  The circle constant (tau = 2 pi)   ctau 11737
            4.9.2  _e is irrational   eirraplem 11739
​​*PART 5  ELEMENTARY NUMBER THEORY
      ​5.1  Elementary properties of divisibility
            5.1.1  The divides relation   cdvds 11749
            ​*5.1.2  Even and odd numbers   evenelz 11826
            5.1.3  The division algorithm   divalglemnn 11877
            5.1.4  The greatest common divisor operator   cgcd 11897
            5.1.5  Bézout's identity   bezoutlemnewy 11951
            5.1.6  Decidable sets of integers   nnmindc 11989
            5.1.7  Algorithms   nn0seqcvgd 11995
            5.1.8  Euclid's Algorithm   eucalgval2 12007
            ​*5.1.9  The least common multiple   clcm 12014
            ​*5.1.10  Coprimality and Euclid's lemma   coprmgcdb 12042
            5.1.11  Cancellability of congruences   congr 12054
      ​5.2  Elementary prime number theory
            ​*5.2.1  Elementary properties   cprime 12061
            ​*5.2.2  Coprimality and Euclid's lemma (cont.)   coprm 12098
            5.2.3  Non-rationality of square root of 2   sqrt2irrlem 12115
            5.2.4  Properties of the canonical representation of a rational   cnumer 12135
            5.2.5  Euler's theorem   codz 12162
            5.2.6  Arithmetic modulo a prime number   modprm1div 12201
            5.2.7  Pythagorean Triples   coprimeprodsq 12211
            5.2.8  The prime count function   cpc 12238
            5.2.9  Pocklington's theorem   prmpwdvds 12307
            5.2.10  Infinite primes theorem   infpnlem1 12311
            5.2.11  Fundamental theorem of arithmetic   1arithlem1 12315
            5.2.12  Lagrange's four-square theorem   cgz 12321
      ​5.3  Cardinality of real and complex number subsets
            5.3.1  Countability of integers and rationals   oddennn 12347
​PART 6  BASIC STRUCTURES
      ​6.1  Extensible structures
            ​*6.1.1  Basic definitions   cstr 12412
            6.1.2  Slot definitions   cplusg 12480
            6.1.3  Definition of the structure product   crest 12579
​PART 7  BASIC ALGEBRAIC STRUCTURES
      ​7.1  Monoids
            ​*7.1.1  Magmas   cplusf 12607
            ​*7.1.2  Identity elements   mgmidmo 12626
            ​*7.1.3  Semigroups   csgrp 12642
            ​*7.1.4  Definition and basic properties of monoids   cmnd 12652
            7.1.5  Monoid homomorphisms and submonoids   cmhm 12681
      ​7.2  Groups
            7.2.1  Definition and basic properties   cgrp 12708
      ​7.3  The complex numbers as an algebraic extensible structure
            7.3.1  Definition and basic properties   cpsmet 12773
​PART 8  BASIC TOPOLOGY
      ​8.1  Topology
            ​*8.1.1  Topological spaces   ctop 12789
                  8.1.1.1  Topologies   ctop 12789
                  8.1.1.2  Topologies on sets   ctopon 12802
                  8.1.1.3  Topological spaces   ctps 12822
            8.1.2  Topological bases   ctb 12834
            8.1.3  Examples of topologies   distop 12879
            8.1.4  Closure and interior   ccld 12886
            8.1.5  Neighborhoods   cnei 12932
            8.1.6  Subspace topologies   restrcl 12961
            8.1.7  Limits and continuity in topological spaces   ccn 12979
            8.1.8  Product topologies   ctx 13046
            8.1.9  Continuous function-builders   cnmptid 13075
            8.1.10  Homeomorphisms   chmeo 13094
      ​8.2  Metric spaces
            8.2.1  Pseudometric spaces   psmetrel 13116
            8.2.2  Basic metric space properties   cxms 13130
            8.2.3  Metric space balls   blfvalps 13179
            8.2.4  Open sets of a metric space   mopnrel 13235
            8.2.5  Continuity in metric spaces   metcnp3 13305
            8.2.6  Topology on the reals   qtopbasss 13315
            8.2.7  Topological definitions using the reals   ccncf 13351
​PART 9  BASIC REAL AND COMPLEX ANALYSIS
            9.0.1  Dedekind cuts   dedekindeulemuub 13389
            9.0.2  Intermediate value theorem   ivthinclemlm 13406
      ​9.1  Derivatives
            9.1.1  Real and complex differentiation   climc 13417
                  9.1.1.1  Derivatives of functions of one complex or real variable   climc 13417
​PART 10  BASIC REAL AND COMPLEX FUNCTIONS
      ​10.1  Basic trigonometry
            10.1.1  The exponential, sine, and cosine functions (cont.)   efcn 13483
            10.1.2  Properties of pi = 3.14159...   pilem1 13494
            10.1.3  The natural logarithm on complex numbers   clog 13571
            ​*10.1.4  Logarithms to an arbitrary base   clogb 13655
            10.1.5  Quartic binomial expansion   binom4 13691
      ​10.2  Basic number theory
            ​*10.2.1  Quadratic residues and the Legendre symbol   clgs 13692
            10.2.2  All primes 4n+1 are the sum of two squares   2sqlem1 13744
​PART 11  GUIDES AND MISCELLANEA
      ​11.1  Guides (conventions, explanations, and examples)
            ​*11.1.1  Conventions   conventions 13756
            11.1.2  Definitional examples   ex-or 13757
​PART 12  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​12.1  Mathboxes for user contributions
            12.1.1  Mathbox guidelines   mathbox 13767
      ​12.2  Mathbox for BJ
            12.2.1  Propositional calculus   bj-nnsn 13768
                  ​*12.2.1.1  Stable formulas   bj-trst 13774
                  12.2.1.2  Decidable formulas   bj-trdc 13787
            12.2.2  Predicate calculus   bj-ex 13797
            12.2.3  Set theorey miscellaneous   bj-el2oss1o 13809
            ​*12.2.4  Extensionality   bj-vtoclgft 13810
            ​*12.2.5  Decidability of classes   wdcin 13828
            12.2.6  Disjoint union   djucllem 13835
            12.2.7  Miscellaneous   funmptd 13838
            ​*12.2.8  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 13847
                  *12.2.8.1  Bounded formulas   wbd 13847
                  ​*12.2.8.2  Bounded classes   wbdc 13875
            ​*12.2.9  CZF: Bounded separation   ax-bdsep 13919
                  12.2.9.1  Delta_0-classical logic   ax-bj-d0cl 13959
                  12.2.9.2  Inductive classes and the class of natural number ordinals   wind 13961
                  ​*12.2.9.3  The first three Peano postulates   bj-peano2 13974
            ​*12.2.10  CZF: Infinity   ax-infvn 13976
                  *12.2.10.1  The set of natural number ordinals   ax-infvn 13976
                  ​*12.2.10.2  Peano's fifth postulate   bdpeano5 13978
                  ​*12.2.10.3  Bounded induction and Peano's fourth postulate   findset 13980
            ​*12.2.11  CZF: Set induction   setindft 14000
                  *12.2.11.1  Set induction   setindft 14000
                  ​*12.2.11.2  Full induction   bj-findis 14014
            ​*12.2.12  CZF: Strong collection   ax-strcoll 14017
            ​*12.2.13  CZF: Subset collection   ax-sscoll 14022
            12.2.14  Real numbers   ax-ddkcomp 14024
      ​12.3  Mathbox for Jim Kingdon
            12.3.1  Propositional and predicate logic   nnnotnotr 14025
            12.3.2  Natural numbers   ss1oel2o 14026
            12.3.3  The power set of a singleton   pwtrufal 14030
            12.3.4  Omniscience of NN+oo   0nninf 14037
            12.3.5  Schroeder-Bernstein Theorem   exmidsbthrlem 14054
            12.3.6  Real and complex numbers   qdencn 14059
            ​*12.3.7  Analytic omniscience principles   trilpolemclim 14068
            12.3.8  Supremum and infimum   supfz 14100
            12.3.9  Circle constant   taupi 14102
      ​12.4  Mathbox for Mykola Mostovenko
      ​12.5  Mathbox for David A. Wheeler
            12.5.1  Testable propositions   dftest 14104
            ​*12.5.2  Allsome quantifier   walsi 14105