Index

  1. A
  2. B
  3. C
  4. D
  5. E
  6. F
  7. G
  8. H
  9. I
  10. J
  11. K
  12. L
  13. M
  14. N
  15. O
  16. P
  17. Q
  18. R
  19. S
  20. T
  21. U
  22. V
  23. W
  24. XY
  25. Z

A

  • A New Kind of Science
    • axiom systems in, 90, 105, 184
    • concept of truth in, 126
    • ruliology in, 197
    • search processes in, 198
    • writing of, 203
  • Abelian group theory
    • entailment cone of, 92
    • theorem distribution in, 110
  • Absorption law
  • Abstract algebra, 20
  • Abstraction
    • in mathematics, 195
  • Accumulative hypergraph systems, 49
  • Accumulative string systems, 45
  • Accumulative systems, 3944
    • and model theory, 102103
    • cosubstitution in, 60
    • definition of, 210
    • iconography for, 209
    • proofs in, 53
  • Activity
    • in metamathematical space, 149
  • Addition
    • from set theory, 171
  • Addition mod k, 97
  • Adjacency matrix
    • for accumulative evolution, 68
  • Agda, 216
  • AI ethics, 205
  • aleph0 (0) (aleph zero), 184
  • Algebra
    • abstract, 20
    • correspondence to geometry, 145
    • empirical metamathematics of, 177
    • proofs in, 179
    • universal, 92
  • Algebraic numbers, 199
  • Algebraic topology, 193
  • Aliens, 182183, 202
    • and the Continuum Hypothesis, 185
  • Analysis (mathematical)
    • empirical metamathematics of, 177
    • formalized theorems of, 168
  • And, 154
    • functional completeness and, 162
    • in combinators, 138
  • Angles
    • proposition about, 163
  • Approximations
    • models as, 100
  • Area of circle, 173, 175176
  • Arithmetic
    • encoding set theory in, 36
    • historical origin of, 191
  •     in Euclid’s Elements, 165
    • non-standard models of, 184
    • Peano axioms for, 94
    • representing by combinators, 134
    • universal computation in, 146
  • Arithmetic-geometric mean inequality, 173, 175176
  • Arithmetic series
  • Assembly language
    • and axioms, 134
    • for mathematics, 201
  • Associativity, 1920
    • in semigroups, 79
    • in string rewriting, 47
  •     of And and Or, 84, 87
  • Atomization
    • and motion, 145
  • Atoms of existence, 132, 140, 187
  •     see emes
  • Atoms of space, 8, 119, 144
    • as generated variables, 32
  • ATP
  •     see Automated theorem proving
  • Automated theorem proving, 5, 6977
    • for Boolean algebra, 87, 157
    • for Euclid, 166
    • for group theory, 82
    • in mainstream mathematics, 197
    • strategies in, 64
    • typical proofs from, 150
  • Automath, 216
  • Axiom
  • Axiom dependency
    • in geometry vs. Boolean algebra, 164
  • Axiom of Choice, 169, 177
  • Axiom of Extensionality, 169
  • Axiom of Infinity, 169
  • Axiom of Replacement, 169
  • Axiom schemas, 94
  • Axiom systems, 5
    • all possible, 129
    • and invention of mathematics, 181
    • development of, 213
    • disembodied, 182
    • for homotopy type theory, 194
    • historical origin of, 191
    • in the wild, 105112
    • model theory of, 97
    • possible for human mathematics, 184
  • Axiomatic level
    • definition of, 210
  • Axiomatic physics, 7
  • Axioms
    • at metamathematical Big Bang, 144
    • concept of math built on, 4
    • depth of, 176
    • equivalences as, 35
    • for homotopy type theory, 194
    • for mechanics, 191
    • going below, 131
    • icon for, 209
    • in Metamath system, 169
    • needed for Pythagorean theorem, 169
    • of Boolean algebra, 83
    • of Euclidean geometry, 90
    • of formalized math, 169
    • of group theory, 24, 79, 97
    • of present-day mathematics, 90
    • of semigroups, 78
    • vs. lemmas, 39

B

  • Babylonian mathematics, 191
  • Bertrand’s ballot problem, 173, 175176
  • Bertrand’s Postulate, 173, 175176
  • Bezout’s Theorem, 173, 175176
  • Bibliography, 213217
  • Big Bang
  • Binary operators
    • axioms for, 105
  • Binomial as number of subsets, 173, 175176
  • Binomial Theorem, 173, 175176
  • Birthday Problem probability, 173, 175176
  • Bisubstitution, 5964
    • and accumulative evolution, 67
    • definition of, 210
    • icon for, 209
  • Black holes, 151
    • metamathematical, 196
  • Blockchain technology, 205
  • Book 1 Proposition 1 (of Euclid), 166
  • Book 1 Proposition 5 (of Euclid), 163
  • Book 1 Proposition 47 (of Euclid), 167
  • Book 1 Proposition 48 (of Euclid), 164
  • Books
  •     in Euclid’s Elements, 165
  • Boolean algebra
    • empirical metamathematics of, 154163
    • entailment cone of, 83
    • minimal axioms for, 204
    • models of, 96
    • pattern of theorems in, 110
    • simplest axiom for, 87
    • textbook theorems of, 84, 87
  • Bound variables, 32
  • Bourbaki group, 214
  • Bracket abstraction, 133
  • Branchial graphs, 2628
    • analog in model theory of, 101
    • and entailment fabrics, 122
    • and metamathematical space, 66
    • coarsened for fields of math, 178
    • for Boolean algebra, 159, 161
    • for Euclid, 165
    • iconography for, 209
  • Branchial space, 26
    • definition of, 210
    • expansion of, 151
    • size of observers in, 118, 188
  • Branching
    • in automated theorem proving, 75
  • Bridges
    • between fields of mathematics, 147
  • Brownian motion, 6, 142
  • Bulk mathematics, 4, 6

