The Metamathematics Project
Conceptual Review and Framework
Machine-Code Level (‘Ur Level’)
Machine-Code Level (‘Ur Level’)
This level hosts all possible combinators whose operations correspond to two-way rules (which minimize ‘hair’). Combinators are the primordia of our framework, their ‘elements’ constituting the ‘urons/urads/uremes’ of metamathematics.
We need not employ operators (i.e. combinators such as x ↔ x[x] may suffice).
Combinator evaluations remain syntactic.
Combinators possess computation cones.
The ‘machine ocean’ necessarily accommodates syntactic rules that would, semantically, yield absurdities if subject to mathematical observation.
Nonetheless, the machine-code for recognizable mathematics lies within the machine ocean.
Low-hanging fruit: combinators for addition, multiplication, exponentiation.
We need not employ operators (i.e. combinators such as x ↔ x[x] may suffice).
Combinator evaluations remain syntactic.
Combinators possess computation cones.
The ‘machine ocean’ necessarily accommodates syntactic rules that would, semantically, yield absurdities if subject to mathematical observation.
Nonetheless, the machine-code for recognizable mathematics lies within the machine ocean.
Low-hanging fruit: combinators for addition, multiplication, exponentiation.
The Machine-Code/Meta-Mathematics Interface
The Machine-Code/Meta-Mathematics Interface
Machine-code evaluations generate ‘halos’ of familiar mathematical expressions/theorems.
A metamathematical halo is a common expression/theorem generated by different combinators (i.e. multicomputational confluence).
Case to pursue: the Pythagorean Halo
Claim: the machine labor involved in halo generation exceeds that undertaken by human mathematicians
(It is here from which physics too arises.)
A metamathematical halo is a common expression/theorem generated by different combinators (i.e. multicomputational confluence).
Case to pursue: the Pythagorean Halo
Claim: the machine labor involved in halo generation exceeds that undertaken by human mathematicians
(It is here from which physics too arises.)
The Meta-Mathematics Level
The Meta-Mathematics Level
When discussing the meta-mathematical level, we speak of entailments rather than machine evaluations.
Axioms (or collections thereof) and expressions each possess an entailment cone.
Entailment proceeds by substitution and co-substitution.
Distance between expressions in meta-mathematical space is a matter of variable position [i.e. the Murzin Position Hypothesis].
Case to pursue: entailments from axioms in the Metamath language.
Case to pursue: Euclid’s theorems as entailments from axioms.
Axioms (or collections thereof) and expressions each possess an entailment cone.
Entailment proceeds by substitution and co-substitution.
Distance between expressions in meta-mathematical space is a matter of variable position [i.e. the Murzin Position Hypothesis].
Case to pursue: entailments from axioms in the Metamath language.
Case to pursue: Euclid’s theorems as entailments from axioms.
The Meta-Mathematics/Mathematics Interface
The Meta-Mathematics/Mathematics Interface
Entailments in meta-mathematical space achieve a recognizable mathematical register if they obey persistence in a manner amenable to observation.
Amenability to observation of an expression or axiomatic system depends on its entailment cone. If the cone admits absurd entailments, then little reliable mathematical work can be extracted therefrom. For instance, rules such as a↔b that entail all expressions are degenerate and fail to find mathematical purchase, despite their feasibility in meta-mathematical space.
Hypothesis: the procession from metamathematical space to mathematical observer-use requires persistent propagation a clear rule, or ‘proof fitness’.
Further meta-modeling is required to understand the qualities of entailments that yield recognizable mathematics (i.e. fitness criteria). It may also be the case that there exist fit, but nonetheless unfamiliar entailment cones, which may occasion inquiry into alternative mathematical systems (i.e. valid mathematics not used by human observers).
Amenability to observation of an expression or axiomatic system depends on its entailment cone. If the cone admits absurd entailments, then little reliable mathematical work can be extracted therefrom. For instance, rules such as a↔b that entail all expressions are degenerate and fail to find mathematical purchase, despite their feasibility in meta-mathematical space.
Hypothesis: the procession from metamathematical space to mathematical observer-use requires persistent propagation a clear rule, or ‘proof fitness’.
Further meta-modeling is required to understand the qualities of entailments that yield recognizable mathematics (i.e. fitness criteria). It may also be the case that there exist fit, but nonetheless unfamiliar entailment cones, which may occasion inquiry into alternative mathematical systems (i.e. valid mathematics not used by human observers).
The Mathematics Level
The Mathematics Level
Mathematics is observable entailment subject to the constraints introduced above.
Each mathematical proof has its own entailment complexity. It remains unknown the factor by which the complexity of proofs in advanced pure math (e.g. Fermat’s Last Theorem) and proofs in introductory mathematics (e.g. the Pythagorean theorem) differ.
Each mathematical proof has its own entailment complexity. It remains unknown the factor by which the complexity of proofs in advanced pure math (e.g. Fermat’s Last Theorem) and proofs in introductory mathematics (e.g. the Pythagorean theorem) differ.
The Mathematics/Observer Interface
The Mathematics/Observer Interface
Different mathematical observers exist. Establishment of mathematical fields concentrates observer activity at particular entailment fronts (i.e. observer-theoretical reference frames).
Math genealogy data can be represented as a multiway [causal?] graph of mathematical observers.
Observer motion is translation between entailment fronts (i.e. ‘horizontal multicomputation’), or the establishment of correspondences between mathematical fields (e.g. the Langlands Functoriality conjecture).
Math genealogy data can be represented as a multiway [causal?] graph of mathematical observers.
Observer motion is translation between entailment fronts (i.e. ‘horizontal multicomputation’), or the establishment of correspondences between mathematical fields (e.g. the Langlands Functoriality conjecture).
The Observer Level
The Observer Level
The observer level is the domain of the working mathematician.
The mathematician (as opposed to the metamathematician or the metamathematical ruliologist) may have reason not to care about sub-observer levels.
The mathematician (as opposed to the metamathematician or the metamathematical ruliologist) may have reason not to care about sub-observer levels.
The Observer/Ruliad Interface
The Observer/Ruliad Interface
The art of abstraction augments the expanse of a given observer within the ruliad.
Human ruliologists can use computers to pursue systems of mathematics that are not mere physical inheritances; with computers, we can ‘wiggle’ in rulial space.
The ‘Mathematical Censorship’ hypothesis: certain mathematical theorems may constitute entailment singularities (i.e. observers cannot follow their entailments).
Human ruliologists can use computers to pursue systems of mathematics that are not mere physical inheritances; with computers, we can ‘wiggle’ in rulial space.
The ‘Mathematical Censorship’ hypothesis: certain mathematical theorems may constitute entailment singularities (i.e. observers cannot follow their entailments).
The Ruliad/Hyper-Ruliad Interface
The Ruliad/Hyper-Ruliad Interface
Ruliad spillage into the hyper-ruliad may occur if the continuum hypothesis is false (i.e. if there exists a set of cardinality greater than the set of all possible Turing machines and less than the set of all possible Turing machine outputs).
Math Formalization Questions
Math Formalization Questions
I.e. Intriguing questions that Avigad should care about.
What is the distribution of ‘halo density’ for expressions? Are some obtained from more combinators than others?
Are halo realizers continuously deformable (i.e. is there a possibility of motion between realizers in machine space)?
Is it possible to prove the minimality of combinators at machine-level?
Can we explain proof fitness ruliologically?
Do there exist unrecognizeable, but nonetheless fit, entailments (i.e. allomathematical systems)?
Can we identify more combinators that the populate machine-code level?
Under what conditions might mathematical censorship hold?
What is the entailment complexity of Fermat’s Last Theorem? The Pythagorean Theorem? By what factor does the former exceed the latter?
Under what conditions should the working mathematician care about sub-observer levels?
Are halo realizers continuously deformable (i.e. is there a possibility of motion between realizers in machine space)?
Is it possible to prove the minimality of combinators at machine-level?
Can we explain proof fitness ruliologically?
Do there exist unrecognizeable, but nonetheless fit, entailments (i.e. allomathematical systems)?
Can we identify more combinators that the populate machine-code level?
Under what conditions might mathematical censorship hold?
What is the entailment complexity of Fermat’s Last Theorem? The Pythagorean Theorem? By what factor does the former exceed the latter?
Under what conditions should the working mathematician care about sub-observer levels?