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

Links

Table of n, a(n) for n=2..22.

Wikipedia, MU Puzzle.

Index entries for sequences from "Goedel, Escher, Bach".

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

Adjacent sequences: A369405 A369406 A369407 * A369409 A369410 A369411

Keyword

nonn,tabf,hard,more

Author

Paolo Xausa, Jan 22 2024

Status

approved