C

  • Caching
    • and accumulative evolution, 50, 54
    • in automated theorem proving, 70
  • Canonical forms
    • and generated variables, 3234
    • of pattern expressions, 31
  • Canonicalization
    • of pattern variables, 37
  • Cantor’s Theorem, 173, 175176
  • Cardinality
    • of the ruliad, 185
  • Category theory, 145, 217
    • as expressing commonalities, 201
    • higher, 194
    • historical role of, 193
  • CauchySchwarz Inequality, 173, 175176
  • Causal graphs, 152, 206
    • in a gas, 187
    • spacetime, 119
  • Causal invariance, 75, 152
  • Cayley graphs, 24
  • CayleyHamilton Theorem, 173, 175176
  • Cellular automata, 203
  • Cellular automaton fluids, 206
  • Central groupoids, 110
  • Ceva’s Theorem, 173, 175176
  • CH (Continuum Hypothesis), 130
  • Chords
  • Church, Alonzo (USA, 19031995), 214
  • Cities
    • and metamathematical space, 154
  • Class 4 cellular automata, 137
  • Classical physics
    • source of, 188
  • Closed timelike curves, 27
  • Coarse-graining, 5, 8
    • and interestingness of theorems, 157
    • and observers, 130, 147
    • in metamathematics, 141
    • in proof space, 118
    • of proof graphs, 163
  • Code
    • computer and automated proofs, 150
  • Code vs. data, 39
  • Cognition
    • and mathematics, 129
  • Coherence
    • assumption of, 186
    • of mathematical observers, 146147
    • of observers, 9, 129
    • of theorems in Boolean algebra, 158
  • Collision events, 187
  • Colonization
    • of rulial space, 202
  • Combinators, 132140
    • and assembly language, 134
    • and machine code, 135
    • as example related to emes, 189
    • definitional distance for, 172
    • for arithmetic, 134
    • my work on, 206
    • representation of logic in, 137
  • Community
    • mathematical, 205
  • Commutative group theory
    • entailment cone of, 92
  • Commutative semigroups, 20
  • Commutativity, 19
  •     of Nand, 89
  • Compilation
    • of statements with quantifiers, 94
  • Completions, 206
  • Complex numbers
    • axioms for, 169
  • Complexity
    • in metamathematical structures, 44
  • Computation
    • concept of, 193
    • ruliad as all possible, 3
  • Computation universality
    • and trapping, 149
  • Computational boundedness
    • and truth, 128
  • Computational contracts, 205
  • Computational irreducibility, 4, 8, 142
    • and heat death of universe, 197
    • and metamathematical uniformity, 148
    • and proofs, 17
    • and Second Law, 6
    • and truth, 127
    • in ruliology, 197
  • Computational language, 198
  • Computational reducibility, 202
  • Computational universe
    • exploration of, 197
    • my work on, 203
  • Computationally bounded observers, 9
  • Condensation
    • of elements in semigroups, 23
  • Confluence
    • and proof space topology, 117
    • and theorem proving, 75
  • Consistency
    • in entailment fabrics, 123
  • Constants
    • and existential quantifiers, 93
  • Constitution
  • Contingent facts, 194
  • Continued fractions, 205
  • Continuum
    • and persistence of observers, 182
  • Continuum description, 142
  • Continuum Hypothesis (CH), 130
  • Contracts
    • computational, 205
  • Conventions
    • axioms as, 184
  • Coordinatization
    • of computation, 131
  • Coq, 216
  • Cosines
  • Cosubstitution, 5964
    • definition of, 210
    • icon for, 209
  • Cramer’s Rule, 173, 175176
  • Critical pair lemmas, 75, 206
  • Cross-linking
  •     in Euclid’s Elements, 165
  • CTCs (closed timelike curves), 27
  • Curry, Haskell B. (USA, 19001982), 214
  • Curvature
    • in metamathematical space, 149
  • Cut elimination, 5758, 75
    • in Euclid, 167
  • Cyclic groups, 97

D

  • D2 group, 24
  • De Moivre’s Theorem, 173, 175176
  • De Morgan’s law, 84, 87
  • Decidability
    • and black holes, 151
    • and metamathematical black holes, 196
  • Dedekind, J. W. Richard (Germany, 18311916), 213
  • Deductive reasoning
    • in physics, 7
  • Deduplication
    • of events, 41
  • Definitional distance, 172
  • Definitional lemmas, 174
  • Definitions
    • in formalized proofs, 170
  • Denumerability of rationals, 173, 175176
  • Dependencies
  • Depth
    • of reaching axioms, 176
  • Derangements Formula, 173, 175176
  • Desargues’s Theorem, 173, 175176
  • Destructive interference, 118
  • Det
    • definitional distance of, 172
  • Dirichlet’s Theorem, 173176
  • Discovery
    • of mathematics, 181
  • Divergence of harmonic series, 173, 175176
  • Divergence of inverse prime series, 173, 175176
  • Divisibility by 3 Rule, 173, 175176
  • Double negation
  • Droplets
    • and elements of semigroups, 2324
  • Dualities
    • in mathematics, 145

