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
      9.2  Basic number theory
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 820
            1.2.8  Decidable propositions   wdc 824
            ​*1.2.9  Theorems of decidable propositions   const 842
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 906
            1.2.11  Abbreviated conjunction and disjunction of three wff's   w3o 967
            1.2.12  True and false constants   wal 1341
                  ​*1.2.12.1  Universal quantifier for use by df-tru   wal 1341
                  ​*1.2.12.2  Equality predicate for use by df-tru   cv 1342
                  1.2.12.3  Define the true and false constants   wtru 1344
            1.2.13  Logical 'xor'   wxo 1365
            ​*1.2.14  Truth tables: Operations on true and false constants   truantru 1391
            ​*1.2.15  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1413
            1.2.16  Logical implication (continued)   syl6an 1422
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1435
            ​*1.3.2  Equality predicate (continued)   weq 1491
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1514
            1.3.4  Introduce Axiom of Existence   ax-i9 1518
            1.3.5  Additional intuitionistic axioms   ax-ial 1522
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1524
            1.3.7  The existential quantifier   19.8a 1578
            1.3.8  Equality theorems without distinct variables   a9e 1684
            1.3.9  Axioms ax-10 and ax-11   ax10o 1703
            1.3.10  Substitution (without distinct variables)   wsb 1750
            1.3.11  Theorems using axiom ax-11   equs5a 1782
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1799
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1810
            1.4.3  More theorems related to ax-11 and substitution   albidv 1812
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1846
            1.4.5  More substitution theorems   hbs1 1926
            1.4.6  Existential uniqueness   weu 2014
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2112
      ​​*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 2147
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2151
            2.1.3  Class form not-free predicate   wnfc 2294
            2.1.4  Negated equality and membership   wne 2335
                  2.1.4.1  Negated equality   wne 2335
                  2.1.4.2  Negated membership   wnel 2430
            2.1.5  Restricted quantification   wral 2443
            2.1.6  The universal class   cvv 2725
            ​*2.1.7  Conditional equality (experimental)   wcdeq 2933
            2.1.8  Russell's Paradox   ru 2949
            2.1.9  Proper substitution of classes for sets   wsbc 2950
            2.1.10  Proper substitution of classes for sets into classes   csb 3044
            2.1.11  Define basic set operations and relations   cdif 3112
            2.1.12  Subclasses and subsets   df-ss 3128
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3231
                  2.1.13.1  The difference of two classes   dfdif3 3231
                  2.1.13.2  The union of two classes   elun 3262
                  2.1.13.3  The intersection of two classes   elin 3304
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3352
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3387
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3401
            2.1.14  The empty set   c0 3408
            2.1.15  Conditional operator   cif 3519
            2.1.16  Power classes   cpw 3558
            2.1.17  Unordered and ordered pairs   csn 3575
            2.1.18  The union of a class   cuni 3788
            2.1.19  The intersection of a class   cint 3823
            2.1.20  Indexed union and intersection   ciun 3865
            2.1.21  Disjointness   wdisj 3958
            2.1.22  Binary relations   wbr 3981
            2.1.23  Ordered-pair class abstractions (class builders)   copab 4041
            2.1.24  Transitive classes   wtr 4079
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4096
            2.2.2  Introduce the Axiom of Separation   ax-sep 4099
            2.2.3  Derive the Null Set Axiom   zfnuleu 4105
            2.2.4  Theorems requiring subset and intersection existence   nalset 4111
            2.2.5  Theorems requiring empty set existence   class2seteq 4141
            2.2.6  Collection principle   bnd 4150
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4152
            2.3.2  A notation for excluded middle   wem 4172
            2.3.3  Axiom of Pairing   ax-pr 4186
            2.3.4  Ordered pair theorem   opm 4211
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4234
            2.3.6  Power class of union and intersection   pwin 4259
            2.3.7  Epsilon and identity relations   cep 4264
            ​*2.3.8  Partial and total orderings   wpo 4271
            2.3.9  Founded and set-like relations   wfrfor 4304
            2.3.10  Ordinals   word 4339
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4410
            2.4.2  Ordinals (continued)   ordon 4462
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4508
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4513
            2.5.3  Transfinite induction   tfi 4558
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4564
            2.6.2  The natural numbers   com 4566
            2.6.3  Peano's postulates   peano1 4570
            2.6.4  Finite induction (for finite ordinals)   find 4575
            2.6.5  The Natural Numbers (continued)   nn0suc 4580
            2.6.6  Relations   cxp 4601
            2.6.7  Definite description binder (inverted iota)   cio 5150
            2.6.8  Functions   wfun 5181
            2.6.9  Cantor's Theorem   canth 5795
            2.6.10  Restricted iota (description binder)   crio 5796
            2.6.11  Operations   co 5841
            2.6.12  Maps-to notation   elmpocl 6035
            2.6.13  Function operation   cof 6047
            2.6.14  Functions (continued)   resfunexgALT 6075
            2.6.15  First and second members of an ordered pair   c1st 6103
            ​*2.6.16  Special maps-to operations   opeliunxp2f 6202
            2.6.17  Function transposition   ctpos 6208
            2.6.18  Undefined values   pwuninel2 6246
            2.6.19  Functions on ordinals; strictly monotone ordinal functions   iunon 6248
            2.6.20  "Strong" transfinite recursion   crecs 6268
            2.6.21  Recursive definition generator   crdg 6333
            2.6.22  Finite recursion   cfrec 6354
            2.6.23  Ordinal arithmetic   c1o 6373
            2.6.24  Natural number arithmetic   nna0 6438
            2.6.25  Equivalence relations and classes   wer 6494
            2.6.26  The mapping operation   cmap 6610
            2.6.27  Infinite Cartesian products   cixp 6660
            2.6.28  Equinumerosity   cen 6700
            2.6.29  Equinumerosity (cont.)   xpf1o 6806
            2.6.30  Pigeonhole Principle   phplem1 6814
            2.6.31  Finite sets   fict 6830
            2.6.32  Schroeder-Bernstein Theorem   sbthlem1 6918
            2.6.33  Finite intersections   cfi 6929
            2.6.34  Supremum and infimum   csup 6943
            2.6.35  Ordinal isomorphism   ordiso2 6996
            2.6.36  Disjoint union   cdju 6998
                  2.6.36.1  Disjoint union   cdju 6998
                  ​*2.6.36.2  Left and right injections of a disjoint union   cinl 7006
                  2.6.36.3  Universal property of the disjoint union   djuss 7031
                  2.6.36.4  Dominance and equinumerosity properties of disjoint union   djudom 7054
                  2.6.36.5  Older definition temporarily kept for comparison, to be deleted   cdjud 7063
                  2.6.36.6  Countable sets   0ct 7068
            ​*2.6.37  The one-point compactification of the natural numbers   xnninf 7080
            2.6.38  Omniscient sets   comni 7094
            2.6.39  Markov's principle   cmarkov 7111
            2.6.40  Weakly omniscient sets   cwomni 7123
            2.6.41  Cardinal numbers   ccrd 7131
            2.6.42  Axiom of Choice equivalents   wac 7157
            2.6.43  Cardinal number arithmetic   endjudisj 7162
            2.6.44  Ordinal trichotomy   exmidontriimlem1 7173
            2.6.45  Excluded middle and the power set of a singleton   pw1on 7178
