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).

1, 4, 2, 2, 11, 5, 8, 5, 8, 3, 9, 9, 6, 9, 5, 6, 9, 6, 3, 6, 3

Offset: 2

Author

Paolo Xausa, Jan 22 2024

Keywords

• nonn
• tabf
• hard
• more

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.

Examples

			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.
		

References

• Douglas R. Hofstadter, Gödel, Escher, Bach: an Eternal Golden Braid, Basic Books, 1979, pp. 33-41 and pp. 261-262.

Links

• Wikipedia, MU Puzzle.
• Index entries for sequences from "Goedel, Escher, Bach".

Crossrefs

Cf. A024495 (row lengths), A331536, A368946, A369173, A369410.

Cf. A369586 (proofs), A369587 (number of symbols).

Programs

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}]]

Formula

T(n,k) <= A369410(n,k).