E

  • e
  • Earth
    • geography of, 154
  • Eigenvalues
    • definitional distance of, 172
  • Elegant proofs, 150
  • Elementary length, 188
  • Elementary time, 188
  • Elements
  • Emes (atoms of existence), 132, 140
    • as underneath axioms, 185
    • definition of, 210
    • number for physics and math, 187190
    • representations in terms of, 147
  • Emic space, 142
  • Empirical metamathematics, 154180
    • my work on, 206
    • simple example of, 65
  • Energy
    • metamathematical analog of, 28, 149
  • Entailment
    • in accumulative systems, 53
    • rule of, 140
  • Entailment cones, 28
    • and automated theorem proving, 69
    • and falsity, 124
    • and incompleteness, 125
    • and inconsistency, 125
    • and light cones, 148
    • and model theory, 102
    • and Wolfram|Alpha output, 200
    • appearance of logic theorems in, 84
    • definition of, 210
    • for arbitrary axiom systems, 106
    • for axiom schemas, 95
    • for Boolean algebra, 156
    • for Wolfram axiom, 88
    • growth of, 89
    • knitting of, 121
  • Entailment fabrics, 101, 119123
    • and gravity, 148
    • and possible mathematics, 129
    • and truth, 127
    • definition of, 210
    • expansion of, 200
    • in arbitrary axiom systems, 108
  • Entailment graph
    • definition of, 210
    • iconography for, 209
  • Entailments
    • bisubstitution and, 64
  • Entanglement
    • and branchial space, 26
  • Enumeration
    • of axiom systems, 105
  • Equal, 12
    • and two-way rules, 35
  • Equality
    • in models, 99
  • Equality predicates
    • emulation of, 146
  • Equilateral triangle
    • formal construction of, 91
  • Equivalence classes
    • and types, 140
  • Equivalences
    • as two-way rules, 35
    • in models, 99
    • in multiway systems, 31
    • in semigroups, 2124
    • mathematical, 147
    • of expressions, 1317
    • of variables, 30
  • Equivalential calculus, 110
  • ErdősSzekeres Theorem, 173, 175176
  • Ethics
  • Euclid (?Egypt, ~300 BC), 213
    • and formalization, 4
  • Euclid’s axioms, 90
  • Euclid’s Elements, 163
  • Euclid’s GCD algorithm, 173, 175176
  • Euler’s Partition Theorem, 173, 175176
  • Euclidean geometry
    • and choice of axioms, 186
    • as idealization of physics, 182
    • in the Wolfram Language, 205
  • Event horizons, 151
    • metamathematical, 118
  • Excluded middle
  • Exhaustive search
    • and entailment cones, 72
  • Existence
    • atoms of, 132, 140
    • of mathematics and physics, 183
  • Existential quantifiers, 9293
  • Expansion
    • of metamathematical space, 196
    • of universe, 151, 196
  • Experience
    • as basis for mathematics, 182
  • Experimental mathematics, 200
    • my use of, 203
  • Experimental validation
    • through empirical metamathematics, 154
  • Experiments
    • as analog of theorems, 7
  • Explosion
    • Principle of, 124
  • Expression code, 98
  • Expression rewriting, 131
    • definition of, 210
  • Expressions
    • similarity of, 28
    • transformations of, 59
  • Extensionality, 147, 169
    • in homotopy type theory, 194

F

  • Fabric
    • entailment, 119
  • Falsifiability
    • and empirical metamathematics, 154
  • Falsity, 124128
    • and white holes, 151
    • in combinators, 137
  • Fermat’s Little Theorem, 173, 175176
  • Fields of mathematics, 105, 177
  • FindEquationalProof, 69, 72, 198, 205
  • Finite groups
    • as models of group theory, 97
  • Finite models, 96104
  • Fishing out of ruliad, 137, 139
  • Fixed points
    • for combinators, 140
  • Fluid-level mathematics
    • and metamathematical space, 150
    • and raw ruliad, 136, 141
  • Fluid mechanics
  • Fluids
    • cellular automaton, 206
  • Foliations
    • and metamathematical space, 29
  • Formal processes
    • ruliad as representing, 3
  • Formalized mathematics, 168, 216
  • Formulas
    • of Boolean algebra, 154
  • Four-Squares Theorem, 173, 175176
  • Fourier series
  • Fractal
    • as game graph, 116
  • Freeways
    • for proofs, 149
    • in connections between fields, 179
  • Frege, F. L. Gottlob (Germany, 18481925), 191, 213
  • Friendship Graph Theorem, 173, 175176
  • FullSimplify, 205
  • Function application
    • and combinators, 132
  • Functionally complete sets
    • in Boolean algebra, 162
  • Fundamental laws of mathematics, 35
  • Fundamental Theorem of Algebra, 173, 175176
  • Fundamental Theorem of Arithmetic, 173, 175176
  • Fundamental Theorem of Calculus, 173, 175177
  • Future
    • of universe, 151