​​*PART 3  CHOICE PRINCIPLES
      ​3.1  Countable Choice and Dependent Choice
            3.1.1  Introduce Countable Choice   wacc 7199
​​*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 7209
            4.1.2  Final derivation of real and complex number postulates   axcnex 7796
            4.1.3  Real and complex number postulates restated as axioms   ax-cnex 7840
      ​4.2  Derive the basic properties from the field axioms
            4.2.1  Some deductions from the field axioms for complex numbers   cnex 7873
            4.2.2  Infinity and the extended real number system   cpnf 7926
            4.2.3  Restate the ordering postulates with extended real "less than"   axltirr 7961
            4.2.4  Ordering on reals   lttr 7968
            4.2.5  Initial properties of the complex numbers   mul12 8023
      ​4.3  Real and complex numbers - basic operations
            4.3.1  Addition   add12 8052
            4.3.2  Subtraction   cmin 8065
            4.3.3  Multiplication   kcnktkm1cn 8277
            4.3.4  Ordering on reals (cont.)   ltadd2 8313
            4.3.5  Real Apartness   creap 8468
            4.3.6  Complex Apartness   cap 8475
            4.3.7  Reciprocals   recextlem1 8544
            4.3.8  Division   cdiv 8564
            4.3.9  Ordering on reals (cont.)   ltp1 8735
            4.3.10  Suprema   lbreu 8836
            4.3.11  Imaginary and complex number properties   crap0 8849
      ​4.4  Integer sets
            4.4.1  Positive integers (as a subset of complex numbers)   cn 8853
            4.4.2  Principle of mathematical induction   nnind 8869
            ​*4.4.3  Decimal representation of numbers   c2 8904
            ​*4.4.4  Some properties of specific numbers   neg1cn 8958
            4.4.5  Simple number properties   halfcl 9079
            4.4.6  The Archimedean property   arch 9107
            4.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 9110
            ​*4.4.8  Extended nonnegative integers   cxnn0 9173
            4.4.9  Integers (as a subset of complex numbers)   cz 9187
            4.4.10  Decimal arithmetic   cdc 9318
            4.4.11  Upper sets of integers   cuz 9462
            4.4.12  Rational numbers (as a subset of complex numbers)   cq 9553
            4.4.13  Complex numbers as pairs of reals   cnref1o 9584
      ​4.5  Order sets
            4.5.1  Positive reals (as a subset of complex numbers)   crp 9585
            4.5.2  Infinity and the extended real number system (cont.)   cxne 9701
            4.5.3  Real number intervals   cioo 9820
            4.5.4  Finite intervals of integers   cfz 9940
            ​*4.5.5  Finite intervals of nonnegative integers   elfz2nn0 10043
            4.5.6  Half-open integer ranges   cfzo 10073
            4.5.7  Rational numbers (cont.)   qtri3or 10174
      ​4.6  Elementary integer functions
            4.6.1  The floor and ceiling functions   cfl 10199
            4.6.2  The modulo (remainder) operation   cmo 10253
            4.6.3  Miscellaneous theorems about integers   frec2uz0d 10330
            4.6.4  Strong induction over upper sets of integers   uzsinds 10373
            4.6.5  The infinite sequence builder "seq"   cseq 10376
            4.6.6  Integer powers   cexp 10450
            4.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 10628
            4.6.8  Factorial function   cfa 10634
            4.6.9  The binomial coefficient operation   cbc 10656
            4.6.10  The ` # ` (set size) function   chash 10684
      ​4.7  Elementary real and complex functions
            4.7.1  The "shift" operation   cshi 10752
            4.7.2  Real and imaginary parts; conjugate   ccj 10777
            4.7.3  Sequence convergence   caucvgrelemrec 10917
            4.7.4  Square root; absolute value   csqrt 10934
            4.7.5  The maximum of two real numbers   maxcom 11141
            4.7.6  The minimum of two real numbers   mincom 11166
            4.7.7  The maximum of two extended reals   xrmaxleim 11181
            4.7.8  The minimum of two extended reals   xrnegiso 11199
      ​4.8  Elementary limits and convergence
            4.8.1  Limits   cli 11215
            4.8.2  Finite and infinite sums   csu 11290
            4.8.3  The binomial theorem   binomlem 11420
            4.8.4  Infinite sums (cont.)   isumshft 11427
            4.8.5  Miscellaneous converging and diverging sequences   divcnv 11434
            4.8.6  Arithmetic series   arisum 11435
            4.8.7  Geometric series   expcnvap0 11439
            4.8.8  Ratio test for infinite series convergence   cvgratnnlembern 11460
            4.8.9  Mertens' theorem   mertenslemub 11471
            4.8.10  Finite and infinite products   prodf 11475
                  4.8.10.1  Product sequences   prodf 11475
                  4.8.10.2  Non-trivial convergence   ntrivcvgap 11485
                  4.8.10.3  Complex products   cprod 11487
                  4.8.10.4  Finite products   fprodseq 11520
      ​4.9  Elementary trigonometry
            4.9.1  The exponential, sine, and cosine functions   ce 11579
                  4.9.1.1  The circle constant (tau = 2 pi)   ctau 11711
            4.9.2  _e is irrational   eirraplem 11713
