Index

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
  • of logic, 84, 87
• Abstract algebra, 20
• Abstraction
  • in mathematics, 195
• Accumulative hypergraph systems, 49
• Accumulative string systems, 45
• Accumulative systems, 39–44
  • and model theory, 102–103
  • 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
• aleph₀ (ℵ₀) (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, 182–183, 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, 175–176
• 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, 175–176
• Arithmetic series
  • sum of, 173, 175–176
• Assembly language
  • and axioms, 134
  • for mathematics, 201
• Associativity, 19–20
  • 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, 69–77
  • 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
  • associativity, 19–20
  • commutativity, 19
• 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, 105–112
  • 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, 175–176
• Bertrand’s Postulate, 173, 175–176
• Bezout’s Theorem, 173, 175–176
• Bibliography, 213–217
• Big Bang
  • in physical universe, 144
  • mathematical, 43, 119, 144
• Binary operators
  • axioms for, 105
• Binomial as number of subsets, 173, 175–176
• Binomial Theorem, 173, 175–176
• Birthday Problem probability, 173, 175–176
• Bisubstitution, 59–64
  • 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, 154–163
  • 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, 26–28
  • 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, 32–34
  • of pattern expressions, 31
• Canonicalization
  • of pattern variables, 37
• Cantor’s Theorem, 173, 175–176
• Cardinality
  • of the ruliad, 185
• Category theory, 145, 217
  • as expressing commonalities, 201
  • higher, 194
  • historical role of, 193
• Cauchy–Schwarz Inequality, 173, 175–176
• Causal graphs, 152, 206
  • in a gas, 187
  • spacetime, 119
• Causal invariance, 75, 152
• Cayley graphs, 24
• Cayley–Hamilton Theorem, 173, 175–176
• Cellular automata, 203
  • class 4, 137
• Cellular automaton fluids, 206
• Central groupoids, 110
• Ceva’s Theorem, 173, 175–176
• CH (Continuum Hypothesis), 130
• Chords
  • product of segments of, 173, 175–176
• Church, Alonzo (USA, 1903–1995), 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, 146–147
  • of observers, 9, 129
  • of theorems in Boolean algebra, 158
• Collision events, 187
• Colonization
  • of rulial space, 202
• Combinators, 132–140
  • 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
  • AI, 205
• 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
  • law of, 173, 175–176
• Cosubstitution, 59–64
  • definition of, 210
  • icon for, 209
• Cramer’s Rule, 173, 175–176
• Critical pair lemmas, 75, 206
• Cross-linking
•     in Euclid’s Elements, 165
• CTCs (closed timelike curves), 27
  • solution of, 173, 175–176
• Curry, Haskell B. (USA, 1900–1982), 214
• Curvature
  • in metamathematical space, 149
• Cut elimination, 57–58, 75
  • in Euclid, 167
• Cyclic groups, 97

D

• D₂ group, 24
• De Moivre’s Theorem, 173, 175–176
• De Morgan’s law, 84, 87
• Decidability
  • and black holes, 151
  • and metamathematical black holes, 196
• Dedekind, J. W. Richard (Germany, 1831–1916), 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, 175–176
• Dependencies
  • causal, 153
• Depth
  • of reaching axioms, 176
• Derangements Formula, 173, 175–176
• Desargues’s Theorem, 173, 175–176
• Destructive interference, 118
• Det
  • definitional distance of, 172
• Dirichlet’s Theorem, 173–176
• Discovery
  • of mathematics, 181
• Divergence of harmonic series, 173, 175–176
• Divergence of inverse prime series, 173, 175–176
• Divisibility by 3 Rule, 173, 175–176
• Double negation
  • law of, 162
• Droplets
  • and elements of semigroups, 23–24
• Dualities
  • in mathematics, 145

E

• e
  • transcendentality of, 173, 175–176
• Earth
  • geography of, 154
• Eigenvalues
  • definitional distance of, 172
• Elegant proofs, 150
• Elementary length, 188
• Elementary time, 188
• Elements
  • Euclid’s, 91, 163
  • in semigroups, 22, 24–25
• Emes (atoms of existence), 132, 140
  • as underneath axioms, 185
  • definition of, 210
  • number for physics and math, 187–190
  • representations in terms of, 147
• Emic space, 142
• Empirical metamathematics, 154–180
  • 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, 119–123
  • 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, 21–24
  • mathematical, 147
  • of expressions, 13–17
  • of variables, 30
• Equivalential calculus, 110
• Erdős–Szekeres Theorem, 173, 175–176
• Ethics
  • AI, 205
• Euclid (?Egypt, ~300 BC), 213
  • and formalization, 4
• Euclid’s axioms, 90
• Euclid’s Elements, 163
• Euclid’s GCD algorithm, 173, 175–176
• Euler’s Partition Theorem, 173, 175–176
• Euclidean geometry
  • and choice of axioms, 186
  • as idealization of physics, 182
  • in the Wolfram Language, 205
• Event horizons, 151
  • metamathematical, 118
• Excluded middle
  • law of, 84–85, 87
• Exhaustive search
  • and entailment cones, 72
• Existence
  • atoms of, 132, 140
  • of mathematics and physics, 183
• Existential quantifiers, 92–93
• 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, 124–128
  • and white holes, 151
  • in combinators, 137
• Fermat’s Little Theorem, 173, 175–176
• Fields of mathematics, 105, 177
• FindEquationalProof, 69, 72, 198, 205
• Finite groups
  • as models of group theory, 97
• Finite models, 96–104
• 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
  • analogy to math, 5–6
• 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, 175–176
• Fourier series
  • convergence of, 173, 175–176
• Fractal
  • as game graph, 116
• Freeways
  • for proofs, 149
  • in connections between fields, 179
• Frege, F. L. Gottlob (Germany, 1848–1925), 191, 213
• Friendship Graph Theorem, 173, 175–176
• FullSimplify, 205
• Function application
  • and combinators, 132
• Functionally complete sets
  • in Boolean algebra, 162
• Fundamental laws of mathematics, 3–5
• Fundamental Theorem of Algebra, 173, 175–176
• Fundamental Theorem of Arithmetic, 173, 175–176
• Fundamental Theorem of Calculus, 173, 175–177
• 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, 175–176
• GCD (greatest common divisor)
  • from set theory, 171
• Generated variables, 31–34
  • and rules applied to rules, 37
  • in raw ruliad, 139
• Generators
  • of groups, 24
  • of semigroups, 21–24
• Geodesics
  • and shortest proofs, 28
  • on entailment fabrics, 148
• Geography
  • metamathematical, 154
• GeometricScene, 91
• Geometric series
  • sum of, 173, 175–176
• 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, 79–82
  • models of, 97
  • textbook theorems of, 82
  • theorem distribution in, 110
• Groupoids
  • central, 110
• Groups, 24

H

• Hanoi
  • Towers of, 115
• Harmonic series
  • divergence of, 173, 175–176
• 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, 1862–1943), 192, 213
• Hilbert’s Program, 184, 192
• History
  • accidents of mathematical, 154
  • of human mathematics, 119, 129, 191–195