G

  • Game graph
    • for Towers of Hanoi, 115
  • Gas, 5
    • collision count in, 187
    • of mathematical statements, 8
    • of semigroup words, 23
    • reactions in mathematical, 43
  • Gas laws
    • emergence of, 9
  • GCD algorithm, 173, 175176
  • GCD (greatest common divisor)
    • from set theory, 171
  • Generated variables, 3134
    • and rules applied to rules, 37
    • in raw ruliad, 139
  • Generators
  • Geodesics
    • and shortest proofs, 28
    • on entailment fabrics, 148
  • Geography
    • metamathematical, 154
  • GeometricScene, 91
  • Geometric series
  • Geometry
    • and higher category theory, 194
    • axioms for, 90
    • correspondence to algebra, 145
    • empirical metamathematics of, 163, 177
    • formalized theorems of, 168
    • Greek, 191
    • historical origin of, 191
    • of metamathematical space, 148
    • theorems in Euclidean, 164
  • Goats
    • counting of, 191
  • Gödel’s Theorem, 127, 184, 192
    • and truth, 125
    • proof of using rule 110
  • Graphical key, 209
  • Gravity
    • in metamathematical space, 28, 148
  • Greek mathematics, 191
  • Group theory
    • entailment cone of, 7982
    • models of, 97
    • textbook theorems of, 82
    • theorem distribution in, 110
  • Groupoids
  • Groups, 24

H

  • Hanoi
    • Towers of, 115
  • Harmonic series
  • Hash codes
    • and model theory, 102
  • Head
    • in an expression, 12
  • Head matching, 36
  • Heat death of universe, 197
  • Higher-level description, 10
    • vs. ruliad, 137
  • Highways
    • in connections between fields, 179
  • Hilbert, David (Germany, 18621943), 192, 213
  • Hilbert’s Program, 184, 192
  • History
  • Holes
    • in proof space, 115
  • Homogeneity
    • of metamathematical space, 144
  • Homology
    • in proof space, 115
  • Homotopy type theory, 147, 194, 216
  • Human experience
    • and observers, 3
  • Human language
    • as model for math, 139
  • Human-level mathematics, 6, 10, 44, 123, 130, 182, 193
    • and automated theorem proving, 77
  • Human mind
    • and mathematics, 192
  • Human scale, 188
  • Humans
    • as source of mathematics, 181
  • Hypercubes
    • and commutativity, 19
  • Hypergraph rewriting
    • accumulative, 49
    • and expressions, 131
    • model theory for, 104
  • Hypergraphs
    • and generated variables, 32, 139
    • counting of, 188
  • Hyperruliad, 185
  • Hypersonic flow, 6, 142
  • Hypersurfaces
    • metamathematical, 148
    • spacelike, 149
  • Hypothesis
    • icon for, 209

I

  • Icons
    • in this book, 209
  • Ideal forms, 194
    • and the ruliad, 191
  • Idealizations
    • of mathematics, 12
  • Idempotence
  •     of And and Or, 84
  • Identity
  • Implicational calculus, 110
  • Implies
    • functional completeness and, 162
    • in combinators, 138
  • Inclusion/Exclusion
  • Incompleteness
    • in rewriting systems, 125
  • Incompleteness Theorems, 127
  • Inconsistency
    • and white holes, 151
    • in rewriting systems, 125
  • Independence
    • from axioms, 130
    • of Continuum Hypothesis, 184
  • Induction (mathematical), 173, 175176
    • in axioms of arithmetic, 94
    • in Peano axioms, 94
  • Inductive inference
    • limits of, 188
  • Inference
    • laws of, 8
  • Infinitude of primes, 173, 175176
  • Infinity
    • axiom of, 169
    • definitional distance of, 172
  • Instruction set
    • for mathematics, 201
  • Integers
    • combinator representation of, 134
  • Interesting theorems
    • of Boolean algebra, 156
  • Interference
    • in proof space, 118
  • Intermediate expressions
    • in proofs, 70
    • size of, 17
  • Intermediate lemmas
  • Intermediate steps
  • Intermediate Value Theorem, 173, 175176
  • Interpretability
    • of combinator expressions, 138
  • Intuition
    • about physical vs. metamathematical space, 145
    • in mathematics, 193
  • Inventions
    • of mathematics, 181
  • Irrationality of  , 173, 175176
  • Island
    • of computational reducibility, 202
  • Isomorphism
    • in hypergraphs, 49
  • Isosceles triangle
    • proposition about, 163
  • Isosceles Triangle Theorem, 173, 175176

J

  • Junctional calculus, 110

K

  • K-theory, 199
  • Klein four-group, 24
  • Knitting
    • of entailment cones, 121
  • Knowledge
  • Königsberg bridge theorem, 173, 175176