​​*PART 5  ELEMENTARY NUMBER THEORY
      ​5.1  Elementary properties of divisibility
            5.1.1  The divides relation   cdvds 11723
            ​*5.1.2  Even and odd numbers   evenelz 11800
            5.1.3  The division algorithm   divalglemnn 11851
            5.1.4  The greatest common divisor operator   cgcd 11871
            5.1.5  Bézout's identity   bezoutlemnewy 11925
            5.1.6  Decidable sets of integers   nnmindc 11963
            5.1.7  Algorithms   nn0seqcvgd 11969
            5.1.8  Euclid's Algorithm   eucalgval2 11981
            ​*5.1.9  The least common multiple   clcm 11988
            ​*5.1.10  Coprimality and Euclid's lemma   coprmgcdb 12016
            5.1.11  Cancellability of congruences   congr 12028
      ​5.2  Elementary prime number theory
            ​*5.2.1  Elementary properties   cprime 12035
            ​*5.2.2  Coprimality and Euclid's lemma (cont.)   coprm 12072
            5.2.3  Non-rationality of square root of 2   sqrt2irrlem 12089
            5.2.4  Properties of the canonical representation of a rational   cnumer 12109
            5.2.5  Euler's theorem   codz 12136
            5.2.6  Arithmetic modulo a prime number   modprm1div 12175
            5.2.7  Pythagorean Triples   coprimeprodsq 12185
            5.2.8  The prime count function   cpc 12212
            5.2.9  Pocklington's theorem   prmpwdvds 12281
            5.2.10  Infinite primes theorem   infpnlem1 12285
            5.2.11  Fundamental theorem of arithmetic   1arithlem1 12289
            5.2.12  Lagrange's four-square theorem   cgz 12295
      ​5.3  Cardinality of real and complex number subsets
            5.3.1  Countability of integers and rationals   oddennn 12321
