Given two different axiom systems, can we determine whether two differently-stated theorems are “the same”
In group theory, each group is like a different axiom system ;; even each presentation of the group (e.g. choice of generators)
[ cf representation theory ]
What results are there in group theory that are “continuum limit” results, independent of which group you’re talking about ... [ There are results in pure group theory like this ... But what about results which are “roughly” true for any big group / big representation ]
Equivalence of types ?
Why is undecidability uncommon in math?
?? For the same reason that gas molecules usually have a short mean free path
Computation [e.g. ruliology] is like free-streaming molecules ; whereas human-processed math is like a gas
In physical space ... consider Euclid
Different underlying hypergraphs all limit to satisfying (approximately) Euclid’s axioms + Euclid’s theorems
[ Mathematicians don’t “live in the mathematics” ... unlike for physics ]
Possible claim: The only math that we think of doing is math informed by our experience in the actual universe
[ E.g. claim: numbers are inevitable given basic physical consciousness ] [ E.g. geometry is a consequence of our consciousness / character as observers ]
Claim: we end up with comprehensible physics for the same reason as we end up with comprehensible mathematics
Is the notion of the continuum deeply related to the character of us as observers?
The observer has continuity / persistence between moments in time
“It’s the same ‘me’ at different moments in time”
Persistence of the observer perception of a continuum
Otherwise, there would be a discontinuity
Our perception is that time is a continuum ; there are no discrete “not us” steps
The observer typically cares about phenomena that persist
A detail of some automated proof that has no persistence is not going to be “noticed”
From an automated proof, can we recognize something that’s a bigger picture?
Is metamathematical space like swiss cheese ... with many topological obstructions?
Does computational irreducibility that this has to be the case?
?? Rulial space for Turing machines
Calculus is the “linguistic construct” that connects observers like us with physical reality
[Things to look up]
We want to use a structure that looks like traditional math
so that we can compare with empirical metamathematics
Pure semigroup theory, with pure substitution, can reach only a finite number of results....
Now introduce a↔a as an axiom
Now try critical pair rule
Substitution lemmas are basically like ReplaceAll
What is the meta-idea of all symbolic rules of inference?
Variables can be replaced by expressions ... Then one uses the rule to say what the transformation is.
Do this replacement everywhere; then go from LHS to RHS of the rule
This is the general notion of a pattern ... together with the general notion of a transformation
[For strings, it’s confusing ... because it looks like we’re just replacing with literals]
Now use rule #2 to get
Now use this to replace a_
In substitution, you are replacing matching subtrees according to some rule
This will work for one-way rules
When there are two-way rules,
Instantiate the variable with:
f[b_] matches a_
Now use rule #2 in rule #1:
Now rule #2 is
this is valid, but it’s just a substitution rule
now replace a_ with f1[b_]
Basic concept of axioms/propositions/math/rules/....
The rules give templates for what should happen, that can be applied in many contexts...
E.g. string substitution: “wherever ABA occurs, replace it” [[ and copy the unchanged parts of the string ]] E.g. cellular automata : “wherever 101 occurs, replace it” E.g. combinators: “wherever this ‘top of tree occurs’ replace it copying the subtrees”
substitution lemma: find where this a match, and copy subtrees [[ and the supertree ]]
(The supertree is your context .... just like the “residue” of the unaffected part of a string)