L

  • L’Hôpital’s Rule, 173, 175176
  • Lagrange’s Theorem, 173, 175176
  • Languages (abstract)
    • for understandable mathematics, 198
  • Law of Cosines, 173, 175176
  • Law of double negation, 84, 87, 162
  • Law of excluded middle, 8485, 87
  • Law of noncontradiction, 84, 87
  • Law of Quadratic Reciprocity, 173, 175176
  • Laws of inference, 8
    • and bisubstitution, 64
  • Laws of mathematics, 35, 196
  • Laws of physics
    • alien, 202
    • from ruliad, 3
  • Lean, 216
  • Lebesgue Integration Theorem, 173, 175176
  • Leibniz’s series for π, 173, 175176
  • Lemmas
    • and accumulative systems, 53
    • definitional, 174
    • in theorem proving, 70
    • to prove lemmas, 39
  • Length
    • elementary, 188
  • Lengths of proofs, 17
  • Light cones
    • and entailment cones, 28, 148
    • in physics vs. mathematics, 119
  • Limits
    • to mathematics, 197
  • Liouville’s Theorem, 173, 175176
  • Log (logarithm)
    • definitional distance of, 172
  • Logic
    • construction of mathematics from, 192
    • empirical metamathematics of, 154163
    • entailment cone of, 83
    • in combinators, 137138
    • textbook theorems of, 84, 87
  • Loop
    • in multiway graph, 20

M

  • Machine code
    • and automated proofs, 150
    • and axioms, 134
    • for physics, 8
    • formal proofs as, 198
    • logic as in WhiteheadRussell, 192
    • of ruliad, 131
  • Macro expansion, 170
  • Matching
    • and generated variables, 32
    • metamathematical, 36
    • of expression patterns, 13
  • Mathematica, 12, 215
    • as practical source of mathematics, 190
    • as tool of forward computation, 198
    • computational language in, 198
    • release of, 203
  • Mathematical Big Bang, 43
  • Mathematical expressions
    • space of, 26
  • Mathematical knowledge
    • and empirical metamathematics, 154163
    • and entailment fabrics, 123
    • curation of, 205
  • Mathematical logic
    • and my work, 204
    • historical role of, 193
    • personal study of, 203
    • syntax in, 36
  • Mathematical observers, 3, 9, 113
    • and combinators, 139
    • and human minds, 192
    • and model theory, 102
    • and notable theorems, 177
    • and truth, 127
    • definition of, 211
    • future of, 201
    • size of, 142
  • Mathematicians
    • as observers, 4
    • lack of interest in formalization of, 205
    • metamodel of, 142, 147
    • theorems pondered per day, 190
    • workflow of, 193
  • Mathematics
    • all possible, 129
    • analog of fluid dynamics to, 6
    • arbitrariness of, 129
    • as use case of the Wolfram Language, 203
    • assembly language for, 201
    • axioms in, 112
    • dualities in, 145
    • emergence from ruliad of, 136
    • existence of, 206
    • experiments in, 200
    • fields of, 177
    • from metamathematics, 25
    • future of, 196
    • general laws of, 11, 12
    • historical content of, 154180
    • human-level, 6, 10, 184
    • human natural language of, 12
    • invention vs. discovery of, 181
    • large-scale structure of, 196
    • literature of, 4
    • molecular-level, 56, 10
    • of aliens, 202
    • ruliad as all possible, 3, 9
    • size of in emes, 187
    • standard axioms of, 90, 184
  • Maximum metamathematical speed, 28
  • Mean Value Theorem, 173, 175176
  • Meaning
    • of mathematics, 192
    • of structure in the ruliad, 134
  • Measurement
    • limits of, 189
  • Mechanics
    • mathematicization of, 191
  • Memory usage
    • for automated theorem proving, 70
  • Merging
    • and patterns, 31
  • Metalogic, 140
  • Metamathematical singularities, 151, 196
  • Metamathematical space, 2629, 65
    • and model theory, 101
    • coarse-graining in, 141
    • curvature of, 149
    • definition of, 211
    • expansion of, 151
    • extent of observers in, 147
    • geography of, 154
    • geometry of, 148, 151
    • maximum speed in, 152
    • notable theorems in, 178
    • position of fields in, 177
    • settlements in, 154
    • space probe in, 202
    • uniformity of, 144
  • Metamathematical space travel, 202
  • Metamathematical speed, 152
  • Metamathematical time dilation, 152
  • Metamathematics (formalized math system), 168, 177, 208
  • Metamodeling
    • of axiomatic math, 12
    • of mathematics, 139
  • Microscopes, 201
    • metamathematical, 118
  • Middle Ages, 124
  • Mind
  • Mizar, 216
  • Model theory, 96104
    • and reference frames, 102
    • and string systems, 104
    • for axioms in the wild, 112
    • guessing theorems from, 73
  • Modus ponens, 169
  • Molecular dynamics, 187
    • analogy to axiomatic math, 56
  • Molecular-level mathematics, 56, 810, 118
    • and automated theorem proving, 77
  • Monoid theory
    • entailment cone of, 92
  • Motion
    • concept of, 11
    • in metamathematical space, 28
    • metamathematical, 145
    • of mathematical observer, 150
    • physical, 144
  • Multicomputational paradigm, 146, 206
  • Multiplication
    • in semigroups, 24
  • Multiplication tables, 96
  • Multiway graphs, 13
    • definition of, 211
    • effective formed from token-event graph, 66
    • mathematical interpretations of, 1925
    • vs. token-event graphs, 39
  • Multiway systems
    • as models of mathematics, 204
  •     in A New Kind of Science, 203