​PART 6  BASIC STRUCTURES
      ​6.1  Extensible structures
            ​*6.1.1  Basic definitions   cstr 12386
            6.1.2  Slot definitions   cplusg 12452
            6.1.3  Definition of the structure product   crest 12551
      ​6.2  The complex numbers as an algebraic extensible structure
            6.2.1  Definition and basic properties   cpsmet 12579
​PART 7  BASIC TOPOLOGY
      ​7.1  Topology
            ​*7.1.1  Topological spaces   ctop 12595
                  7.1.1.1  Topologies   ctop 12595
                  7.1.1.2  Topologies on sets   ctopon 12608
                  7.1.1.3  Topological spaces   ctps 12628
            7.1.2  Topological bases   ctb 12640
            7.1.3  Examples of topologies   distop 12685
            7.1.4  Closure and interior   ccld 12692
            7.1.5  Neighborhoods   cnei 12738
            7.1.6  Subspace topologies   restrcl 12767
            7.1.7  Limits and continuity in topological spaces   ccn 12785
            7.1.8  Product topologies   ctx 12852
            7.1.9  Continuous function-builders   cnmptid 12881
            7.1.10  Homeomorphisms   chmeo 12900
      ​7.2  Metric spaces
            7.2.1  Pseudometric spaces   psmetrel 12922
            7.2.2  Basic metric space properties   cxms 12936
            7.2.3  Metric space balls   blfvalps 12985
            7.2.4  Open sets of a metric space   mopnrel 13041
            7.2.5  Continuity in metric spaces   metcnp3 13111
            7.2.6  Topology on the reals   qtopbasss 13121
            7.2.7  Topological definitions using the reals   ccncf 13157