• 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
  • of emes, 140
• Implicational calculus, 110
• Implies
  • functional completeness and, 162
  • in combinators, 138
• Inclusion/Exclusion
  • Principle of, 173, 175–176
• 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, 175–176
  • in axioms of arithmetic, 94
  • in Peano axioms, 94
• Inductive inference
  • limits of, 188
• Inference
  • laws of, 8
• Infinitude of primes, 173, 175–176
• 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
  • and proofs, 57–58
  • in Boolean algebra, 157–158, 204
  • in Euclid, 168
• Intermediate steps
  • in proofs, 70, 168
  • size of, 17
• Intermediate Value Theorem, 173, 175–176
• Interpretability
  • of combinator expressions, 138
• Intuition
  • about physical vs. metamathematical space, 145
  • in mathematics, 193
• Inventions
  • of mathematics, 181
• Irrationality of , 173, 175–176
• Island
  • of computational reducibility, 202
• Isomorphism
  • in hypergraphs, 49
• Isosceles triangle
  • proposition about, 163
• Isosceles Triangle Theorem, 173, 175–176

J

• Junctional calculus, 110

K

• K-theory, 199
• Klein four-group, 24
• Knitting
  • of entailment cones, 121
• Knowledge
  • mathematical, 154–163
• Königsberg bridge theorem, 173, 175–176

L

• L’Hôpital’s Rule, 173, 175–176
• Lagrange’s Theorem, 173, 175–176
• Languages (abstract)
  • for understandable mathematics, 198
• Law of Cosines, 173, 175–176
• Law of double negation, 84, 87, 162
• Law of excluded middle, 84–85, 87
• Law of noncontradiction, 84, 87
• Law of Quadratic Reciprocity, 173, 175–176
• Laws of inference, 8
  • and bisubstitution, 64