N

  • Named theorems
    • of Boolean algebra, 156
  • Names
    • of emes, 140
    • of generated variables, 31
    • of pattern variables, 37
  • Nand, 87
    • formalized definition of, 170
    • functional completeness and, 162
    • in combinators, 138
    • models giving, 97
  • Natural language, 12
    • vs. computational language, 198
  • Natural math understanding, 200
  • Negation, 125
    • law of double, 84, 87
  • Nested pattern
    • as game graph, 116
  • Non-constructive proofs, 191
  • Noncontradiction law, 8485, 87
  • Non-denumerability of continuum, 173, 175176
  • Non-Euclidean geometry
    • and abstraction in math, 191
  • Nor
    • functional completeness and, 162
    • models giving, 97
  • Not, 154
    • functional completeness and, 162
  • Notable theorems, 157
  • Notebooks
    • for this book, 208
  • Number theory
    • empirical metamathematics of, 177
    • proofs in, 179

O

  • Objects
    • coherence of, 11
  • Observers
    • and combinators, 139
    • and emergence of mathematics, 136
    • and entailment fabrics, 123
    • and heat death of universe, 197
    • and history of mathematics, 194
    • and model theory, 102
    • conflating in proof space, 118
    • constraints of, 181
    • mathematical, 3, 9, 113
    • persistence of, 144, 182
    • physical, 3, 9
    • relation between physical and mathematical, 182
    • size in metamathematical space, 118
  • Open-ended questions, 151
  • Operator patterns, 59
  • Operator systems, 210
  • Operators
    • compilation to emes of, 189
    • going below, 131
    • in Boolean algebra, 162
    • matching of, 36
    • models of, 96104
  • Or, 154
    • functional completeness and, 162
    • in combinators, 138
  • Ornamentation
    • in theorems, 157

P

  • Parallel transport
    • in metamathematics, 152
  • Paramathematics, 202
    • definition of, 211
  • Paramodulation, 64
  • Parsing
    • of ruliad, 183
  • Particles
    • analog in math of, 139
    • and notable theorems, 174
    • identification of, 136
  • Paths
    • in accumulative systems, 53
    • in multiway systems, 113
  • Pattern expression
    • definition of, 211
  • Pattern variables, 30
  • Patterns
    • and accumulative evolution, 41
    • applied to patterns, 5964
  • Peano Arithmetic, 94, 146, 184
  • Peano, Giuseppe (Italy, 18581932), 213
  • Pell equation, 173, 175176
  • Perception
    • and definition of mathematics, 195
    • and invention of mathematics, 181
  • Perfect Number Theorem, 173, 175176
  • Persistence
  • Philosophy
    • historical view of math by, 191
  • Phonemes
    • as name analog of emes, 140
  • Physical observers, 3, 9
  • Physicalized laws of mathematics, 145, 148
  • Physics
    • analog to mathematics of, 141
    • axiomatic, 7
    • perception of as real, 182
    • ruliad as representing, 3
  • Physics Project, 3
    • and causal invariance, 75
    • branchial space in, 26
    • generated variables in, 32
    • hypergraph rewriting in, 50
  • Pi (π)
    • definitional distance of, 172
  • Plato (Greece, 427347 BC), 191, 194, 206, 213
  • Platonic view
  • Plus
    • from set theory, 171
  • Polynomial Factor Theorem, 173, 175176
  • Post, Emil L. (USA, 18971954), 215
  • Powers
    • combinator representation of, 135
  • PrimePi
    • definitional distance of, 172
  • PrimeQ
    • as function involving proofs, 198
  • Primes 4k + 1 are sums of 2 squares, 173, 175176
  • Principia Mathematica (of Whitehead and Russell)
    • and foundations of math, 192
  • Principle of Computational Equivalence, 17, 44
    • and incompleteness, 127
    • and motion, 146
  • Principle of Explosion, 124
  • Principle of Inclusion/Exclusion, 173, 175176
  • Progress
    • in mathematics, 119
  • Proof assistants, 199
  • Proof cone, 211
  •     see entailment cone
  • Proof graphs, 5558, 71
    • definition of, 211
    • for Euclid, 163
  • Proof path
    • and metamathematical motion, 28
  • Proof space, 113
  • Proof-to-proof transformations, 75
  • Proofs
    • all possible, 114
    • as exposition of ideas, 197
    • as narrative explanations, 77, 193
    • as path in graph, 1416
    • by automated theorem proving, 6977
    • density of, 149
    • elegant, 150
    • event horizons for, 151
    • hand-constructed, 168
    • in accumulative systems, 53
    • in geometry, 91
    • in Wolfram|Alpha, 205
    • lengths of, 17
    • non-constructive, 191
    • of law of double negation, 162
    • of law of excluded middle, 85
    • of noncontradiction, 85
    • of textbook theorems in logic, 87
    • shortest, 148
    • size in emes of, 189
    • space of, 113
    • transformations between, 75
    • verification with, 199
    • vs. models, 100
  • Propositional logic
    • empirical metamathematics of, 154163
    • entailment cone of, 83
  • Pure mathematics
    • in the Wolfram Language, 199, 205
  • Puzzle
    • Towers of Hanoi, 115
  • pythag (formalization of Pythagorean theorem), 172
  • Pythagorean theorem, 10, 147, 174
    • compilation to emes of, 189
    • dependence on axioms of, 169
    • formalized dependency graph, 168
    • formalized version of, 170
    • in terms of emes, 142
    • multiple definitions of, 172
    • variants of, 130
  • Pythagorean triples, 173, 175176
  • pythi (formalization of Pythagorean theorem), 172

