Thing 1: Find an MW with unruly (but slow) growth in the total number of distinct (i.e. not uniquified across time) string.

Thing 1a: <Make pictures of evolution after uniquification> [explicit time has been removed, in the same way as it is in mathematical proofs, if one remembers what theorems one has proved]

Thing 2: Find MWs with short theorems and long proofs [uniquified is the only thing that is relevant]

Thing 1a: <Make pictures of evolution after uniquification> [explicit time has been removed, in the same way as it is in mathematical proofs, if one remembers what theorems one has proved]

Thing 2: Find MWs with short theorems and long proofs [uniquified is the only thing that is relevant]

Thing ℵ: Illustrate how adding a new axiom (rule) to the MW rules can rearrange the metric on the space of theorems.

### Other random notes

Other random notes

Normally in mathematics the same rules of inference are always used. (p ∧ pq)q is equivalent to actually performing the multiway substitution.

Theorem: statement that can potentially be proved to be true

Axiom: a theorem one starts from

Theorem: statement that can potentially be proved to be true

Axiom: a theorem one starts from

True⟶"AAABBBBA"

{"ABBB","BBA"}

"AAABBBB""BBBA"

True"ABBBAA"

{"A""ABBBA","A""BBBAA"}

a,ab⊢b

ab⊢b

ABAA,A

"AAA","A"