login
A369408
Irregular triangle read by rows: T(n,k) is the length of the shortest proof for the MIU formal system string (theorem) given by A369173(n,k).
8
1, 4, 2, 2, 11, 5, 8, 5, 8, 3, 9, 9, 6, 9, 5, 6, 9, 6, 3, 6, 3
OFFSET
2,2
COMMENTS
See A368946 for the description of the MIU formal system and A369173 for the triangle of the corresponding derivable strings.
The length of the shortest proof for a string (theorem) S is the number of lines of the shortest possible derivation of S.
A369173(n,k) first appears in row T(n,k) - 1 in triangle A368946.
REFERENCES
Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.
FORMULA
T(n,k) <= A369410(n,k).
EXAMPLE
Triangle begins:
[2] 1;
[3] 4 2 2;
[4] 11 5 8 5 8 3;
[5] 9 9 6 9 5 6 9 6 3 6 3;
...
For the theorem MUI (301), which is given by A369173(3,1), the shortest derivation from the axiom MI is MI (31) -> MII (311) -> MIIII (31111) -> MIU (301) (4 lines), so T(3,1) = 4.
MATHEMATICA
MIUStringsW3[n_] := Map[FromCharacterCode[# + 48]&, Select[Tuples[{0, 1}, n - 1], ! Divisible[Count[#, 1], 3] &]];
MIUStepDW3[s_] := DeleteDuplicates[Flatten[Map[{If[StringEndsQ[#, "1"], # <> "0", Nothing], # <> #, StringReplaceList[#, {"111" -> "0", "00" -> ""}]} &, s]]];
Module[{rowmax = 5, treedepth = 10, tree}, tree = NestList[MIUStepDW3, {"1"}, treedepth]; Map[Quiet[Check[Position[tree, #, {2}][[1, 1]], "Not found"]]&, Array[MIUStringsW3, rowmax - 1, 2], {2}]]
CROSSREFS
Cf. A024495 (row lengths), A331536, A368946, A369173, A369410.
Cf. A369586 (proofs), A369587 (number of symbols).
Sequence in context: A095800 A055630 A182700 * A136202 A075418 A199221
KEYWORD
nonn,tabf,hard,more
AUTHOR
Paolo Xausa, Jan 22 2024
STATUS
approved