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"