Can the pool of patterns contain patterns that do not assert a truth value?
The full pool contains all possible pattern expressions....
We look at a certain slice of this pool, and that gives us recognizable math....
Simple case: single arbitrary axiom
Plus some rules about equality?
Enumerations: all possible initial conditions (i.e. arbitrarily sized pool of patterns) [or could be generated from nothing, by rules] all possible rules
Metamodels of mathematics
Possible model: equational axiom systems
Pure substitution model
The distinguished operator is ==, AKA and ←
? constructivist view: you can only do substitutions at the root ??
Critical pair lemmas require using equality...
Expression expression using an axiom
In here, lhs can be a subpart of expr1
This requires some additional rules for <-> (e.g. the fundamental rule is with , but there is a rule that allows reversal [and the reversal could involve rewriting what is a pattern variable])
Basic design issue: is there a meaningful notion of a 2-way pattern? [twp]
Entailment is just: apply a twp to a twp, to get a twp
How are variables shared across twps?
The · should be shared. The individual a’s etc. should not.
The goal of the equational theorem prover is to produce TWPs of the form lhs ↔ True
There is nothing absolute about True; cf there is no absolute space.... Everything is defined by relations; even the concept of truth....
(cf category theory)
Fundamental assumption: our TWPs are operating on trees/expressions
This could be modeled with hypergraphs, but that’s lower level. Hypergraphs may be more convenient for physics; trees for math....
In physics, we are dealing with pure “relations” i.e. one-level lists....
In math, modeling human language, we’re dealing with trees...
“Phrase structured math”
Analog of TWPs for hypergraphs
With this foliation, it just alternates back and forth:
What does it look like if there is “learning” in the set of rules?
I.e. from a rule we derive another rule, by evolving one of the sides of the rule
This is inducing transitive closure in the transformations between elements
Encoding with hyperedges...
Comparison between math and physics:
In math, every relation that has been discovered is used any time in the future In (ordinary) physics, things happen again and again; they are not cached We can imagine a transitive closure of physics, where anything that has happened is cached; in the ordinary model, only the “underlying rules” are cached
Caching in the ruliad
The ruliad involves all possible rules. But given a particular point in the ruliad, it takes time to reach other rules, because you have to build them up from your local rules.
In the presence of computational irreducibility “it’s already there” is something super-computational
And it’s not accessible by a computationally bounded observer
Difference between math and physics
In physics, we imagine that there are a finite set of underlying rules from which we can derive everything; but ... we could have “cached” higher-level rules
In math, we imagine that there a finite set of axioms from which we can derive everything ... but we like to have higher-level cached lemmas
PCE implies that you can start from essentially any set of rules, in both physics and math. What then matters is the relation of the observer to these rules.
Are the observed laws of mathematics based on the observed laws of physics, or vice versa?
Analogy: given a random UTM, we can make it emulate [whatever we want]
Given a random tree rewriting system ... we can make it emulate some area of math
Axioms and their typical laws of inference are just one possible basis for math; any computational system is also a basis
Construction of reference frames ↔ what instrumentation is available in science
The mathematical interpretation of the advance of instrumentation is different reference frames in the ruliad
Axiomatic math will be brittle wrt reference frame; math as practiced by mathematicians will not be
Minimal TWP generator
Case 1: hypergraph-like relations
Case 2: tree structures
1. In patt1 (lhs1->rhs1) where does lhs2 (from patt2) apply? Create patt3 from all possible such rule applications
Are there in fact two kinds of things in math? (a) expressions, and (b) rules? [cf. objects and morphisms] [in type theory: general types ; function types ] (all of these representations happen to [nowadays] use arrows for the rules/morphisms/functions)
[ We might minimally build up just as category theory does... ]
modus ponens rule....
What we want is a multiway graph whose states are complete lists of TWPs : those states are states of mathematics, with certain proofs made
Decidability in the bulk limit
There might be things which depend on details at the molecular dynamics level ... but which inevitably come out a certain way for human-like mathematical observers at the bulk scale where mathematicians operate
Calculus and continuum structures are used both in physics and in mathematics
The continuous description of the mathematical world is like the continuous description of the physical world
Mathematicians think in terms of the continuum; ATPs think in terms of discrete symbolic expressions
“statement” vs “statement is true”
There may be statement which can’t be generated within a certain reference frame, or can’t be seen there
Constructivism : can “statement” be constructed?
Types of equivalence classes in TEGs
States constructed from tokens
Model theory coordinatizes metamathematical space
For a given model, more than the general theorems will be true (e.g. group theory)
Certain theorems are true of all groups; more are true for specific groups
I.e there are additional TWPs that will be true if we just construct them with a particular model for the operator
This TWP might be provable from the axioms we’ve chosen... Or it might just be that a specific model (e.g. finite model) for f (and for a, b etc.) will make it true
But there is a particular multiplication table which is symmetric, and for which
By using models, we can go faster than the speed of proof.... Because we can immediately reach a TWP that would take many proof steps to reach
E.g. look at TWPs that can be generated by many models; how close is that set to the set that can be generated by proofs?
E.g in Peano arithmetic, look at reverse mathematics and ask what theorems can robustly be generated in many models...
Special relativity is a statement about the equivalence of models (?)
What is the analog of GR in math?
?? the continuum exists
In metamathematics, we’re taking the continuum limit in proof space. How is that related to the continuum limit in “physical” space?
Are these related through the ruliad, and Grothendieck’s hypothesis?
Claim: if we’ve done enough proofs, we’ll start seeing signs of the continuum
If one has enough theorems about integers ... it’ll be like making a statement about reals [???]
Can we find proof cones in TWP dynamics?
Probably: proof cones will emerge if the entailment rules maintain bounded information content
Abstraction and equivalence classes created by observers