Q

  • Quartic equations, 173, 175176
  • Quantifiers, 93
  • Quantum effects
    • in metamathematics, 118
  • Quantum histories
    • and branchial space, 26
  • Quantum mechanics
    • and counting emes, 188
    • and multiway systems, 205
    • in mathematics, 11
  • Quaternions
    • and abstraction in math, 191
    • as example of abstraction, 184, 191
  • Quine, Willard Van Orman (USA, 19082000), 214

R

  • Ramsey’s Theorem, 173176
  • Real numbers, 6
    • and Continuum Hypothesis, 184
    • axioms for, 147, 169
  • Reality
    • physical, 5
  • Reduce
    • as function involving proofs, 198
  • Reducibility
    • computational, 202
  • Reductionism
    • in modeling mathematics, 139
  • Reference frames
    • and models, 102
    • for Boolean algebra, 161
    • in the ruliad, 910
    • metamathematical, 29, 148
  • Relativity
    • and theorem proving, 75
    • in mathematics, 11
    • metamathematical, 151152
  • Replacement Axiom, 169
  • Replacements
    • in expressions, 59
  • Representations
    • of mathematical statements, 12
  • Representation theory, 97
  • Rest frames, 29
  • Reverse mathematics, 201
  • Rewriting
    • accumulative of strings, 45
    • of expressions, 59, 131
  • Rigidity
    • of observers in metamathematical space, 147
  • Rigor in mathematics, 191
  • Ring theory
    • entailment cone of, 92
  • RISC instruction sets, 201
  • Routing
    • of proofs, 149
  • Rule of entailment, 140
  • Rules
    • applied to rules, 3538
    • in the Wolfram Language, 13
  • Ruliad, 35, 9
    • and bridges between fields, 147
    • and comparison with human axiom systems, 112
    • and entailment fabrics, 122
    • and going below axioms, 131
    • and higher category theory, 194
    • and hypergraph rewriting, 50
    • and possible mathematics, 129
    • and truth, 127128
    • as container of all computation, 193
    • as source of mathematics, 181
    • as underlying reality, 187
    • cardinality of, 185
    • connectivity of, 150
    • definition of, 211
    • definitional distance in, 172
    • entailments and, 64
    • inevitability of, 4
    • made of emes, 140
    • possible samplings of, 185
  • Rulial multiway system, 206
  • Rulial space, 9
    • definition of, 211
    • size in, 188
  • Ruliology, 197
    • for inequivalent axiom systems, 190
    • of axiom systems, 105112
  • Russell, Bertrand A. W. (England, 18721970), 191, 213

S

  • S, K combinators, 132140
  • SatisfiableQ
    • as function involving proofs, 198
  • Schemas (axiom), 94
  • Schönfinkel, Moses I. (Germany/Russia, 1889 ~1942), 215
  • SchröderBernstein Theorem, 173176
  • Second Law of thermodynamics, 6, 206
    • and higher-level descriptions, 142
    • and observers, 130
  • Secret weapon, 203
  • Semigroup theory, 78
    • theorem distribution in, 110
  • Semigroups
    • commutative, 20
    • theorems about, 21
  • Semiring theory
    • entailment cone of, 92
  • Set theory, 146
    • and everyday experience, 184
    • as foundation for math, 193
  •     definition of Plus in, 171
    • empirical metamathematics of, 177
    • encoding in arithmetic, 36
    • independence of CH in, 130
  • set.mm, 168, 177
  • Settlements
    • in metamathematical space, 154
  • Shortest proofs, 18, 28, 69
  • Shredding (of observers), 6, 10, 142, 150, 182, 185
    • definition of, 211
  • Sierpiński triangle
    • as game graph, 116
  • Similar expressions, 28
  • Simultaneity
    • in metamathematics, 148
  • Simultaneity surfaces, 29
  • Singularities
    • metamathematical, 196
    • spacetime, 130
  • Singularity theorems, 151
  • Sinh
    • definitional distance of, 172
  • Skolemization, 94
  • Slice
    • of entailment cone, 148
  • Smart contracts, 205
  • SMP
  •     see Symbolic Manipulation Program
  • Sorting
    • of two-way rules, 35
  • Space
    • and mathematical observers, 142
    • atoms of, 8
    • continuity of, 188
    • instantaneous state of, 119
    • perception of, 130, 182
  • Spacecraft
  • Spacelike hypersurfaces, 29, 149
  • Spacetime
    • metamathematical analog of, 28
  • Spacetime singularities, 130
  • Specialties
    • in mathematics, 177
  • Speed of light, 152
    • metamathematical analog of, 28
  • Statements
    • of Boolean algebra, 155
    • icon for, 209
    • mathematical, 12
  • Statistical mechanics
    • and heat death of universe, 197
  • Stirling’s Formula, 173, 175176
  • Straight-line proofs, 76
  • String rewriting
    • and entailment fabrics, 120
    • negation in, 125
  • String systems
    • accumulative, 45
  • Strings
    • models for, 104
    • vs. trees, 47
  • Subaxiomatic mathematics, 131
  • Subsets of a set, 173, 175176
  • Substitution Axiom, 169
  • Substitutions
    • and two-way rules, 36
    • definition of, 212
    • icon for, 209
    • in expression trees, 16
    • in Metamath system, 170
  • Sum of kth powers, 173, 175176
  • Sylow’s Theorem, 173, 175176
  • Symbolic discourse language, 205
  • Symbolic expressions, 12
    • and rules applied to rules, 36
    • as code and data, 39
    • personal use of, 203
  • Symbolic language, 8
  • Symbolic Manipulation Program (SMP), 203, 215
  • Syntactic rules
    • in mathematical logic, 36