• Laws of mathematics, 3–5, 196
  • physicalized, 145, 148
• Laws of physics
  • alien, 202
  • from ruliad, 3
• Lean, 216
• Lebesgue Integration Theorem, 173, 175–176
• Leibniz’s series for π, 173, 175–176
• 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, 175–176
• Log (logarithm)
  • definitional distance of, 172
• Logic
  • construction of mathematics from, 192
  • empirical metamathematics of, 154–163
  • entailment cone of, 83
  • in combinators, 137–138
  • 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 Whitehead–Russell, 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, 154–163
  • 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, 154–180
  • 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, 5–6, 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, 175–176
• 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, 26–29, 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
  • empirical, 154–180
  • vs. mathematics, 19
• Metamodeling
  • of axiomatic math, 12
  • of mathematics, 139
• Microscopes, 201
  • metamathematical, 118
• Middle Ages, 124
• Mind
  • human, 192
• Mizar, 216
• Model theory, 96–104
  • 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, 5–6
• Molecular-level mathematics, 5–6, 8–10, 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, 19–25
  • 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, 84–85, 87
• Non-denumerability of continuum, 173, 175–176
• 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
  • of logic, 84, 87
• 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, 96–104
• 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, 59–64
• Peano Arithmetic, 94, 146, 184
• Peano, Giuseppe (Italy, 1858–1932), 213
• Pell equation, 173, 175–176
• Perception
  • and definition of mathematics, 195
  • and invention of mathematics, 181
• Perfect Number Theorem, 173, 175–176
• Persistence
  • of observers, 123, 144, 182
  • of observers and objects, 144
• 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, 427–347 BC), 191, 194, 206, 213
• Platonic view
  • of mathematics, 182, 192
• Plus
  • from set theory, 171
• Polynomial Factor Theorem, 173, 175–176
• Post, Emil L. (USA, 1897–1954), 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, 175–176
• 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, 175–176
• Progress
  • in mathematics, 119
• Proof assistants, 199
• Proof cone, 211
•     see entailment cone
• Proof graphs, 55–58, 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, 14–16
  • by automated theorem proving, 69–77
  • 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, 154–163
  • 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, 175–176
• pythi (formalization of Pythagorean theorem), 172

Q

• Quartic equations, 173, 175–176
• 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, 1908–2000), 214

R

• Ramsey’s Theorem, 173–176
• 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, 9–10
  • metamathematical, 29, 148
• Relativity
  • and theorem proving, 75
  • in mathematics, 11
  • metamathematical, 151–152
• 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, 35–38
  • in the Wolfram Language, 13
• Ruliad, 3–5, 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, 127–128
  • 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, 105–112
• Russell, Bertrand A. W. (England, 1872–1970), 191, 213

S

• S, K combinators, 132–140
• SatisfiableQ
  • as function involving proofs, 198
• Schemas (axiom), 94
• Schönfinkel, Moses I. (Germany/Russia, 1889– ~1942), 215
• Schröder–Bernstein Theorem, 173–176
• 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
  • rulial, 202
• 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, 175–176
• 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, 175–176
• 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 k^th powers, 173, 175–176
• Sylow’s Theorem, 173, 175–176
• 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, 175–176
• Telescopes, 201
  • rulial, 202
• Term rewriting
  • entailment in, 64
• Textbooks
  • of logic, 156
• Theorem dependency graph
  • for Euclid, 163
• Theorem proving
  • automated, 69–77
• 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, 173–179
  • 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
  • of time, 188
• 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
  • proof of, 173, 175–176
• 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, 16–17
  • and accumulative evolution, 42
  • in metamathematical space, 66
  • space of, 28
• Trees
  • vs. strings, 47
• Triangle
  • sum of angles of, 173, 175–176
• Triangle Inequality, 173, 175–176
• Triangular-number reciprocals, 173, 175–176
• Truth, 124–128
  • in combinators, 137
• Two-way hypergraph rewriting, 50
• Two-way rules, 35
  • accumulative evolution with, 39–41
  • 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
  • of emes, 140
• Uniquification
  • and generated variables, 32–34
  • 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, 175–176
• 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, 1861–1947), 191, 213
• White holes
  • and falsity, 151
• Wilson’s Theorem, 173, 175–176
• 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

X–Y

• Xor
  • functional completeness and, 162
•  
   
•  
   

Z

• Zermelo, Ernst F. F. (Germany, 1871–1953), 213
• Zermelo–Fraenkel 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