|
| |
|
|
A369587
|
|
Irregular triangle read by rows: row n lists the number of symbols of the shortest proof (see comments) for each of the distinct derivable strings (theorems) in the MIU formal system that are n characters long.
|
|
5
|
|
|
|
2, 13, 5, 5, 68, 17, 44, 20, 44, 9, 52, 52, 31, 52, 18, 31, 52, 31, 10, 31, 10
(list;
graph;
refs;
listen;
history;
text;
internal format)
|
|
|
|
OFFSET
|
2,1
|
|
|
COMMENTS
|
See A368946 for the description of the MIU formal system and A369173 for the triangle of corresponding strings.
Strings are encoded by mapping the characters M, I, and U to 3, 1, and 0, respectively.
In case more than one shortest proof exists, the lexicographically earliest one (after encoding) is chosen.
|
|
|
REFERENCES
|
Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.
|
|
|
LINKS
|
|
|
|
EXAMPLE
|
Triangle begins:
[2] 2;
[3] 13 5 5;
[4] 68 17 44 20 44 9;
[5] 52 52 31 52 18 31 52 31 10 31 10;
...
For the theorem MIUU (3100), which is given by A369173(4,4), the shortest proof is MI (31) -> MII (311) -> MIIII (31111) -> MIIIIU (311110) -> MIUU (3100), which consists of a total of 20 symbols (counting only M, I and U characters): T(4,4) is therefore 20.
|
|
|
MATHEMATICA
|
MIUStrings[n_] := Map["3" <> FromCharacterCode[# + 48] &, Select[Tuples[{0, 1}, n - 1], ! Divisible[Count[#, 1], 3] &]];
MIUNext[s_] := Flatten[{If[StringEndsQ[s, "1"], s <> "0", Nothing], s <> StringDrop[s, 1], StringReplaceList[s, {"111" -> "0", "00" -> ""}]}];
Module[{uptolen = 5, searchdepth = 10, mi = "31", g}, g = NestGraph[MIUNext, mi, searchdepth]; Map[Quiet[Check[Map[FromDigits, StringLength[StringJoin[If[# == mi, #, First[Sort[FindPath[g, mi, #, {GraphDistance[g, mi, #]}, All]]]]]]], "Not found"]] &, Array[MIUStrings, uptolen - 1, 2], {2}]] (* Considers theorems up to 5 characters long, looking up to 10 steps away from the MI axiom -- please note it takes a while *)
|
|
|
CROSSREFS
|
|
|
|
KEYWORD
|
nonn,tabf,hard,more
|
|
|
AUTHOR
|
|
|
|
STATUS
|
approved
|
| |
|
|