T

  • Tag systems, 215
  • Tally marks, 191
  • Tautologies
    • and automated theorem proving, 71
    • and concept of truth, 125
  • Taylor’s Theorem, 173, 175176
  • Telescopes, 201
  • Term rewriting
    • entailment in, 64
  • Textbooks
    • of logic, 156
  • Theorem dependency graph
    • for Euclid, 163
  • Theorem proving
  • Theorems
    • about semigroups, 79
    • curation of, 205
    • equivalences as, 35
    • from accumulative evolution, 43
    • icon for, 209
    • in history of mathematics, 154
    • in literature, 4
    • notable, 173179
    • number of in entailment cones, 189
    • number of published, 4
    • of Boolean algebra, 155
    • of Euclid, 164
    • of group theory, 82
    • of logic, 84, 87, 155
    • to prove theorems, 39
    • up to complexity bound, 160
  • Threads
  • Tilings
    • as analogy for entailment fabrics, 122
  • Time
    • elementary, 188
    • in metamathematics, 119
    • perception of continuous, 182
  • Time dilation, 152
  • Token-event graphs, 39
    • and automated theorem proving, 70
    • and metamathematical phenomenology, 65
    • and proof graphs, 55
    • definition of, 212
    • for Boolean algebra, 157
    • for hypergraph rewriting, 52
    • for semigroup theory, 78
    • iconography for, 209
    • with cosubstitution, 59
  • Topology
    • empirical metamathematics of, 177
    • formalized theorems of, 168
    • of proof space, 113
  • Towers of Hanoi, 115
  • Transcendentality
  • Transformations
    • of expressions, 13, 59
    • personal use of, 203
  • Transitivity of equality, 147
  • Translation
    • in metamathematical space, 146
    • metamathematical and time dilation, 152
  • Translation distance
    • metamathematical, 152
  • Transversals, 29
    • and entailment fabrics, 122
    • of entailment cone, 148
  • Tree rewriting, 131
  • Tree-structured expressions, 12, 1617
    • and accumulative evolution, 42
    • in metamathematical space, 66
    • space of, 28
  • Trees
    • vs. strings, 47
  • Triangle
  • Triangle Inequality, 173, 175176
  • Triangular-number reciprocals, 173, 175176
  • Truth, 124128
    • in combinators, 137
  • Two-way hypergraph rewriting, 50
  • Two-way rules, 35
    • accumulative evolution with, 3941
    • definition of, 212
  • Type theory, 140, 194
    • homotopy, 147

U

  • Unbounded growth
    • in accumulative string systems, 48
  • Undecidability
    • and accumulative proof lengths, 58
    • and lower-level math, 130
    • in mainstream mathematics, 193
    • in mathematics, 204
    • of consistency, 129
    • of proof paths, 150
    • rarity of in mathematics, 150
  • Unification
    • of patterns, 59, 64
  • Uniformity
    • of metamathematical space, 144
  • Uniqueness
  • Uniquification
    • and generated variables, 3234
    • definition of, 212
  • Univalence axiom, 147, 194
  • Universal algebra, 92, 214
  • Universal quantifiers, 92
  • Universality (computational), 131
    • and motion, 146
  • Universe
    • as made of generated variables, 32
    • existence of, 206
    • future of, 151
    • number of emes in, 189
    • rule for, 9
    • size of in emes, 187
  • Unrolling
    • of proofs, 75
    • proofs in Euclid, 167
  • Ur level, 131

V

  • Value of ζ (2), 173, 175176
  • Variables, 12
    • compilation to emes of, 189
    • generated, 30
    • going below, 131
    • matching inside, 37
  • Verification
    • with proofs, 199
  • Vortices
    • as analogy to math structure, 6, 136

W

  • Whitehead, Alfred N. (England/USA, 18611947), 191, 213
  • White holes
    • and falsity, 151
  • Wilson’s Theorem, 173, 175176
  • Wolfram|Alpha, 200
    • step-by-step computations in, 205
  • Wolfram axiom (for logic), 87, 198, 204, 208
    • models of, 96
  • Wolfram Language, 12
    • and automated theorem proving, 69
    • as computational language, 198
    • as symbolic language, 8
    • as tool for this book, 208
    • bisubstitution and, 64
    • count of expressions evaluated in, 190
    • pattern heads in, 94
    • precursor of, 203
    • primitives in, 199
    • structure of patterns in, 37
    • translation from natural math to, 200
  • Wolfram Physics Project, 3, 205
  • Words
    • in languages, 12
    • in semigroups, 22
  • Workflows
    • for mathematics, 199

XY

  • Xor
    • functional completeness and, 162
    •  
       
    •  
       

Z

  • Zermelo, Ernst F. F. (Germany, 18711953), 213
  • ZermeloFraenkel set theory
  •     see ZFC set theory
  • Zeta
    • definitional distance of, 172
  • ZFC set theory, 146
    • as axiom system for math, 201
    • in empirical metamathematics, 168