|
|
A369586
|
|
Irregular triangle read by rows: row n lists the lines of the shortest proof for the MIU formal system string (theorem) given by A369173(n+1).
|
|
6
|
|
|
31, 31, 311, 31111, 301, 31, 310, 31, 311, 31, 311, 31111, 311111111, 3011111, 30011, 300110011, 3001100110, 30011110, 300100, 3001, 31, 311, 31111, 301, 3010, 31, 311, 31111, 311111111, 3011111, 30111110, 301100, 3011, 31, 311, 31111, 311110, 3100, 31, 311, 31111, 311111111, 3101111, 31011110, 310100, 3101, 31, 311, 3110
(list;
graph;
refs;
listen;
history;
text;
internal format)
|
|
|
OFFSET
|
1,1
|
|
COMMENTS
|
See A368946 for the description of the MIU formal system.
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:
[1] 31;
[2] 31 311 31111 301;
[3] 31 310;
[4] 31 311;
[5] 31 311 31111 ... 30011 300110011 3001100110 30011110 300100 3001;
...
For the theorem MUI (301), which is given by A369173(3,1) or (after flattening) A369173(3), the shortest proof is 31 -> 311 -> 31111 -> 301, which is row 2 of the present sequence (same as the "normal" proof, cf. A369409).
For the theorem MIUU (3100), which is given by A369173(4,4) or (after flattening) A369173(9), the shortest proof is 31 -> 311 -> 31111 -> 311110 -> 3100, which is row 8 of the present sequence (shorter than the "normal" proof).
|
|
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, If[# == mi, {#}, First[Sort[FindPath[g, mi, #, {GraphDistance[g, mi, #]}, All]]]]], {"Not found"}]] &, Flatten[Array[MIUStrings, uptolen - 1, 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
|
|
AUTHOR
|
|
|
STATUS
|
approved
|
|
|
|