## Miscellaneous Metamathematics Notes

(Transcribed from calls with SW: 11/20-11/21)

Miscellaneous Metamathematics Notes

(Transcribed from calls with SW: 11/20-11/21)

(Transcribed from calls with SW: 11/20-11/21)

## Expression Distance

Expression Distance

We should calculate distance between expressions.

SW question: Can we think of such distance as branchial distance?

(Nik, independently, expressed to me today that he thinks of distance between expressions in terms of variable position, which can in turn be examined with branchial graphs.)

SW question: did he mention tree distance in his combinator post?

James’ answer: yes

SW question: Can we think of such distance as branchial distance?

(Nik, independently, expressed to me today that he thinks of distance between expressions in terms of variable position, which can in turn be examined with branchial graphs.)

SW question: did he mention tree distance in his combinator post?

James’ answer: yes

“One approach would just be to look at ‘raw distances’ between trees—say based on asking how many edits have to be made to one tree to get to another. But an approach that more closely reflects actual features of combinators is to think about the concept of branchial graphs and branchial space that comes from our Physics Project.”

## Metamathematical Studies

Metamathematical Studies

Consider the Pythagorean Halo and arithmetic halos

At the machine-code level, we should consider the commutativity of arithmetic and successor functions.

We must ‘compile Metamath’ (the Metamath language, that is).

What is the ratio between the number of operations necessary to ‘reach’ the proof of Fermat’s Last Theorem and the number of operations necessary to reach the Pythagorean theorem? What if the ratio between the two is surprisingly modest?

Study the Math Genealogy Project tree (mathematical time, mathematical observers, etc.).

Question: What is the mathematical observer for string-based systems?

Can we yield the same results as FindEquationalProof simply by performing substitution on the original axioms?

At the machine-code level, we should consider the commutativity of arithmetic and successor functions.

We must ‘compile Metamath’ (the Metamath language, that is).

What is the ratio between the number of operations necessary to ‘reach’ the proof of Fermat’s Last Theorem and the number of operations necessary to reach the Pythagorean theorem? What if the ratio between the two is surprisingly modest?

Study the Math Genealogy Project tree (mathematical time, mathematical observers, etc.).

Question: What is the mathematical observer for string-based systems?

Can we yield the same results as FindEquationalProof simply by performing substitution on the original axioms?

## On the Necessity of Tree Idealizations

On the Necessity of Tree Idealizations

At the machine code level, is it necessary to use trees, or can we just use prefix notation?

## Ruliology and Metamath

Ruliology and Metamath

Some simple rules, by merit of uniqueness, do not form halos. Others that correspond to equivalents (and are thus amenable to multicomputational) can form halos.

Simple rules, treated in isolation, offer us the opportunity to investigate machine-level undecidability.

Metamodeling is insufficiently applied to mathematics.

## Metamathematical Motion

Metamathematical Motion

Metamathematical motion is proof translation.

Model theory allows us to inquire into the statements that can be accessed via motion.

Model theory allows us to inquire into the statements that can be accessed via motion.

## Planning

Planning

SW will begin writing the blog next week.

Nik and James will be on-call for real-time assistance.

Nik and James will be on-call for real-time assistance.