​PART 8  BASIC REAL AND COMPLEX ANALYSIS
            8.0.1  Dedekind cuts   dedekindeulemuub 13195
            8.0.2  Intermediate value theorem   ivthinclemlm 13212
      ​8.1  Derivatives
            8.1.1  Real and complex differentiation   climc 13223
                  8.1.1.1  Derivatives of functions of one complex or real variable   climc 13223
​PART 9  BASIC REAL AND COMPLEX FUNCTIONS
      ​9.1  Basic trigonometry
            9.1.1  The exponential, sine, and cosine functions (cont.)   efcn 13289
            9.1.2  Properties of pi = 3.14159...   pilem1 13300
            9.1.3  The natural logarithm on complex numbers   clog 13377
            ​*9.1.4  Logarithms to an arbitrary base   clogb 13461
            9.1.5  Quartic binomial expansion   binom4 13497
      ​9.2  Basic number theory
            ​*9.2.1  Quadratic residues and the Legendre symbol   clgs 13498
            9.2.2  All primes 4n+1 are the sum of two squares   2sqlem1 13550
​PART 10  GUIDES AND MISCELLANEA
      ​10.1  Guides (conventions, explanations, and examples)
            ​*10.1.1  Conventions   conventions 13562
            10.1.2  Definitional examples   ex-or 13563
​PART 11  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​11.1  Mathboxes for user contributions
            11.1.1  Mathbox guidelines   mathbox 13573
      ​11.2  Mathbox for BJ
            11.2.1  Propositional calculus   bj-nnsn 13574
                  ​*11.2.1.1  Stable formulas   bj-trst 13580
                  11.2.1.2  Decidable formulas   bj-trdc 13593
            11.2.2  Predicate calculus   bj-ex 13603
            11.2.3  Set theorey miscellaneous   bj-el2oss1o 13615
            ​*11.2.4  Extensionality   bj-vtoclgft 13616
            ​*11.2.5  Decidability of classes   wdcin 13634
            11.2.6  Disjoint union   djucllem 13641
            11.2.7  Miscellaneous   2ssom 13644
            ​*11.2.8  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 13654
                  *11.2.8.1  Bounded formulas   wbd 13654
                  ​*11.2.8.2  Bounded classes   wbdc 13682
            ​*11.2.9  CZF: Bounded separation   ax-bdsep 13726
                  11.2.9.1  Delta_0-classical logic   ax-bj-d0cl 13766
                  11.2.9.2  Inductive classes and the class of natural number ordinals   wind 13768
                  ​*11.2.9.3  The first three Peano postulates   bj-peano2 13781
            ​*11.2.10  CZF: Infinity   ax-infvn 13783
                  *11.2.10.1  The set of natural number ordinals   ax-infvn 13783
                  ​*11.2.10.2  Peano's fifth postulate   bdpeano5 13785
                  ​*11.2.10.3  Bounded induction and Peano's fourth postulate   findset 13787
            ​*11.2.11  CZF: Set induction   setindft 13807
                  *11.2.11.1  Set induction   setindft 13807
                  ​*11.2.11.2  Full induction   bj-findis 13821
            ​*11.2.12  CZF: Strong collection   ax-strcoll 13824
            ​*11.2.13  CZF: Subset collection   ax-sscoll 13829
            11.2.14  Real numbers   ax-ddkcomp 13831
      ​11.3  Mathbox for Jim Kingdon
            11.3.1  Propositional and predicate logic   nnnotnotr 13832
            11.3.2  Natural numbers   ss1oel2o 13833
            11.3.3  The power set of a singleton   pwtrufal 13837
            11.3.4  Omniscience of NN+oo   0nninf 13844
            11.3.5  Schroeder-Bernstein Theorem   exmidsbthrlem 13861
            11.3.6  Real and complex numbers   qdencn 13866
            ​*11.3.7  Analytic omniscience principles   trilpolemclim 13875
            11.3.8  Supremum and infimum   supfz 13907
            11.3.9  Circle constant   taupi 13909
      ​11.4  Mathbox for Mykola Mostovenko
      ​11.5  Mathbox for David A. Wheeler
            11.5.1  Testable propositions   dftest 13911
            ​*11.5.2  Allsome quantifier   walsi 13912